Re: [racket-users] A bug in the Typed Racket system?

[Sourav Datta]

Thanks for the clarification.

On 09-Aug-2017 3:29 AM, "Sam Tobin-Hochstadt"  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 
> 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 
> 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))
> >>
> >> #
> >>
> >>
> >>
> >> 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))
> >>
> >> #
> >>
> >>
> >>
> >> 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 

Re: [racket-users] A bug in the Typed Racket system?

[Sam Tobin-Hochstadt]

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  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  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))
>>
>> #
>>
>>
>>
>> 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))
>>
>> #
>>
>>
>>
>> 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 

Re: [racket-users] A bug in the Typed Racket system?

[Sourav Datta]

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  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))
> 
> #
> 
> 
> 
> 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))
> 
> #
> 
> 
> 
> 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.

Re: [racket-users] A bug in the Typed Racket system?

[Ben Greenman]

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  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))
> #
>
> 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))
> #
>
> 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.