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.
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.
