Skip to content

Latest commit

 

History

History
206 lines (140 loc) · 26 KB

README.md

File metadata and controls

206 lines (140 loc) · 26 KB
Raw

Edinburgh Logical Framework (first-order dependent types)

Haskell implementation of Bob Harper, Furio Honsell, and Gordon Plotkin's Edinburgh Logical Framework which captures first-order dependent types. It is STLC, but with a generalised Pi type, type-level application of terms, and type families. Dependent type machinery isn't useful on its own so we add Nats, and size-dependent Vectors of Nats to demonstrate how to instantiate types based on the size of their terms. We do not want to conflate LF with System F, and so do not include term-level types or polymorphism.

This strongly normalising calculus works on the notion of terms that depend on types under the banner of propositions as types. Dependent types allow us to encode predicate logic in a language with programs as witness or proof of propositions.

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

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

In either case you get something like the following:

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

  • \x:Nat.x the identity function on Nats.
  • nil the empty list of type Vec Nat 0
  • cons 0 1 nil the singleton list of type Vec Nat 1
  • cons 1 42 (cons 0 43 nil) a two element list.
  • (\n:Nat.cons n) 2 42 a function that takes a number and instantiates cons 2 with type Nat->Vec Nat 2->Vec Nat (succ 2). 42 is then applied to return a term of type Vec Nat (succ 2)
  • (\n:Nat. cons (succ n)) 0 42 (cons 0 9001 nil) Similar to the above but a two element set with 42 and 9001 in it.
  • \x:Pi n:Nat.Nat.x
  • \x:(\n:Nat.Vec Nat n) 0.x type-level abstraction to make clear that Pi types operate on terms from the term level, and abstractions operate on type level terms.

Note: Π is the dependent product type and Πx:A.B is the same as A -> B when x does not occur in B. Π is alternatively typed as Pi, respectively.

The parser is smart enough to recognise λ, Π , Nat, and Vec; so you can copy and paste from the output:

>   \x:Nat.x
=   λx:Nat.x
>   (\x:Vec Nat 1.x) (cons 0 42 nil)
~>* cons 0 42 nil

> 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.\x:Nat.cons (succ n) x) 0 42 (cons 0 42 nil)
~>  (λx:Nat.cons (succ 0) x) 42 (cons 0 42 nil)
~>  cons (succ 0) 42 (cons 0 42 nil)
~>  cons 1 42 (cons 0 42 nil)

Note: succ n stands for the successor of n, Peano style.

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

>   (\x:Vec Nat 4.x) nil
Cannot Type Term: (λx:Vec Nat 4.x) nil
>   (\x:Vec Nat 0.x) nil
~>* nil

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 singleton = \x:Nat.cons 0 x nil
Saved term: λx:Nat.cons 0 x nil
>   singleton 2
~>* cons 0 2 nil

Note: Consequently let and = are keywords, and so you cannot name variables with these. Additionally Nat, succ, cons, nil, and Pi are keywords in LF.

Note: We include introduction rules for Nats to show type-level term substitution works. We do not include Nat eliminators or any notion of type-based polymorphism however as the focus is on dependent types. 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 VECZ = Vec Nat 0
Saved type: Vec Nat 0
>   (\x:VECZ.x) nil
~>* nil

Submit a PR with eliminators for Vectors and Natural numbers, or perhaps some machinery to introduce term constructors of a given type.

This makes it easier to define both terms and types, but does not allow type-level application (See Omega) or type-based polymorphism (see SystemF). lett is also a keyword.

