[racket-dev] [racket-bug] all/12434: match fails to signal type error?

On Fri, Dec 9, 2011 at 3:32 PM, Jay McCarthy <jay.mccarthy at gmail.com> wrote:
> This is now the fourth time I've seen people ask about this.
>
> Why can't Typed Racket be a little different than Racket and have another
> match form that does this or a notion of disjoint unions?

This has been implemented, and is used in Eli's PL class.  It just
needs to be merged into the main branch of PLAI development.

However, this doesn't give you what people seem to want, which is
having `match' report coverage errors.  Instead, it works only on its
notion of disjoint union, just as the regular PLAI forms do.

Having this work for `match', in general, is not in my opinion
feasible.  However, writing a version of `match' that puts
`typecheck-fail' in the else clause could work, although you'd need to
implement `match' differently in certain ways to avoid over-agressive
type errors.

> You've said many times that TR is for converting Racket programs, but
> clearly some of us want to write quasi-ML in TR, but we can't without hacks
> like this.

This (the `typecheck-fail' form) is not a hack -- it's a tool for
building exactly the thing you want.

>
> Jay
>
>
> On Fri, Dec 9, 2011 at 1:29 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu>
> wrote:
>>
>> I think what you're asking for is static errors for coverage failures
>> in `match' when used in Typed Racket.
>>
>> There are two reasons this isn't something I'm planning on doing in
>> general:
>> 1. It would be a significant change from the semantics of `match' in
>> Racket, which as you note raises a runtime error.
>> 2. It's unlikely to be precise enough in enough cases to be useful.
>> `match' is just too flexible, and TR insufficiently smart, for this to
>> be the right default.
>>
>> However, for this purpose, Typed Racket provides the `typecheck-fail'
>> form [1], for raising explicit type errors.  Rewrite your match
>> expression to:
>>
>> (match f
>>    [(list s) #true]
>>    [_ (typecheck-fail #'here #:covered-id f)])
>>
>> and you get the error message:
>>  Type Checker: Incomplete case coverage; missing coverage of Foo
>>
>> [1]
>> http://pre.racket-lang.org/docs/html/ts-reference/Utilities.html?q=type-e#%28form._%28%28lib._typed-racket/base-env/prims..rkt%29._typecheck-fail%29%29
>>
>> On Fri, Dec 9, 2011 at 3:20 PM,  <clements at brinckerhoff.org> wrote:
>> > *** Description:
>> > Code using match to take apart opaque types
>> > signal runtime match failure rather than
>> > a type-checking failure.
>>
>>
>>
>> --
>> sam th
>> samth at ccs.neu.edu
>
>
>
>
> --
> Jay McCarthy <jay at cs.byu.edu>
> Assistant Professor / Brigham Young University
> http://faculty.cs.byu.edu/~jay
>
> "The glory of God is Intelligence" - D&C 93



-- 
sam th
samth at ccs.neu.edu