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

Questions & Answers
,
1

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
(: 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,

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

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 :slight_smile:

2 Likes
3

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:

#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
Screenshot of DrRacket showing the tooltip over988×534 38.3 KB

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 Caveats and Limitations

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.

2 Likes
4

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.

5

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.

2 Likes
6

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

2 Likes