search

RedPRL / cooltt

😎TT
http://www.redprl.org/
Apache License 2.0
217 stars 16 forks source link

🦆 Inductive Types #282

Open TOTBWF opened 3 years ago

TOTBWF commented 3 years ago

Basic Design + Syntax

The (rough) syntax for defining an inductive type is as follows:

data type-name (x1 : p1) (x2 : p2) ... : (y1 : i1) -> (y2 : i2) -> ... -> type where
| c1 : args -> type-name y1 y2 ...

This command will do a couple of things:

  1. Add datatype information (eliminator, constructor info, parameters, etc) to the current code-unit's datatype table.
  2. Add type-name to the current code-unit's namespace.

Constructors

Constructors pose a slight challenge. Namely, when we elaborate them we want to be in chk mode to make sure we can properly instantiate parameters, and they ought to be eta-long so that we can supply all the arguments simultaneously. Furthermore, if we don't add some sort of fancy renaming/disambiguation pass, we should probably add some sort of syntactic flag indicating that we are applying a constructor. To see why this is the case, consider how cons x xs will be parsed and subsequently elaborated. We will parse this as Ap(Ap(Var cons, Var x), Var xs), and then we will apply the Pi.apply tactic twice during elaboration, which will put us into syn mode when we try to resolve the cons. This means that we will be forced to annotate the type of the cons constructor, which is no good!

However, if this was parsed as Ctor "cons" [Var x, Var y], then we would be able to use our hypothetical Data.intro tactic, which let us remain in chk mode, and properly instantiate things like datatype parameters.

Eliminators

Eliminators are relatively straightforward. As we can syn the scrutinee, we can lookup the datatype in question in the datatype table, instantiate parameters + indexes, gather info about constructors, and then proceed as usual.

Datatype Table

Because we will often need to look up metadata about a datatype (for instance, constructor types when performing elimination, parameter types, etc), it makes sense to add a new table to a code unit for tracking this information. This should behave in a similar manner as the existing symbol_table. We might want to consider mucking with the Global type to track which table it ought to index into, but that's mostly a question of code aesthetics.

Notes

Having to syntactically disambiguate constructors is kind of ugly, and seems to hint at the idea that we may want some sort of renaming/disambiguation pass. This may also open the possibility of dot-notation for record projections, though that may still conflict with our very permissive naming rules. Food for thought!

favonia commented 3 years ago

I just want to express my unconditional approval of whatever designs based on the excellent choice of Unicode emojis.