search

CategoricalData / hydra

Transformations transformed
Apache License 2.0
72 stars 10 forks source link

Replace type schemes with forall types #76

Closed joshsh closed 2 months ago

joshsh commented 1 year ago

Hydra uses Hindley-Milner type inference, but its actual type grammar has moved on from Hindley-Milner to System F. Rather than inferring type schemes, Hydra must now infer forall types -- the main difference being the ordering of type variables. Since the algorithm is still Hindley-Milner, forall types will only be produced at the top level; they will be eliminated from subterms. Previously, all elements (top-level terms with names) had to be manually annotated with types anyway, so there was no need to get forall types right. Now it should be possible to omit all type annotations except in the case of cycles.

joshsh commented 7 months ago

Done in #103. Possibly superseded by #118 (which only uses type schemes internally, for STLC to F).

joshsh commented 2 months ago

We are actually going back to type schemes for now. Again, the overriding concern right now is translatability, although symmetry between the term grammar and the type grammar is still a concern as well. Every let-binding is potentially annotated with a type scheme, and type variables are not introduced anywhere else.