Omega

Lambda Omega

Haskell implementation of Renardel de Lavalette's Simply Typed Lambda Calculus with type operators. It has STLC terms, a type-level abstraction (with application), kinding (with * and K => K kinds), and Natural numbers as an example of proper types.

This language formalises the notion of a type constructor by providing functions from types to types used by many functional languages. This is enabled by having two sorts of expressions of the form object/term:type and type:kind Additionally this language formalises the inclusion of type variables.

Prerequisites

You need Haskell, this compiles with GHC 8.2.2 at least (Stack resolver: lts-11.0).

To Build & Run

You can use cabal to build and run this, see this README, alternatively you can use vanilla ghc to build:

To compile and run do: ghc -O2 -o omega Main then run ./omega

Alternatively to use the GHCi Interpreter do: ghci Main then type main

In either case you get something like the following:

Welcome to the Omega REPL
Type some terms or press Enter to leave.
>

Note: When run in GHCi, you don't have the luxury of escaped characters, backspace, delete etc... Compile it using GHC if you need this.

Examples

Where you can then have some fun, try these examples:

• z This is zero, in Peano style.
• s (s (s z)) This is 3 in Peano style.
• \x:Nat. x This is the identity function on Nats.
• \x:(\A::*.A) Nat.x This is the identity function except with type-level abstraction and application. The type-level abstraction accepts proper types (kinded *) such as Nat, and returns a type (of kind *) such that the resultant kind is * => *. The type-level application applies Nat to the abstraction and returns Nat.

The parser is also smart enough to recognise λ, so you can copy and paste from the output:

>   \x:Nat. x
=   λx:Nat.x
>   λx:Nat.x
=   λx:Nat.x

