Polymorphism implementation sketch

[rachitnigam]

With functions in place, we can start thinking about polymorphism.

Implementation sketch

• Create AST where EVar can either be an Id or a Hole. A Hole is a type parameter.
  • For example, def foo(a: int[M bank N]) parses to Func(foo, List(a -> TArray((EVar(M), EVar(N))))
  • Use scala trait to create an AST parameterized on the type of Id.
• Redefine the parser to allow for holes to exist in:
  • Array types: Both dimension and banking factor
  • Ranges: Both range end and unrolling factor.
• Write a constrain generator that outputs SMT-lib
  • Constraints are generated on EAA.
  • Encode CSeq and CPar constraints in a preamble
  • Note: It seems some type checking and capability checking might be useful at this point, but I don't want to create another type checker in here.
  • TODO: probably missing some stuff
• Write a deparser for SMT-lib that extracts the model and remaps it to symbols.
• Walk through each function definition in order and resolve the bounds on each type parameter.
  • Instead of concrete assignment, we want a bound. So instead of M = 24, we want M % 4 = 0
  • Once a function is done, add the function def with bounds into a simple environment.
• For function applications with abstract parameters, foo[M, N](a, b)
  • add the bounds from the function definition into the constraint formula.
  • When the solver returns a concrete model, add an instantiation of foo with these concrete values to a Set of concrete function instantiations.
• Once all function definitions are checked, remove all abstract functions and add concrete instantiations of the function into the AST.
• Replace abstract function calls with calls to the concrete functions.
• Send to the type checker!

Even at a high level, this proposal implies 3-4 days of concerted hacking.

[sampsyo]

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.