glam is an implementation of the guarded λ-calculus, as described in the paper The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types by Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl and Lars Birkedal, and extended with polymorphism and automatic boxing as described in my internship report.
Please refer to those papers for basic motivation and introduction to the language, as well as a description of its type system, operational and denotational semantics. This README only covers the specifics of my implementation.
An online demo is available, as well as rendered documentation.
This project is built using Cabal (cabal build).
usage: glam [options...] files...
-i --interactive run in interactive mode (default if no files are provided)
The interactive mode gives you a REPL that will execute statements and display their results. It also provides a :type command that displays the type of a given term.
glam's syntax is intended to be similar to Haskell's. See the examples directory for example programs.
The syntax for types is as follows:
TVar = [a-zA-Z_] [a-zA-Z_0-9']* ; (excluding keywords)
Type = "(" Type ")"
| TVar ; type variables
| TVar Type* ; application of type synonyms
| "Int" ; integer type
| "0" ; zero/void/initial type
| "1" ; unit/terminal type
| Type "*" Type ; product types
| Type "+" Type ; coproduct/sum types
| Type "->" Type ; function types
| ">" Type ; Later types
| "#" Type ; Constant types
| "Fix" TVar "." Type ; fixed point types
TypeDef = "type" TVar TVar* "=" Type ; type synonyms
Polytype = ("forall" ("#"? TVar)+ ".")? Type
*, + and -> are right-associative. Unicode syntax is supported (μ, ∀, →, ×, ⊤, ⊥, ℤ, ▸, ■).
Some syntactic sugar is provided:
| Construct | Desugars to |
|---|---|
type T x y z = ... (T x y z) ... |
type T x y z = Fix T. ... T ... |
Due to the absence of type-level lambdas, type synonyms must be applied to exactly as many arguments as they expect. When using a type synonym recursively inside its own definition, it must be applied to its exact formal arguments.
The syntax for terms is as follows:
Var = [a-zA-Z_] [a-zA-Z_0-9']* ; (excluding keywords)
Integer = [0-9]+
Binary = "+" | "-" | "*" | "/" | "<$>" | "<*>"
Unary = "fst" | "snd"
| "abort" | "left" | "right"
| "fold" | "unfold"
| "next" | "prev"
| "box" | "unbox"
Term = "(" Term ")"
| Var ; variables
| Integer ; integers
| "intrec" ; integer recursion operator (forall a. (a -> a) -> a -> (a -> a) -> Int -> a)
| "(" ","-separated(Term+) ")" ; tuples
| "(" ")" ; unit
| Term Term ; applications
| Term Binary Term ; binary operators
| Unary Term ; unary operators
| "\" Var+ "." Term ; λ-abstractions
| "fix" Var+ "." Term ; fixed points
| "let" "{" ";"-separated(TermDef) "}" ; let expressions
"in" Term
| "case" Term "of" "{" ; case expressions
"left" Var "." Term ";"
"right" Var "." Term "}"
TermDef = Var Var* "=" Term
Unicode syntax is supported (λ, ⊛).
Some syntactic sugar is provided:
| Construct | Desugars to |
|---|---|
f x y z = t |
f = \x y z. t |
f = ... f ... |
f = fix f. ... f ... |
(a, b, c, ...) |
(a, (b, (c, ...))) |
\x y z. t |
\x. \y. \z. t |
fix x y z. t |
fix x. \y z. t |
f <$> x |
next f <*> x |
glam programs are structured as follows:
Signature = Var ":" Polytype
Statement = TypeDef
| Signature
| TermDef
| Term
Program = newline-separated(Statement)
Statements can span over multiple lines, provided that subsequent lines are indented further than the first line.
Type signatures and term definitions don't have to appear consecutively, but signatures have to appear before definitions.
Type signatures can be omitted; a most general type will then be inferred. In practice, most signatures can be omitted, except for terms involving fold and unfold.
The interpreter currently prints the (inferred or checked) type for each top-level term definition, as well as the value and inferred type of top-level terms.
Terms are evaluated using a call-by-need strategy (piggy-backing on Haskell's), based on the operational semantics given in the paper. This is a form of normalisation by evaluation (NbE), except we don't reify values back into terms.
glam extends the guarded λ-calculus with predicative, rank-1 polymorphism à la Hindley-Milner.
Polymorphic types (or polytypes) are of the form forall a #b. ..., where a refers to any type, while b refers to any constant type.
To allow for interesting polymorphic types involving the constant (#) modality, the definition of valid types has been modified to allow polymorphic type variables to appear under #.
The definition of constant types has also been modified as follows:
xis a constant type if and only ifxis bound byforall #x0,1,#Tare constant types>Tis not a constant typeT1 * T2,T1 + T2are constant if and only ifT1andT2are both constantT1 -> T2is constant if and only ifT2is constant¹Fix x. Tis constant if and only ifTis constant
¹ This is also more permissive than the paper's definition; this modification is based on semantic considerations.
Just like in standard Hindley-Milner, polymorphic generalisation only occurs for let-bound terms (but not inside recursive definitions).
Consider the following motivating examples:
- The term
let { z = consG 0 z } in box z(whereconsGis the constructor for guarded recursive streams) should type-check, becausebox (fix z. consG 0 z)does; but the typing rules given by the paper prohibit this becausezhas the non-constant typeFix s. Int * >s. - The box⁺ term former introduced in the paper is inelegant. We would like to be able to define such a construct internally:
Again, this would not be allowed, because
box' : forall a b. #(a + b) -> #a + #b box' ab = case unbox ab of { left a. left box a; right b. right box b }aandbhave the potentially non-constant typesaandb.
We solve these two problems simultaneously by introducing (context-dependent) notions of boxable terms and boxed variables, defined as follows:
- A term is boxable if each of its free variables is either boxed or has a constant type.
- A variable that is
let-bound to a boxable term is automatically boxed (this includes top-level bindings; as a consequence, all top-level bound variables are boxed). Similarly, a variable bound in acaseexpression from matching on a boxable term is boxed.
The box t and prev t constructs require t to be boxable. This makes the examples above type-check as expected.
- Infer types for
foldandunfoldvia higher-orderish unification. This should type-check:(Note that it does if you usetype CoNat = 1 + >CoNat rec : forall a. a -> (>a -> a) -> CoNat -> a rec z s = let { go n = case unfold n of { left _. z; right m. s (go <*> m) } } in gofix go.) - Better type error reporting.
- Make semicolons and braces optional using something like Haskell's layout rules.
- Add infix operators.
- Make
left,right,abort,fst,snd,(,)(the pair former),fix,next,(<$>),(<*>)andunboxfirst-class functions instead of keywords. - Proper type constructors and pattern matching.
- Add basic types and operations (booleans, characters, strings...), and some sort of standard library for dealing with streams, colists, ...
- Add syntactic sugar to make recursive definitions less painful to write and read: idiom brackets, Idris-style
!(notation), something. - More generally turn glam into a usable and useful programming language.