[racket-dev] A more useful struct type predicate for structs with contravariant blah-de-blah?

That should be safe.

The issue is that TR cannot do it currently, because it doesn't
understand that (foo A) and (exists B. (bar B)) => (bar A). It instead
reduces this to (exists B. (bar B)) and then to (bar Nothing).

I'm working on some stuff that might make that easier to teach it the
correct thing but I am not sure if it will work.


On Fri, Aug 24, 2012 at 4:29 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> 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