On Friday, July 21, 2017 at 9:06:16 PM UTC+5:30, Ben Greenman wrote:
> Type inference is failing you again.
Yes, well, that seems to be a common theme whenever I hover around the these
type of areas which are uncommon but works perfectly fine in untyped Racket.
>
>
> 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))
Yes, that works fine. For my personal use it is good enough, but exporting that
function as a library would require every user to annotate the type whenever
they want to call it, even for very simple types - which is not a very good
experience for a typed language.
>
>
>
>
> I wouldn't call this a bug, but it's definitely a program that a better type
> inferencer should accept.
In other cases where type inference fails, the compiler bails out with an error
(even though that is a confusing one like `expected: (Seq a) given: (Seq
Integer)`). But here:
1. The inference did not fail but assumed it's Nothing just because I changed
the function signature from (-> a) to (-> a a). I can't understand why the
inference fails for this change. And on top of this,
2. The function type is clearly specified as (-> (Foo a) (Foo b) (Foo b)) and
it can unify a = Integer, b = String, from the first argument alone. So, even
though a is Integer, it still produces a = Nothing, without a compile error.
Integer =/= Nothing. Seems very close to a bug in the type deduction algorithm.
>
>
> On Fri, Jul 21, 2017 at 5:19 AM, Sourav Datta <soura...@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...@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.
