Polymorphism implementation sketch about dahlia HOT 1 OPEN

This is indeed a complex next step! I'm excited for it, and it's worth carefully considering how to design the semantics. Here are just a few notes to get us started.

At an extremely high level, I suggest we divide the effort (both design and implementation) into two phases:

1. Polymorphism without inference.
   • Defining a polymorphic function type would require explicit type parameters. For example, the syntax might look something like def foo[M: nat, N: nat](a: int[M bank N]). The parameters in square brackets are type-level parameters; the parameters in parentheses remain type-level, and their types can refer to type parameters.
   • Invoking a polymorphic function would require explicitly specifying its type parameters. The syntax might look like foo[10, 2](m).
   • In this phase, we'd need to define the abstract syntax for polymorphic types. I'd recommend taking inspiration from the appropriate formalism (i.e., System F): there would be explicit type-level abstractions. A type variable occurrence would refer to a specific type abstraction. These type abstractions could be either their own type AST node kind, or they could be folded in with function types (i.e., function types have both a list of type-level parameters and a list of value-level parameters).
2. Add inference.
   • Once we're happy with the correctness of the polymorphic language, but exhausted from typing all the parameters every time, now we add inference—and therefore the constraint generation.
   • In version 1.0, we should just ask the SMT solver to give us back a concrete assignment for the whole program. Rather than getting back a new set of constraints ourselves, the solver can just pick an arbitrary valuation that makes the program type-check.
   • Then, it would be a good subsequent challenge to get this to work in a compositional, intraprocedural way. That would probably involve enriching the language itself to include constraints along the lines of M % 4 == 0, which could be written explicitly in addition to being inferred.

from dahlia.