SOL

SOL

Haskell implementation on John Mitchell and Gordon Plotkin's SOL. It has the features of System F but with existential types made explicit.

We have added Natural numbers, Booleans, records, product, and sum (disjoint union) types to make this calculus slightly more interesting as Mitchell and Plotkin do. These types are not necessary for SOL, and others have presented existentials with just STLC, however we use this presentation to make clear their relation with parametricity.

This strongly normalising calculus makes it easier to see how abstract data types, objects, and (simplistic) modules can arise as a special case of parametric polymorphism.

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 sol Main then run ./sol

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

In either case you get something like the following:

Welcome to the SOL 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:

• LX.\x:X.x where L stands for second-order abstraction. See if you can see why \x:X.x won't type check.
• (LX. \x:X.x) [PX.(X->X)->X->X] the identity function for Church natural numbers.
• LX.\f:X->X.\x:X.x this is zero in Church numeral format.
• 2 Nats are supported.
• if ((λb:Bool.b) true) then 0 else 1 booleans are supported.
• LX.{f=\x:X.x, u=2} This is a record with a universally quantified function and a constant.
• LB.\r:{b:B}.r.b This is a function that takes a record and accesses field b.
• case (inl 1: Nat + Bool) (\x:Nat.x) (\b:Bool.1)
• λn:∀X.(X->X)->X->X.ΛY.λf:Y->Y.λy:Y.f (n [Y] f y) this is succ in Church Numeral format.
• fst (1,2), snd (1,2) are left and right projections on tuples.
• pack {Nat, 4} as EX.X existential quantification where E stands for 'there exists'.
• pack {Nat, {init=0, set=\x:Nat.x}} as EX.{init:X, set:X->X} packs the record up as an existentially quantified type X with operations init and set.
• unpack {X,body} = foo in body.f is the means to import an existentially quantified foo as variable body and substitute instances of the quantified type X in the body of the unpack statement. In this case body is a record that contains a field f.

Note: ∀ is the second-order product type, ∃ is existential quantification, Λ is second-order abstraction and [X] is the type variable X. Alternatively typed as P, E L, and [X] respectively.

The parser is smart enough to recognise λ, ∀ , ∃, and Λ; so you can copy and paste from the output:

Welcome to the System F REPL
Type some terms or press Enter to leave.
>   LX.\x:X.x
=   ΛX.λx:X.x
>   ΛX.λx:X.x
=   ΛX.λx:X.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:∀X.(X->X)->X->X.ΛY.λf:Y->Y.λy:Y.f (n [Y] f y)) (LX.\f:X->X.\x:X.x)
~>  ΛY.λf:Y->Y.λy:Y.f ((ΛX.λf:X->X.λx:X.x) [Y] f y)
~>  ΛY.λf:Y->Y.λy:Y.f ((λf:Y->Y.λx:Y.x) f y)
~>  ΛY.λf:Y->Y.λy:Y.f ((λx:Y.x) y)
~>  ΛY.λf:Y->Y.λy:Y.f y

Note: this is succ zero (or one) in Church numeral format

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

>   tpack {Nat, {init=0, set=\x:Nat.x}} as EX.{init:X, set:X->X}
∃X.{init:X, set:X->X}
>   tLX.\x:X. x
∀X.X->X
>   unpack {B,b} = (pack {Bool, \b:Bool.b} as EX.X->X) in b true
Cannot Type Term: unpack {"b", "B"} = pack {Bool, λb:Bool.b} as ∃X.X->X in b true

where ∀Y.(Y->Y)->Y->Y is equivalent to the System F/SOL type for Nats.

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

You can save terms 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 foo = pack {Nat, {init=0, set=\x:Nat.x}} as EX.{init:X, set:X->X}
Saved term: pack {Nat, {init=0, set=λx:Nat.x}} as ∃X.{init:X, set:X->X}
>   unpack {X,body} = foo in body
~>* {init=0, set=λx:Nat.x}
>   unpack {X,body} = foo in body.init
~>* 0

Note: Consequently let and = are keywords, and so you cannot name variables with these. Additionally L, [, ], and P, E, pack, unpack, true, false, fst, snd, inl, inr, case, *, +, Nat, Bool, {, }, as, (, ), if, then, else and in are keywords in SOL.

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

>   lett REGISTER = EX.{init:X, set:X->X}
Saved type: ∃X.{init:X, set:X->X}
>   let reg = pack {Nat, {init=0, set=λx:Nat.x}} as REGISTER
Saved term: pack {Nat, {init=0, set=λx:Nat.x}} as ∃X.{init:X, set:X->X}
>   unpack {R,register} = reg in register.init
~>* 0