Note: we do not allow the ability to add types, constructors, or type families (something like assume (Bool::*) (True:Bool)) as this would allow us to encode term-level types which is the remit of FOmega, and indeed may allow us to encode Girard's Paradox.

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:

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 variables are strings (excluding numbers), as this is isomorphic to a whiteboard treatment and hence the most familiar. Term variables are lower case.
  • Terms are variables, functions \x:Nat.x, applications a b (where a and b are in scope), empty lists nil, non-empty lists cons 0 42 nil which is a singleton list containing 42 of type Vec Nat 1, or a non-negative natural number 0,1,2,3,....
  • Types are dependent abstractions Pi n:Nat.T, type-level abstractions \x:Nat.x applications A t (where t is a term), arrows A -> B (which is the same as a Pi type where the variable doesn't occur in B), Nats, or size bounded vectors Vec Nat t where t is a term of type Nat.
  • kinds are not part of the syntax, but play a role in typing. See K.
  • Type arrows associate to the right so that X -> Y -> Z is the same as X -> (Y -> Z) but not ((X -> Y) -> Z).
  • The Pi type binds weaker than arrows, so Pi x:Nat. Nat->Nat is the same as Pi x:Nat. (Nat->Nat).
  • Nested terms don't need brackets: \x:Nat.\y:Nat. y unless enforcing application on the right. Whitespace does not matter (\x:Nat. x) unless it is between application where you need at least one space. Like term-level functions, Pi must be put in brackets when applied to a term: \x:(Pi n:Nat.Vec Nat n) 0.x.
  • To quit use Ctrl+C or whatever your machine uses to interrupt computations.

Semantics

The semantics implements beta-reduction on terms and typed definitional equality as the Eq instance of T. The term semantics are the same as STLC with the addition of dependent abstraction of types over terms, term-dependent vectors and natural numbers. We reformulate the semantics as typing judgements:

Firstly, we have the standard rule for variables augmented with kinding information (variables must be of proper type):

For term abstractions we replace -> with a dependent Π type, which allows the type on the right-hand side of the type to depend on the value passed on the left (Πn:Nat.Vec Nat n for instance). When the right-hand side does not use the variable Πx:Nat.Nat, we pretty print it as Nat -> Nat (where Π_:A.B = A -> B):

For term applications, we can now instantiate a type with a term provided to the application. The left-hand Π type must be parametrized by the same type as the value on the right-hand side of the application, and the value can then be substituted into the type. For instance in (\n:Nat.cons n) 2 42, n and 2 are of the same type and so the expression has type Vec Nat 2->Vec Nat 3 (see the typing rules below for nats.)

We have the standard beta reduction from the untyped calculus at the term-level:

We have standard typing rules for Nats (with standard reduction rules under terms omitted):

or put another way (see typeof in LF.hs):

where Π _:Nat.Nat is pretty printed as Nat -> Nat since _ does not occur in the right-hand side of the type.

Similarly we have typing rules for size-bounded Vectors. Since this is the first-order dependent types, we do not have type abstraction as the intention of this language is to show off dependent types in action. As a result, Vector types are parametrised only by Nats:

We now have term-dependent abstraction (Pi type), application, and type-constants (like Nat) at the type level with 'types of types' known as kinds and type families. Type families are kinds indexed by a term, which is also indexing types of this kind as a result of the term application rule above. Note: kinds do not appear in the syntax but aid-typing.

We have kind variables:

We have Pi abstractions of proper type:

We have type-level abstractions:

And kinding rules for type-level application:

Nat is a proper type *, and cons, succ make use of the typing rules, and kinding rules as necessary.

  • This means the typing context now also contains types, and terms occur in types. The phrase X :: K means type 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 Vec 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), or any dependent types, and so it is unusable as no terms can be introduced. To demonstrate dependent types, we add the proper type Nat, with constructors succ and 0,1,2,3 as well as the type Vec with nil and cons as constructors.
  • Type-level application is identical to term-level application in STLC, except it makes uses of dependent typing from terms to types. In applying a term t of type T to a term f of type Pi x:T.T2 we substitute t into T2 wherever x is bound.
  • Arrows/Pi types have the constraint that both the domain and co-domain must be proper types. This prevents non-nonsensical types such as Pair Nat _ -> Nat.
  • LF provides a mean to define types from terms. By using abstraction and application to form types from terms. Type operators themselves do not define terms (there is no term of type \x:Nat.Vec Nat x) but are used to form proper types which do have terms: (\x:Nat.Vec Nat x) 0 ~>* Vec Nat 0 which has term nil.
  • Unlike type operators, Pi types do have terms, Pi types are introduced by term-level abstractions and their type depends on the term applied to this abstraction. For instance \x:Nat.cons x 42 has type Π x:Nat.Vec Nat x->Vec Nat (succ x).
  • Now that computation occurs at the type level, we can not simply use structural equality on types as we would not be able to equate type-level terms (\x:Nat.x) 0 and 0. Thus we adopt a kind of computational definitional equality based on typed beta-reduction. That is two types are the same if they are the structurally the same with equivalent typeable terms after reduction (with alpha-equivalent normal forms wherever terms appear). Likewise typeable terms are equivalent if they match in structure after normalisation with equivalent types according to the first criteria. This mutually recursive definition is normalising according to arguments that always reduce in size.
  • This implementation follows a small-step operational semantics and Berendregt's variable convention (see substitution in LF.hs).
  • Reductions include the one-step reduction (see reduce1 in LF.hs), the many-step reduction (see reduce in LF.hs). Additionally there is a one-step type-level reduction (see reduce1T in LF.hs).

Other Implementation Details

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