Polymorphism implementation sketch
Opened this issue · 1 comments
rachitnigam commented
With functions in place, we can start thinking about polymorphism.
Implementation sketch
- Create AST where
EVar
can either be anId
or aHole
. AHole
is a type parameter.- For example,
def foo(a: int[M bank N])
parses toFunc(foo, List(a -> TArray((EVar(M), EVar(N))))
- Use scala
trait
to create an AST parameterized on the type ofId
.
- For example,
- 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
andCPar
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
- Constraints are generated on
- 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 wantM % 4 = 0
- Once a function is done, add the function def with bounds into a simple environment.
- Instead of concrete assignment, we want a bound. So instead of
- 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 commented
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:
- 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).
- Defining a polymorphic function type would require explicit type parameters. For example, the syntax might look something like
- 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.