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 < ***@***.***> 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<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? — You are receiving this because you were assigned. Reply to this email directly, view it on GitHub <#50 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEqTwDf4Io8HmG3sVXqbGGuklLB0WpFxks5rU9a2gaJpZM4LqhAg> .