Fωμ type checker and compiler
A type checker and compiler (*, *) for Fωμ restricted to non-nested types (*). This Fωμ variant has
- structural sum and product types (*, *),
- join and meet type operators (*),
- equirecursive types (*, *),
- higher-kinded types (*), including type level lambdas and kind inference (*),
- impredicative universal and existential types (*),
- structural subtyping (*, *),
- decidable type checking, and
- phase separation.
These features make Fωμ relatively well-behaved as well as expressive (*, *, *) and also allow a compiler to make good use of untyped compilation targets (*, *) such as JavaScript.
Although this is ultimately really intended to serve as an intermediate language or elaboration target, the implementation provides both a fairly minimalistic AST and a somewhat more programmer friendly syntax with some convenience features that are elaborated into the AST.
The implementation also supports dividing a program into multiple files via an
import mechanism for types and values and an include mechanism for type
definitions. Value imports can be separately compiled. HTTP URLs and relative
paths are allowed as references.
Please note that this is a hobby project and still very much Work-in-Progress with tons of missing features, such as
and probably more bugs than one could imagine.
Next steps
- Try examples in the online playground.
- See the syntax summary.
- See project board.
Background
This Fωμ variant is basically a generalization of the type system for Fωμ*,
that is Fωμ restricted to first-order recursive types of kind *, described
in the article
- System F-omega with Equirecursive Types for Datatype-generic Programming
- by Yufei Cai, Paolo G. Giarrusso, and Klaus Ostermann.
While Fωμ* is powerful enough to express regular datatypes, it requires type
parameters to be hoisted outside of the μ. For example, the list type
μlist.λα.opt (α, list α)
needs to be rewritten as
λα.μlist_1.opt (α, list_1)
Both of the above types are allowed by this generalized system and are also considered equivalent as shown in this example.
In this generalized system, nested types are not allowed. For example,
μnested.λα.(α, nested (α, α))
is disallowed due to the argument (α, α) as demonstrated in this
example.
Disallowing nested types is sufficient to keep the number of distinct subtrees finite in the infinite expansions of recursive types and to keep type equivalence decidable.
Fortunately, as conjectured in
- Do we need nested datatypes?
- by Stephanie Weirich
many uses of nested datatypes can also be encoded using e.g. GADTs and Fωμ is powerful enough to encode many GADTs. Consider, however, the higher-kinded nested type
λf.μloop.λx.(x, loop (f x))
that, when given an f and an x, would expand to the infinite tree
(x,
(f x,
(f (f x),
(f (f (f x)),
...))))
illustrating a process of unbounded computation where x could be higher-rank
and encode arbitrary data. It would seem that this kind of recursion pattern
would allow simulating arbitrary computations, which would seem to make type
equality undecidable. Thus, it would seem that disallowing nested types is not
only sufficient, but also necessary to keep type equivalence decidable in the
general case.
Why?
Greg Morrisett has called Fω "the workhorse of modern compilers". Fωμ adds equirecursive types to Fω bringing it closer to practical programming languages.
Typed λ-calculi, and System F in particular, are popular elaboration targets for programming languages. Here are a couple of papers using such an approach:
- 1ML — core and modules united
- Andreas Rossberg
- Elaborating Intersection and Union Types
- Jana Dunfield
Perhaps a practical System Fωμ implementation could serve as a reusable building block or as a forkable boilerplate when exploring such programming language designs.
Here are a couple of papers about using a Fωμ variant as an IR:
- Unraveling Recursion: Compiling an IR with Recursion to System F
- Michael Peyton Jones, Vasilis Gkoumas, Roman Kireev, Kenneth MacKenzie, Chad Nester, and Philip Wadler
- System F in Agda, for fun and profit
- James Chapman, Roman Kireev, Chad Nester, and Philip Wadler
System Fω might also be a good language for teaching functional programming and make an interesting object of study on its own:
- Lambda: the ultimate sublanguage (experience report)
- Jeremy Yallop, Leo White
System Fω interpreter for use in Advanced Functional Programming course
- Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
- Matt Brown, Jens Palsberg