Brent Yorgey

I have sat down to work on this several times and always end up getting bogged down in details trying to figure out how it is going to work. Definitely...

Some ideas: 1. Add type lambdas & type applications to the language. Actually, this might not require any changes at all: types can already be embedded in terms (because of...

I am not sure whether this is still necessary. #160 was the original motivation and it is now closed because it's fixed. Is there anything else where we need a...

Probably a helpful thing to do as a start would be to try several simple examples and just imagine / write out what an evaluation trace might look like. For...

Maybe the right way to do this is to make a CEK machine for the surface language, and pretty-print CEK states by nesting evaluation contexts with the focused subexpression highlighted....

Some preliminary code for this is in the `multitype` branch, https://github.com/disco-lang/disco/tree/multitype . A comment on the commit there explains what still needs to be done: https://github.com/disco-lang/disco/commit/f1ee1415bd8a9e5cc68ed640c800c69d6f1b24ad , reproduced below for...

Note, simply finding polarities of variables in a type is not by itself enough. We also need to deal with the many unification variables generated during typechecking & constraint generation....

Another option would be to enable the list cons operator via a language extension, but always allow building lists via more primitive sum and product types.

I think this is really important pedagogically, but after some thought I can't figure out how to make it work. We could simply make a synonym `type List(a) = Unit...

So `2f(n)` needs to parse as `2 * (f(n))` because function application has higher precedence than multiplication; however, the problem is that since function application and multiplication are both left-associative,...