> On Dec 9, 2017, at 1:04 PM, 'John Clements' via users-redirect > <us...@plt-scheme.org> wrote: > > TR doesn’t really do exhaustiveness checking, really, … except sorta. I’m > mostly just writing this to summarize my thinking and to see if there’s > something obvious I’m missing.
The Utilities section of the TR reference has the form `typecheck-fail`, with an example of a `cond`-like macro that does exhaustiveness checking. http://docs.racket-lang.org/ts-reference/Utilities.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._typecheck-fail%29%29 <http://docs.racket-lang.org/ts-reference/Utilities.html#(form._((lib._typed-racket/base-env/prims..rkt)._typecheck-fail))> I tried using it for `match`, but it seems to fail on everything, not just on incomplete matches. This is because `match` doesn't cooperate with occurrence typing enough for it to know that if a pattern succeeds then it can eliminate "that type" from clauses after that. It's like having only the #:+ propositions and not the #:- ones. And `match` features like (=> fail-id) and (failure-cont) will make that even harder. > I spent some time this morning debugging code that looked something like this: > > #lang typed/racket > > (define-type Format (U 'fmt-a 'fmt-b 'fmt-c)) > > (define (process-num [a : Number] [f : Format]) : Number > (match f > ['fmt-a (+ a 1)] > ['fnt-b (* a 2)] > [_ (+ a 1234)])) > > (process-num 2431 'fmt-b) > > > The problem is that the call winds up in the third case rather than the > second, because I’ve misspelled ‘fmt-b’ in the second clause of the match. > > I figured out the bug, of course, but then I had a moment of mild panic, > because that bug lived in the bin in my brain labeled “don’t worry, TR will > catch this kind of problem.” And, of course, that’s not true; TR is perfectly > happy to allow equality checks between elements of type Format and Symbol, > because *Racket* is perfectly happy to allow these comparisons, and that’s > kind of the whole point of TR. > > My thought process: > > 1) I looked for a “dead code” indication in TR, and the closest I could get > was hovering over the dead code for a tooltip. Currently, it appears that > the tooltip for dead code is… well, there is no tooltip. Maybe it would be a > good idea for the tooltip for dead code to signal “unreachable code” somehow? > > 2) I looked for a “dead code” indication in the Optimization > coach…unfortunately, I couldn’t figure out how to get the Optimization Coach > to signal dead code. Is it in there? I couldn’t find it. > > So then I started trying to figure out if I could code differently in order > to get around this. > > 3) Clearly the wildcard match is a problem; if I want TR to tell me something > about not being able to match, I’ve got to let TR know that falling off the > end is possible. So I can change the third pattern to ‘fmt-c’. Unfortunately, > I now discover that the very thing I *like* about match—namely, the fact that > it signals an error for no match—is going to kill the TR checking of this, > because of course errors don’t return, so the presence of the error *helps* > the code to type-check. > > 4) Instead, I can use a conditional, or a case. This is fragile, because I’ll > only get a type error if Void isn’t in the stated return type. My > recollection is that there’s an expression which has the type “Nothing”, but > I can’t remember what it is… and I can't seem to find it in the docs. > > > So, at the end of the day, if I want to get exhaustiveness checking for > things like this, it looks like my best practice is: a) use a case > expression, and b) mentally check that ‘void’ is not in the return type. > Does this sound right? > > John > > > > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
