Thanks for the clarification.
On 09-Aug-2017 3:29 AM, "Sam Tobin-Hochstadt" <sa...@cs.indiana.edu> wrote:
> The reason that Typed Racket chooses the istantiation `Nothing` here
> is that because `a` is used in both a positive and negative position
> (both as an input and an output) in the type of the `val` field,
> there's no way to pick a "best" choice for `a`. `(Foo Integer)` is not
> a subtype of `(Foo Any)`, for example. Furthermore, whatever Typed
> Racket chooses for `a`, the function application will type check.
> Typed Racket therefore picks the smallest type that works, which is
> `Nothing`.
>
> This actually tells you more about your second program -- in
> particular, you can't ever call the `val` function from the `(Foo a)`,
> because you can't construct a value of type `a`.
>
> Sam
>
> On Fri, Jul 21, 2017 at 1:40 PM, Sourav Datta <soura.ja...@gmail.com>
> wrote:
> > 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.
>
--
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.
