Type inference is failing you again.
If you instantiate `foo/s`, you get the type you expect:
#lang typed/racket
(struct (a) Foo ([val : (-> a a)]))
(: foo/s (All (a b)
(-> (-> a b)
(-> (Foo a)
(Foo b)
(Foo b)))))
(define (foo/s f)
(λ ([f1 : (Foo a)]
[f2 : (Foo b)])
f2))
(define r1 (#{foo/s @ Integer String} (λ ([x : Integer]) (format "~a" x))))
;> r1
;- : (-> (Foo Integer) (Foo String) (Foo String))
I wouldn't call this a bug, but it's definitely a program that a better
type inferencer should accept.
On Fri, Jul 21, 2017 at 5:19 AM, Sourav Datta <soura.ja...@gmail.com> wrote:
> Consider this program,
>
> #lang typed/racket
>
> (struct (a) Foo ([val : (-> a)]))
>
> (: foo/s (All (a b)
> (-> (-> a b)
> (-> (Foo a)
> (Foo b)
> (Foo b)))))
> (define (foo/s f)
> (λ ([f1 : (Foo a)]
> [f2 : (Foo b)])
> f2))
>
>
> (define r1 (foo/s (λ ([x : Integer]) (format "~a" x))))
>
> The type of r1 is correctly deduced as:
>
> - : (-> (Foo Integer) (Foo String) (Foo String))
> #<procedure>
>
> However, if I slightly change the struct Foo and do the same, like this:
>
> #lang typed/racket
>
> (struct (a) Foo ([val : (-> a a)]))
>
> (: foo/s (All (a b)
> (-> (-> a b)
> (-> (Foo a)
> (Foo b)
> (Foo b)))))
> (define (foo/s f)
> (λ ([f1 : (Foo a)]
> [f2 : (Foo b)])
> f2))
>
>
> (define r1 (foo/s (λ ([x : Integer]) (format "~a" x))))
>
> Now, r1 has this type:
>
> - : (-> (Foo Nothing) (Foo String) (Foo String))
> #<procedure>
>
> Surprisingly (Foo Integer) has changed to (Foo Nothing)! Is this a
> possible bug in the type system? Or, may be I'm missing something?
>
> Thanks!
>
> --
> 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.
