Skip to content

Attempt some simple polymorphism

E. Rivas requested to merge er433/polymorphism-expression into dev

This MR attempts to do some amount of polymorphism, only on the pass 10-checking (not inference).

For CameLIGO, where type parameters can be introduced by the parser, it modifies the pass 4-tree abstraction:

  • Tree abstraction: type parameters are abstracted using a new T_for_all in a Declaration_constant or a E_let_in. For example, the K combinator can be presented as let k (type a b) (x : a) (_y : b) : a = x.

For JsLIGO, ReasonLIGO, and PascaLIGO, type variables starting with _ are quantified universally. For example, the K combinator in JsLIGO can be presented as let k : (p : [_a, _b]) => _a = ([x, _y] : [_a, _b]) => x.

Then, the change operates in two passes: 10-checking and 11-self_ast_typed:

  • Checking: the main modification is in application. When we apply an expression with type T_for_all _, then it will try to use the information of the applied parameters to "infer" the type of the abstracted variables. The type checker "saves" this information in the expression, using a new type application construct E_type_inst. E.g. let x : int = k 4 "hello" it will be modified by type checking to let x : int = k@{int}@{string} 4 "hello".

  • Self ast typed: a new pass doing monomorphisation is introduced. It goes in backwards direction, it saves type instantiations (E_type_inst) as the pass is applied, when a declaration is introduced it's checked if there's any type instantiation corresponding to it, and in that case, a new monomorphic version of the declaration is introduced. E.g.:

let k (type a b) (x : a) (_y : b) : a = x
let x : int = k@{int}@{string} 4 "hello"

will start by processing x, and save that k is instantiated with int, string, int (arguments and final type), and replace the identifier k in the call with a new id k_#1 that's also saved. When processing k, it will check in instantiations, and find that k is instantiated with int, string, int, so it will create a new instance of k with the name of the saved id: let k_#1 (x : int) (_y : string) : int = x. In the end, you get the program:

let k_#1 (x : int) (_y : string) : int = x
let x : int = k_#1 4 "hello"

which is ready to be compiled as no polymorphism is present anymore.

  • has a changelog entry
Edited by E. Rivas

Merge request reports