ct-gradual-typing / Papers

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

Feedback needed #54

Closed michaelto20 closed 7 years ago

michaelto20 commented 7 years ago

Can you take a look at the work I most recently pushed to the M_branch? Specifically, when I'm testing the evaluator I don't always get back what I expect.

For example, this looks great (this was after loading the ChurchEncodings.gry file):

Core Grady> two s z
s (s z)

However, the output of this was unexpected:

Core Grady> add (one s z) (one s z) s z
((s z) s) (((((\(s:? -> ?).\(z:?).s z) s) z) s) z)

I was expecting: s (s z)

Is it working right, but my expectation is off? If however this behavior is off, do you have anywhere you could point me to track down the issue?

Also I know we had talked about updating the function insertCasts with the context similar to Typechecking. However, the insertCasts function is never used in the CoreRepl like it is in the Gradual Repl. Should it be?