Is there a way in TR to ensure that a match is exhaustive at type-checking
time? It seems to me like the right design would be a special TR form that goes
in expression positions and always signals a type error.
…
Actually, I did a bit of exploring, and it looks like I can almost "roll my
own", but that the expansion of ‘match’ is stymieing (yikes, sp?) me.
Specifically, with a conditional (as shown below), TR can deduce that the
‘else’ in the conditional is unreachable, and doesn’t signal a type error in
the program below. However, if I swap in the definition that uses ‘match,’ then
I get a type error. (I’m guessing that the expansion of match generates a
predicate that TR can’t reason about.)
Is there a better way to do this?
Thanks, and apologies if my searching just wasn’t thorough enough to find an
existing thread on this topic!
John
#lang typed/racket
(require typed/rackunit)
(struct NumC ([n : Number]) #:transparent)
(struct PlusC ([l : ExprC] [r : ExprC]) #:transparent)
(define-type ExprC (U NumC PlusC))
;; examples
(NumC 3)
(PlusC (NumC 3) (NumC 14))
;; TR can deduce that else is unreachable:
(: num-nums (ExprC -> Number))
(define (num-nums tree)
(cond
[(NumC? tree) 1]
[(PlusC? tree) (+ (num-nums (PlusC-l tree)) (num-nums (PlusC-r tree)))]
[else (/ 3 "type error")]))
;; Here, TR *cannot* deduce that else is unreachable
#;(define (num-nums tree)
(match tree
[(struct NumC (n)) 1]
[(struct PlusC (l r)) (+ (num-nums l)
(num-nums r))]
[other 34]
[other (/ 3 "type error")]))
(check-equal? (num-nums (NumC 3)) 1)
(check-equal? (num-nums (PlusC (NumC 3)
(PlusC (NumC 4)
(NumC 5)))) 3)
--
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.
