search

disco-lang / disco

Functional teaching language for use in a discrete mathematics course
Other
162 stars 23 forks source link

Pass types at runtime as necessary, or determine it is not needed #177

Open byorgey opened 5 years ago

byorgey commented 5 years ago

Sometimes we need to know type information at runtime, e.g. to do comparison. The current approach is restrictive and broken. See #160.

byorgey commented 4 years ago

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 needs someone with a high amount of type-system-fu...

byorgey commented 4 years ago

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 e.g. enumerate and count).

  2. When we typecheck a top-level polymorphic declaration, we compile it to something with an extra type lambda for each type variable with one or more qualifiers.

  3. When type checking an application of such a polymorphic top-level thing, we have to figure out what types its type variables get unified with, and pass them as parameters. Note this might be tricky since the types unified with the type variables might themselves be type variables coming from a bigger enclosing polymorphic definition, so we have to figure out the right way to refer to them at runtime.

There has got to be some good information/examples/tutorials/papers about doing this kind of thing somewhere... Possibly relevant: https://www.sciencedirect.com/science/article/pii/S1571066105051376

byorgey commented 2 years ago

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 type at runtime? A next step would be to look and see where Types are still stored in some Core or Op thing, and whether we can get it to blow up by containing a type variable or something like that.