This makes it easier to define both terms and types, but does not allow type level application (See Omega). 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 for terms as follows:

and types:

with term variables/primitives:

and type variables:

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.
• Variables are strings (excluding numbers), as this is isomorphic to a whiteboard treatment and hence the most familiar.
• Natural numbers are positive of the form 1, 2, 3 etc...
• Introduce booleans as true or false and eliminate them using if expressions. if expressions take an expression of type Bool and two sub-expressions of the same type.
• Products are 2-element pairs like in Haskell. You form products like (x, y) and access each element using fst (or π1) and snd (or π2).
• Sums are 2-element co-pairs, formed with either inl x:A or inr y:B (assuming either x:A or y:B is in scope). case s f g does case analysis on s, passing the result to the function f if s was inl or g if inr.
• To construct terms using case, use space to apply arguments. for instance, case s f c applies s to case, which then applies f to the case s and g to case s f etc...
• Records are generalised products formed as comma-separated sequence of assignments of terms to labels t=v, nested inside curly braces {u=1, idnat=\a:Nat.a}. Record types are comma-separated assignments of typings to labels t:v, nested inside curly braces (such as {1:Nat, f:Nat->Nat}).
• Types are uppercase strings as they must be distinct from term variables.
• You can introduce a universal type with Λ or L much like you would use a function abstraction.
• You can introduce existential types with the pack {T1,t} as T2 construct. This construct takes a concrete type T1 like Nat, a term t, and an existential type T2.
• Products have the highest precedence, followed by sums, arrows, and then all other types.
• Types are either type variables, abstractions, or nested arrow types: T -> T. Arrows associate to the right so that T -> T -> T is the same as T -> (T -> T) but not ((T -> T) -> T). The product binds weaker than arrows, so ∀X.X->X is the same as ∀X.(X->X).
• Nested terms don't need brackets: LX.LY.\x:X.\y:Y. y unless enforcing application on the right. Whitespace does not matter LX.\x:X. 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 SOLTerm. The semantics are the same as SystemF with the addition of existential quantification over types, nats, bools, records, sums, and products. We reformulate the semantics as typing judgements:

for variables (adopted from STLC):

for abstractions (adopted from STLC):

and application (adopted from STLC):

and the reduction relation (adopted from STLC):

and special introduction, elimination, and reduction rules for universal types:

We have special introduction, elimination and reduction rules for products:

for sums:

Next, there is a special elimination rule for records:

with sensible structural (internal) reduction rules for terms inside records. Lastly we have rules for record projections:

We have standard rules for Nats, Booleans, and if statements:

Finally, we have special introduction and elimination rules for existentials:

As well as sensible reduction rules under pack/unpack statements.

• This means the typing context now also contains types, and types occur in terms. The phrase X Type means X is a type. We do not implement Agda style type hierarchies here.
• Variables, abstraction, sums, products, booleans, and Nats follow semantics that are fairly standard in the literature.
• Records are typeable only if all of their subterms are typeable and all of the labels are unique. We leverage the STLC typing rules and the subtyping relation to ensure record fields are typeable.
• Projections are typeable only if it is applied to a term which is a well-typed record and the projection label (x in {x=2}.x) explicitly matches a label in that record.
• The pack statement enables you to package up a witness type T1 with a term t. The witness type here is known as the hidden representation type which must be provided as the type checker cannot infer the type of an existential in general. For instance pack {Nat, {z=\x:Nat.x}} as EX.{z:X->X} has existential type ∃X.{z:X->X} but also ∃X.{z:Nat->X}. We can then pass this into a function as a 'module' of sorts, where any term with a witness type to a given interface can be used.
• We can use existential types by unpacking them. This construct takes an existential type, binding them to the type variable X and a term variable x. We may then use x in the body of the expression. However, the representation type is hidden during typechecking so that we may only use operations allowed by the abstract type in the body. This enforces that uses adhere to an interface so that concrete implementations may be swapped out as needed without breaking abstraction boundaries.
• This implementation follows a small-step operational semantics and Berendregt's variable convention (see substitutite in SOL.hs). The variable convention is adopted for both types and terms.
• Reductions include the one-step reduction (see reduce1 in SOL.hs), the many-step reduction (see reduce in SOL.hs).

Other Implementation Details

• SOL.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.