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

• partial type inference, and
• variance or polarized types,

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