[racket-dev] goofy type hack (was: Re: type-case + typed racket yet?)

From: John Clements (clements at brinckerhoff.org)
Date: Wed May 25 16:43:16 EDT 2011

On May 25, 2011, at 12:53 PM, Sam Tobin-Hochstadt wrote:

> On Wed, May 25, 2011 at 12:27 PM, John Clements
> <clements at brinckerhoff.org> wrote:
>> Is there a "best-practice" model for type-case-like things in typed racket yet? Obvious choices:
>> 
>> - tagged-list style, it's all a big cond but I have to use first, second, etc to refer to fields
>> - struct-union style, feels better but I don't get to use match (IIUC).
> 
> `match' and unions of structs should work fine together in Typed Racket.

Forgive me; I checked the docs & didn't see anything for 'match', but I see now that it works as I'd expect. 

Thanks!

Hang on, here's another question.

I see that typed racket doesn't signal an error on a match that doesn't have clauses for all possible inputs, which is entirely reasonable; since that will signal an error, that code should typecheck fine.

However, I might *want* typed racket to check that for me.  I managed to come up with this grozzz hack:

(: g ((U Number False) -> Number))
(define (g x)
  (cond [(number? x) (+ x 4)]
        [(false? x) 13]
        ;; type of x is now uninhabitable, so no typechecking error
        [else (begin (string-append x "abc") (error 'foo))]))

In this case, when I comment out the 'false?' clause, the bogus clause suddenly is type-checked (because x's type is no longer the empty union), and I get an error.

So... I can get what I want, but in a very icky way.  Is there a different and more elegant way to force typed racket to check that I'm not failing to match?	

John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4624 bytes
Desc: not available
URL: <http://lists.racket-lang.org/dev/archive/attachments/20110525/3e55cfc6/attachment.p7s>

Posted on the dev mailing list.