Typing rules

The typing rules will appear when I've figured out how to do them in HTML, and also figured out exactly what they are. :-)

"Star"

# : #1

Variable

A:s
, x : A x : A

Apply

f : (x::A) -> B a : A
f a : B[x:=a]

Lambda

, x : A b : B ((x::A) -> B) : t
(\(x::A) -> b) : ((x::A) -> B)

Pi

A:s , x : A B : t
((x::A) -> B) : t

Conversion

a:A B:s A =ß B
a : B

Weakening

b : B B : s
, x : B b : B

Data

Aij : #
k > 0, nk 0
data C1 A11 ... A1n1 | ... | Ck Ak1 ... Aknk : #

Constructor

T data C1 A11 ... A1n1 | ... | Ck Ak1 ... Aknk

T : #
Ci @ T : Ai1 -> ... -> Aiki -> T

Case

Product

A1 : s1 ... An : sn ... ej : Aj
sig { l1 :: A1 1; ... lk :: Ak k; ... ln :: An n } : #u
where all i is either empty or "= ei".
where j belongs to a subset of 1..n.

Record

Select

Beta

(\(x::A) -> B) C =ß B[x := C]

Sel

{ l1 :: A1 = e1; ... ln :: An = en } . lk =ß ek[l1 := e.l1, ... ln := e.ln]

Sel-Type

e : { l1 :: A1 1; ... lk :: Ak = ek; ... ln :: An n }
e . lk =ß ek[l1 := e.l1, ... lb := e.ln]
where i is either empty or "= ei".

Back

Lennart Augustsson
Last modified: Mon Aug 31 01:39:56 CEST 1998