> denotes the REPL waiting for input, = means no reductions occurred (it's the same term), ~> denotes one reduction, and ~>* denotes 0 or more reductions (although in practice this is 1 or more due to =).

There is also a reduction tracer, which should print each reduction step. prefix any string with ' in order to see the reductions:

>   '(\n:Nat.(\m:Nat.m) ((\x:Nat.x) n)) z
~>  (λm:Nat.m) ((λx:Nat.x) z)
~>  (λx:Nat.x) z
~>  z

Reduction occurs at both the term level and type level (inside term-level abstractions as this is where the types are). Here's a function that reduces only at the type level:

>   '\x:(\P::(*=>*=>*)=>*.P (\A::*.\B::*.A)) ((\A::*.\B::*.\P::*=>*=>*.P A B) Nat Nat).x
~>  λx:(λA::*.λB::*.λP::*=>*=>*.P A B) Nat Nat (λA::*.λB::*.A).x
~>  λx:(λB::*.λP::*=>*=>*.P Nat B) Nat (λA::*.λB::*.A).x
~>  λx:(λP::*=>*=>*.P Nat Nat) (λA::*.λB::*.A).x
~>  λx:(λA::*.λB::*.A) Nat Nat.x
~>  λx:(λB::*.Nat) Nat.x
~>  λx:Nat.x

There is also a typing mechanism, which should display the type or fail as usual.

>   t\x:(\A::*.A) Nat.x
(λA::*.A) Nat->(λA::*.A) Nat
>   t\x:(\A::*.A).x
Cannot Type Term: \x:(\A::*.A).x

Note: The above is untypeable as λA::*.A is a type operator, such that it takes a type and returns a type (not a term). See the semantics for details on why.

Note: if you provide a non-normalizing term, the type checker will fail and reduction will not occur.

You can save variables for the life of the program with a let expression. Any time a saved variable appears in a term, it will be substituted for the saved term:

>   let three = s (s (s z))
Saved term: s (s (s z))
>   let addone = \m:Nat. s m
Saved term: λm:Nat.s m
>   addone three
~>* s (s (s (s z)))

Note: Consequently let and = are keywords, and so you cannot name variables with these.

Note: We include introduction rules for Nats to show how kinding works for proper types. We do not include Nat eliminators however as the focus is on type operators. Use the calculus with this in mind, like the next example.

Additionally we have type level lett statements that allow you to define and use types:

>   lett PAIR = \A::*.\B::*.\P::*=>*=>*.P A B
Saved type: λA::*.λB::*.λP::*=>*=>*.P A B
>   lett FST = \P::(*=>*=>*)=>*.P (\A::*.\B::*.A)
Saved type: λP::(*=>*=>*)=>*.P (λA::*.λB::*.A)
>   \x:FST (PAIR Nat Nat).x
~>* λx:Nat.x

This makes it easier to define both terms and types. lett is also a keyword.

Syntax

We base the language on the BNF for the typed calculus:

However we adopt standard bracketing conventions to eliminate ambiguity in the parser. Concretely, the parser implements the non-ambiguous grammar as follows:

For terms:

for types:

and for kinds (equivalent to the parser for O and T->T in STLC):

Some notes about the syntax:

• The above syntax only covers the core calculus, and not the repl extensions (such as let bindings above). The extensions are simply added on in the repl.
• Term and type variables are strings (excluding numbers), as this is isomorphic to a whiteboard treatment and hence the most familiar. Term variables are lower case whereas type variables are upper case.
• All term level syntax is identical to STLC, however the valid types are different.
• Types are variables A,B,C,..., type operators/abstractions \X::K.T, applications A B, or arrows A -> B. There is also the Nat type.
• Omega formally introduces type variables A, B, C... which until now are used informally for convenience. STLC does not have variables for this reason. Some treatments of STLC range over base types A,B,C,... which implicitly assumes these are proper types.
• Type arrows associate to the right so that X -> Y -> Z is the same as X -> (Y -> Z) but not ((X -> Y) -> Z). The same is true at the kind level * => * => * is the same as * => (* => *) but not (* => *) => *.
• For both term and type abstractions, nested terms don't need brackets: \x:Nat.\y:Nat. y unless enforcing application on the right. Similarly at both levels whitespace does not matter (\x:Nat. x) unless it is between application where you need at least one space.
• To quit use Ctrl+C or whatever your machine uses to interrupt computations.

Semantics

The semantics implements beta-reduction on terms and alpha-equivalence as the Eq instance of OTerm. The semantics are the same as the untyped calculus with the addition of types and kinds. We reformulate the semantics as typing judgements:

for term-level variables:

for term-level abstractions, with the added constraint that the variable in the abstraction has a proper type (*):

and term-level application:

for zero and succ:

and the reduction relation adopted from the untyped theory (with types added in the abstraction):

We now have abstraction, application and type-variables at the type level with 'types of types' known as kinds. This means the semantics of types mirror term-level semantics of STLC but one level up:

For type-variables:

For type-abstraction (known as a type operator):

For type-application:

For the existing type arrow (now with constraints that both sides of the arrow must have proper types):

Next, Nats are a proper type:

Lastly, we have type-level beta reduction, identical to STLC reduction but for types:

• This means the typing context now also contains types. The phrase X :: K means X is has kind K. We do not implement Agda style type hierarchies here.
• There is the additional constraint that any term abstractions must take a term of proper type. This prevents nonsensical or partially-applied types terms such as Pair Nat _.
• This reflects the principle that any typeable term has a kindable type.
• The base calculus on its own does not have any proper types (such as Nat, Bool or Unit) and so it is unusable as no terms can be introduced. To demonstrate proper types, we add the proper type Nat, with constructors z and s.
• Type abstractions can be of any kind permitted by Omega, however the resultant type must be proper for it to be accepted by a term-level abstraction. This prevents nonsensical terms and types like z (s z) typed Nat Nat.
• Type-level application is identical to term-level application in STLC, except it makes uses of the kinding arrow => from types to types.
• Arrows have the constraint that both the domain and co-domain must be proper types. This prevents non-nonsensical types such as Pair Nat _ -> Nat.
• The term-level calculus is identical to STLC.
• Omega provides a mean to define types from types. By using abstraction and application to form types from types. Type operators themselves do not define terms (there is no term of type \X::*.X) but are used to form proper types which do have terms: (\X::*.X) Nat ~>* Nat which has term z.
• System F provides a means to form terms from a type. By providing a type at the term level we can form terms parametrised by that type.
• This implementation follows a small-step operational semantics and Berendregt's variable convention (see substitution in Omega.hs).
• Reductions include the one-step reduction (see reduce1 in Omega.hs), the many-step reduction (see reduce in Omega.hs). additionally there is a one-step type-level reduction (see reduce1T in Omega.hs).

Other Implementation Details

• Omega.hs contains the Haskell implementation of the calculus, including substitution, reduction, and other useful things.
• Parser.hs contains the monadic parser combinators needed to parse input strings into typed-term ASTs for the calculus.
• Repl.hs contains a simple read-eval-print loop which hooks into main, and into the parser.
• Main.hs is needed for GHC to compile without any flags, it also invokes the repl.

For contributions, see the project to-do list or submit a PR with something you think it needs.

Work initially documented here.