TypeChecking with unbox

[michaelto20]

I ran across this example and I don't think this should typecheck.

Grady> :t \(m:Nat) -> unbox<Nat> m 
Nat -> Nat

It's my understanding we should not be able to unbox a Nat? Is that correct?

[heades]

Actually, that is not a bug. In Surface Grady -- that is, not using Core Grady -- then that program is perfectly valid. It uses the dynamic typing fragment of the gradual type system.

By unbox<Nat> m you are telling Grady to cast m to type ?, and then unbox it. Here is the same program after cast insertion:

\(m:Nat).(unbox<Nat>) ((\(y:Nat).(\(y:?).y) ((box<Nat>) y)) m)

You can see that it knows that m is of type Nat, but then boxes it up, and the unboxes it right away. Thus, your program is equivalent to the following:

\(m:Nat).m

In fact, we can run it:

Grady> (\(m:Nat) -> unbox<Nat> m) 3
3
Grady> 

Now if you try and type the same program directly in the core, then it fails:

Core Grady> :t (\(m:Nat) -> unbox<Nat> m)
TypeMismatch Nat U
Core Grady> 

Does that make sense?

[michaelto20]

Yes that makes sense. I just wanted to make sure that was the expected behavior.

Thanks.

Michael

On Sun, Jan 22, 2017 at 5:22 PM, Harley D. Eades III < notifications@github.com> wrote:

Actually, that is not a bug. In Surface Grady -- that is not using Core Grady -- then that programs is perfectly valid. It uses the dynamic typing fragment of the gradual type system.

By unbox m you are telling Grady to cast m to type ?, and then unbox it. Here is the same program after cast insertion:

(m:Nat).(unbox) (((y:Nat).((y:?).y) ((box) y)) m)

You can see that it knows that m is of type Nat, but then boxes it up, and the unboxes it right away. Thus, your program is equivalent to the following:

(m:Nat).m

In fact, we can run it:

Grady> ((m:Nat) -> unbox m) 3 3 Grady>

Now if you try and type the same program directly in the core, then it fails:

Core Grady> :t ((m:Nat) -> unbox m) TypeMismatch Nat U Core Grady>

Does that make sense?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/heades/gradual-typing/issues/50#issuecomment-274364761, or mute the thread https://github.com/notifications/unsubscribe-auth/AEqTwDf4Io8HmG3sVXqbGGuklLB0WpFxks5rU9a2gaJpZM4LqhAg .