types for Asumu

[Matthias Felleisen]

Why does this

> (compose (λ (x) x) (λ #:forall (a) ({x : a}) x))

have this type:

> - : (-> Nothing Any)

Thanks -- Matthias

[Sam Tobin-Hochstadt]

I think something problematic is happening with type inference here,
and better types could be picked. Right now, Typed Racket is doing
this:

(compose (λ (x) x) (inst (λ #:forall (a) ({x : a}) x) Nothing))

when it should probably do

(compose (λ (x) x) (inst (λ #:forall (a) ({x : a}) x) Any))

However, using polymorphic arguments (such as your second function)
to polymorphic functions (such as `compose`) in general won't produce
the results you want, and I recommend writing the instantiation you
want explicitly.

Sam

> --
> You received this message because you are subscribed to the Google Groups "Racket Developers" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-dev+...@googlegroups.com.
> To post to this group, send email to racke...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/7E7C582D-7066-4073-AAFD-9B6CA99F1F1E%40ccs.neu.edu.
> For more options, visit https://groups.google.com/d/optout.

[Matthias Felleisen]

On Sep 29, 2015, at 3:25 PM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote:

> I think something problematic is happening with type inference here,
> and better types could be picked. Right now, Typed Racket is doing
> this:
>
> (compose (λ (x) x) (inst (λ #:forall (a) ({x : a}) x) Nothing))
>
> when it should probably do
>
> (compose (λ (x) x) (inst (λ #:forall (a) ({x : a}) x) Any))
>
> However, using polymorphic arguments (such as your second function)
> to polymorphic functions (such as `compose`) in general won't produce
> the results you want, and I recommend writing the instantiation you
> want explicitly.

Well yes, that's where I started with inst. The Nothing told me I was on the wrong track with inst.

What you might be saying is 'use inst for compose'.

-- Matthias

[Sam Tobin-Hochstadt]

What use of `inst` produced `Nothing`?

Sam

On Tue, Sep 29, 2015 at 3:46 PM, Matthias Felleisen
<matt...@ccs.neu.edu> wrote:
>
> On Sep 29, 2015, at 3:25 PM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote:
>

>> I think something problematic is happening with type inference here,
>> and better types could be picked. Right now, Typed Racket is doing
>> this:
>>
>> (compose (λ (x) x) (inst (λ #:forall (a) ({x : a}) x) Nothing))
>>
>> when it should probably do
>>
>> (compose (λ (x) x) (inst (λ #:forall (a) ({x : a}) x) Any))
>>
>> However, using polymorphic arguments (such as your second function)
>> to polymorphic functions (such as `compose`) in general won't produce
>> the results you want, and I recommend writing the instantiation you
>> want explicitly.
>
>
>

> Well yes, that's where I started with inst. The Nothing told me I was on the wrong track with inst.
>
> What you might be saying is 'use inst for compose'.
>
> -- Matthias
>
>
>
>
>
>>

[Matthias Felleisen]

The inst inside the expression.

Is this expression typable at the moment?

[Sam Tobin-Hochstadt]

Your original program does not use `inst`, so I'm not sure what you're
referring to.

The expression is certainly typable -- the second program I gave
typechecks at `(-> Any Any)`.

Sam

On Tue, Sep 29, 2015 at 4:32 PM, Matthias Felleisen
<matt...@ccs.neu.edu> wrote:
>
> The inst inside the expression.
>
> Is this expression typable at the moment?
>
>
>

[Ian Johnson]

The instantiation of (inst compose Nothing Any Any) gives (-> Nothing Any).

If you give Nothing Nothing Any, then the type error refers to some gensym, heh.

-Ian

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/CAK%3DHD%2BY9VNCsvx81nHpXcevEW0PmMHD%3DcZxdbFBsmrSEiCiZ2g%40mail.gmail.com.