# Pattern matching in TypedRacket that uses types to rule out impossible branches?

**URL:** <https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743>\
**Category:** Questions & Answers\
**Tags:** question, typed-racket\
**Created:** [February 27, 2023, 10:16pm UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743 "2023-02-27T22:16:53Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![AssertionError](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/assertionerror/32/1016_2.png) [@AssertionError](https://racket.discourse.group/u/AssertionError)\
**Post date:** [February 27, 2023, 10:16pm UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743/1 "2023-02-27T22:16:53Z")

</div>

Hi everyone,

I was wondering if anyone is aware of any pattern-matching-like macro for TypedRacket that supports types.

For instance, consider the following thunk that holds a list. Type-wise there are two problems:

1. `l` is a thunk, yet both patterns are of a `list`. TypedRacket makes no note of these impossible branches.
2. The recursive call `(len2 l)` would require `l` to be a thunk, which is also impossible

```scheme
(: foo (All [T] (-> (-> (Listof T)) Number)))
(define (foo l1)
  (match l1
    [(list) 0]
    [(list _ l2 ...) (+ 1 (foo l2))]
  )
)

```

It feels that whatever pattern I write, TypedRacket will make its best to assume some arbitrary type necessary to typecheck each branch, which can lead to subtle programming errors.

Is there a better alternative to `match` that rules out impossible branches?

FYI,

```scheme
$ racket --version
Welcome to Racket v8.2 [cs].

```

---

<div class="post-metadata">

**Author:** ![jbclements](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/jbclements/32/11_2.png) [@jbclements](https://racket.discourse.group/u/jbclements)\
**Post date:** [February 28, 2023, 12:17am UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743/2 "2023-02-28T00:17:28Z")

</div>

I think in your very last sentence you put your finger on the problem. The issue here is that the right-hand-sides of these clauses are actually unreachable! This means that the match expression is guaranteed to signal a runtime error, and therefore the whole expression has type `None`, which means that _no type errors will occur during the execution of this program_, which is exactly the goal of the type checker. So the type checker has done its job.

A reasonable response to this would be: "wait wait wait! The type checker _knows_ that this expression is guaranteed to raise an error. Isn't that something that the programmer might like to know?" And I would answer: yes, I (personally) think it would be great if there were some way for the type checker to inform the programmer about dead code and code that is guaranteed to signal an error. They could be warnings, for instance.

This is generally the point in the conversation where @samth tells me that (a) it's impossible, or (b) it's already done 🙂

---

<div class="post-metadata">

**Author:** ![LiberalArtist](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/liberalartist/32/151_2.png) [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)\
**Post date:** [February 28, 2023, 1:33am UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743/3 "2023-02-28T01:33:10Z")

</div>

I agree that the behavior of `match` in Typed Racket is less useful than people coming from languages like ML or Haskell hope it might be.

[I started writing before dinner, and meanwhile @jbclements has explained, but perhaps some of this is still useful.]

To understand the behavior of your program, it might help to think about `match` expanding it to code like this:

```scheme
#lang typed/racket

(: foo (All [T] (-> (-> (Listof T)) Number)))
(define (foo l1)
  (cond
    [(null? l1)
     0]
    [(list? l1)
     (define l2 (rest l1))
     (+ 1 (foo l2))]
    [else
     (error "no match")]))

```

Typed Racket actually does note that the branches are impossible, or your program would fail to typecheck!

The type of `list?` is `(-> Any Boolean : (Listof Any))`, where the proposition at the end says what the typechecker can know about any value for which `list?` returns `#t`.

By hovering over the closing parenthesis in DrRacket, we can see what Typed Racket has conclusded the type of the expression `(list? l1)` is `False`.

 ![Screenshot of DrRacket showing the tooltip over](https://global.discourse-cdn.com/free1/uploads/racket/original/2X/2/2dc9131409d83293e0e21ef20f51dcda2e4e1760.png)

I'll leave the room for improvement for others to discuss in more detail. It does seem like there could be some more useful warning about bottom cases, but I wouldn't be shocked if there's macro-generated code that relies on this behavior to typecheck. A pattern-matching form that does more useful things with types would certainly be nice to have, but I also know there are challenges to writing one.

The fact that `match` has an implicit `else` clause raising a runtime error surprises people who are used to pattern matching with an exhaustiveness checker. Interestingly, while in an untyped context `match`'s behavior is far preferable, `cond`'s implicit default `[else (void)]` is more useful for catching bugs in Typed Racket.

Maybe there are improvements that could be made to the pattern-matching caveats in the guide? [8&nbsp;Caveats and Limitations](https://docs.racket-lang.org/ts-guide/caveats.html#%28part._.Pattern_.Matching_and_.Occurrence_.Typing%29)

I tend to use `match` less in Typed Racket for these reasons. For convenient destructuring binding, you can get much of the same benefit using forms like `match-define` or `match-let` once you know the shape of the value you have.

---

<div class="post-metadata">

**Author:** ![AssertionError](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/assertionerror/32/1016_2.png) [@AssertionError](https://racket.discourse.group/u/AssertionError)\
**Post date:** [February 28, 2023, 1:36pm UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743/4 "2023-02-28T13:36:06Z")

</div>

Thank you @jbclements and @LiberalArtist for the thorough and helpful responses!

Just as a clarification in terms of intention: I wasn't trying to imply that `match` is not doing its job or is unsound in any way.

I was hoping for an alternative to enable exhaustive checks in pattern matching (eg, a different primitive that is stricter than match), but it seems that there is no such option at the moment.

It's really interesting that DrRacket already has the information to identify dead code in `cond`. It would be great if that were `False` branches were identifiable through a warning as well.

---

<div class="post-metadata">

**Author:** ![samth](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/samth/32/3_2.png) [@samth](https://racket.discourse.group/u/samth)\
**Post date:** [February 28, 2023, 2:54pm UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743/5 "2023-02-28T14:54:37Z")

</div>

Typed Racket already issues warnings for the original program, reporting that there is dead code in the `match` expression. To see the warnings, you can turn on "show log" in DrRacket and enter "warning" in the text box. Unfortunately, Racket doesn't really have good infrastructure for warnings so this isn't easy to find. If there was a better way to issue a warning it would be easy for TR to use it.

---

<div class="post-metadata">

**Author:** ![hendrikboom3](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/hendrikboom3/32/2748_2.png) [@hendrikboom3](https://racket.discourse.group/u/hendrikboom3)\
**Post date:** [February 28, 2023, 6:53pm UTC](https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743/6 "2023-02-28T18:53:46Z")

</div>

The problem with such warnings is that a macro may have been written to take care of all possibilities, but that some of those possibities might actually be impossible in particular invocations. An optimisation of removing those impossibilities after expansion would be welcome, but getting warnings would just be distracting.

-- hendrik