ct-gradual-typing / Papers

The Combination of Dynamic and Static Typing from a Categorical Perspective
10 stars 0 forks source link

Parsing error with box and unbox #31

Closed michaelto20 closed 7 years ago

michaelto20 commented 7 years ago

Currently, this won't typecheck anymore: \(m:?).\(f:? -> Nat).box<Nat> (f m)

It should typecheck to: ? -> Nat -> (? -> Nat) -> ?

It fails to parse in anything after box<T> or unbox<T>.

heades commented 7 years ago

Looks like you have some debugging to do. :-)

heades commented 7 years ago

All kidding aside, you should try and see if you can find the problem.

heades commented 7 years ago

Lastly, that parses just fine on my computer:

*Parser> parseTest expr "\\(m:?).\\(f:? -> Nat).box<Nat> (f m)"
Fun U (bind m(Fun (Arr U Nat) (bind f(Box Nat))))
*Parser> 
michaelto20 commented 7 years ago

Oh definitely. That'll be for tomorrow, the wife is telling me to come to bed!

On Mon, Dec 26, 2016 at 9:52 PM, Harley D. Eades III < notifications@github.com> wrote:

All kidding aside, you should try and see if you can find the problem.

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

michaelto20 commented 7 years ago

Are you running that on the master branch or loadfile branch?

On Mon, Dec 26, 2016 at 9:54 PM, Harley D. Eades III < notifications@github.com> wrote:

Lastly, that parses just fine on my computer:

Parser> parseTest expr "\(m:?).\(f:? -> Nat).box (f m)" Fun U (bind m(Fun (Arr U Nat) (bind f(Box Nat)))) Parser>

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

heades commented 7 years ago

The loadfile branch. But, I am running the parser directly, but when I try it from the repl I get an error.

heades commented 7 years ago

So there is a problem with the repl.

heades commented 7 years ago

Go to bed, and try to see what you can find out later.

michaelto20 commented 7 years ago

Thanks for fixing this!