Skip to content

Latest commit

 

History

History
157 lines (114 loc) · 6.26 KB

README.md

File metadata and controls

157 lines (114 loc) · 6.26 KB

Chapter 10: Simple Types

A Ruby implementation of the type checker described in Chapter 10 of Benjamin C. Pierce's "Types and Programming Languages" mobbed during a meeting of London Computation Club on Tuesday, 23rd May 2017.

Installation

git clone git://github.com/computationclub/simple-types.git
cd simple-types
bundle install
make

AST nodes

Symbolic operators

This syntax makes use of a few non-ASCII symbols for operators. All have ASCII alternatives should you be working in an environment where typing these symbols is a faff. They are:

  • λ, used to begin an abstraction, alternative: \
  • ⇒, to introduce case clause bodies, alternative: =>
  • →, the function type operator, alternative: ->
  • ×, the product type operator, alternative: *

Lambda calculus

Syntax Node
x Term::Var(name: string)
λx:T. t Term::Abs(param: string, type: type, body: term)
t t Term::Application(left: term, right: term)
T → T Type::Function(from: type, to: type)

Booleans

Syntax Node
true Term::True
false Term::False
if t then t else t Term::If(condition: term, consequent: term, alternate: term)
Bool Type::Boolean

Numeric

Syntax Node
0 Term::Zero
succ t Term::Succ(arg: term)
pred t Term::Pred(arg: term)
iszero t Term::Iszero(arg: term)
Nat Type::Natural

Base types

Syntax Node
T Type::Base(name: string)

Unit type

Syntax Node
unit Term::Unit
Unit Type::Unit

Sequencing

Syntax Node
t ; t Term::Sequence(first: term, last: term)

Ascription

Syntax Node
t as T Term::Ascribe(term: term, type: type)

Let binding

Syntax Node
let x=t in t Term::Let(param: string, arg: term, body: term)

Projection

Syntax Node
t.1, t.foo Term::Project(object: term, field: int | string)

Pairs

Syntax Node
{t | t} Term::Pair(left: term, right: term)
T × T Type::Product(left: type, right: type)

Tuples

Syntax Node
{t, t, ...} Term::Tuple(members: [term])
{T, T, ...} Type::Tuple(members: [type])

Records

Syntax Node
{foo=t, bar=t, ...} Term::Record(members: {string => term})
{foo: T, bar: T, ...} Type::Record(members: {string => type})

Sums

In these terms, clause means Term::CaseClause(param: string, body: term)

Syntax Node
inl t Term::Inl(term: term)
inr t Term::Inr(term: term)
inl t as T Term::Inl(term: term, type: type)
inr t as T Term::Inr(term: term, type: type)
case t of inl x ⇒ t | inr x ⇒ t Term::SumCase(term: term, left: clause, right: clause)
T + T Type::Sum(left: type, right: type)

Variants

In these terms, clause means Term::CaseClause(param: string, body: term)

Syntax Node
<label=t> as T Term::Tagged(label: string, term: term, type: type)
case t of <foo=x> ⇒ t | <bar=x> ⇒ t | ... Term::VarCase(term: term, clauses: {string => clause})
<foo: T, bar: T, ...> Type::Variant(clauses: {string => type})

Lists

Syntax Node
nil[T] Term::Nil(type: type)
cons[T] t t Term::Cons(type: type, head: term, tail: term)
isnil[T] t Term::Isnil(type: type, arg: term)
head[T] t Term::Head(type: type, arg: term)
tail[T] t Term::Tail(type: type, arg: term)
List T Type::List(type: type)

References

Syntax Node
ref t Term::Ref(value: term)
!t Term::Deref(ref: term)
t := t Term::Assign(ref: term, value: term)
Ref T Type::Ref(type: type)