The variant (dialect) for morte language implementation.
Implementation based on http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/ and the next 2 posts.
This is a toy compiler of dependently-typed lambda calculus - a programming language with the next constructs:
-
f x
- apply a functionf
to argumentx
; -
universe n
-universe 0
is a type of all plain types (Int
,String
, etc),universe (n+1)
is a type ofuniverse n
; -
var x
-
(a : A) -> b
- an lambda function from variablea
of typeA
to expressionb
- ab
couldshould contain refs toa
. -
(a : A) => b
- a type of functions fromA
tob
(pi-type). Note,b
could mentiona
- there is the "dependency" comes from.