A while ago, on PR 12903 (I don't know why it's not closed yet, FWIW,
because I think it's fixed), we had this discussion:
Me: I think this should work.
#lang typed/racket
(struct: (A) bar ([proc : (A -> Any)]))
(define-predicate -bar? (bar Any))
Sam: That's evil; here's why. Suppose `bar` had a predicate with type
(Any -> Boolean : (bar Any)). You could do this:
(define: v : Any (bar (lambda: ([x : Integer]) (add1 x))))
(when (my-bar? v) ;; check that `v` is a `(bar Any)`
(define: f : (Any -> Any) (bar-proc v)) ;; type-correct: A = Any
(f "not an integer"))
Me: Got it. [Consults this answer every time it comes up, because he
forgets why a useful `bar?' predicate is bad.]
So here's my latest question. Say we have these definitions:
#lang typed/racket
(struct: (A) foo ())
(struct: (A) bar foo ([proc : (A -> Any)]))
Could `bar?' have the type (All (A) ((foo A) -> Boolean : (bar A)))?
Then (I think), something like this should type:
(: maybe-foo-proc (All (A) ((foo A) -> (U #f (A -> Any)))))
(define (maybe-foo-proc v)
(if (bar? v) (bar-proc v) #f))
(Well, it wouldn't currently; the error is "Expected (bar A); given
#(struct:#<syntax:4:13 bar> ((Nothing -> Any)))".)
Is that also evil? I hope not, because the useless type of `bar?' is
precluding a possibly important performance enhancement.
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
