| Safe Haskell | None |
|---|
Annah.Core
Contents
Description
This module contains the core machinery for the Annah language, which is a medium-level language that desugars to Morte.
The main high-level features that Annah does not provide compared to Haskell are:
- type classes
- type inference
You cannot type-check or normalize Annah expressions directly. Instead,
you desugar Annah expressions to Morte, and then type-check or normalize
the Morte expressions using typeOf and normalize.
Annah does everything through Morte for two reasons:
- to ensure the soundness of type-checking and normalization, and:
- to interoperate with other languages that compile to Morte.
The typical workflow is:
- data Var = V Text Int
- data Const
- data Arg = Arg {}
- data Let = Let {}
- data Data = Data {}
- data Type = Type {}
- data Bind = Bind {}
- data Expr
- desugar :: Expr -> Expr Path
- desugarFamily :: [Type] -> [Let]
- desugarNatural :: Integer -> Expr Path
- desugarDo :: Expr -> [Bind] -> Bind -> Expr Path
- desugarList :: Expr -> [Expr] -> Expr Path
- desugarPath :: Expr -> [(Expr, Expr)] -> Expr -> Expr Path
- desugarLets :: [Let] -> Expr -> Expr Path
Syntax
data Var
Label for a bound variable
The Text field is the variable's name (i.e. "x").
The Int field disambiguates variables with the same name if there are
multiple bound variables of the same name in scope. Zero refers to the
nearest bound variable and the index increases by one for each bound variable
of the same name going outward. The following diagram may help:
+-refers to-+
| |
v |
\(x : *) -> \(y : *) -> \(x : *) -> x@0
+-------------refers to-------------+
| |
v |
\(x : *) -> \(y : *) -> \(x : *) -> x@1
This Int behaves like a De Bruijn index in the special case where all
variables have the same name.
You can optionally omit the index if it is 0:
+refers to+
| |
v |
\(x : *) -> \(y : *) -> \(x : *) -> x
Zero indices are omitted when pretty-printing Vars and non-zero indices
appear as a numeric suffix.
data Const
Constants for the calculus of constructions
The only axiom is:
⊦ * :
... and all four rule pairs are valid:
⊦ * ↝ * : ⊦ □ ↝ * : ⊦ * ↝ □ ⊦ □ ↝ □
Argument for function or constructor definitions
Arg "_" _A ~ _A Arg x _A ~ (x : _A)
Instances
| Show Arg |
Let f [a1, a2] _A rhs ~ let f a1 a2 : _A = rhs
Instances
| Show Let |
Data c [a1, a2] ~ data c a1 a2
Instances
| Show Data |
Type t [d1, d2] f ~ type t d1 d2 fold f
Instances
| Show Type |
Bind arg e ~ arg <- e;
Instances
| Show Bind |
Syntax tree for expressions
Constructors
| Const Const | Const c ~ c |
| Var Var | Var (V x 0) ~ x Var (V x n) ~ x@n |
| Lam Text Expr Expr | Lam x _A b ~ λ(x : _A) → |
| Pi Text Expr Expr | Pi x _A _B ~ ∀(x : _A) → _B |
| App Expr Expr | App f a ~ f a |
| Annot Expr Expr | Annot a _A ~ a : _A |
| Lets [Let] Expr | Lets [l1, l2] e ~ l1 l2 in e |
| Family [Type] Expr | Family f e ~ f in e |
| Natural Integer | Natural n ~ n |
| List Expr [Expr] | List t [x, y, z] ~ [nil t,x,y,z] |
| Path Expr [(Expr, Expr)] Expr | Path c [(o1, m1), (o2, m2)] o3 ~ [id c {o1} m1 {o2} m2 {o3}]
|
| Do Expr [Bind] Bind | Do m [b1, b2] b3 ~ do m { b1 b2 b3 }
|
| Embed Path |
Desugaring
Convert an Annah expression to a Morte expression
desugarFamily :: [Type] -> [Let]Source
This translates datatype definitions to let expressons using the Boehm-Berarducci encoding.
For example, this mutually recursive datatype definition:
type Even data Zero data SuccE (predE : Odd) fold foldEven type Odd data SuccO (predO : Even) fold foldOdd in SuccE
... desugars to seven let expressions:
let Even : * = ... let Odd : * let Zero : Even = ... let SuccE : ∀(predE : Odd ) → Even = ... let SuccO : ∀(predO : Even) → Odd = ... let foldEven : ∀(x : Even) → ... = ... let foldOdd : ∀(x : Odd ) → ... = ... in SuccE
... and normalizes to:
λ( predE : ∀(Even : *)
→ ∀(Odd : *) → ∀(Zero : Even) → ∀(SuccE : ∀(predE : Odd ) → Even → ∀(SuccO : ∀(predO : Even) → Odd → Odd )
→ λ(Even : * → λ(Odd : * → λ(Zero : Even → λ(SuccE : ∀(predE : Odd) → Eve → λ(SuccO : ∀(predO : Even) → Od → SuccE (predE Even Odd Zero SuccE SuccO)desugarNatural :: Integer -> Expr PathSource
Convert a natural number to a Morte expression
For example, this natural number:
4
... desugars to this Morte expression:
λ(Nat : * ) → λ(Succ : ∀(pred : Nat) → Na → λ(Zero : Nat → Succ (Succ (Succ (Succ Zero)))
desugarDo :: Expr -> [Bind] -> Bind -> Expr PathSource
Convert a command (i.e. do-notation) into a Morte expression
For example, this command:
do m
{ x0 : _A0 <- e0;
x1 : _A1 <- e1;
}
.. desugars to this Morte expression:
λ(Cmd : *) → λ(Bind : ∀(b : *) → m b → (b → Cmd) → → λ(Pure : ∀(x1 : _A1) → Cm → Bind _A0 e0 ( λ(x0 : _A0) → Bind _A1 e1 Pure
)
desugarList :: Expr -> [Expr] -> Expr PathSource
Convert a list into a Morte expression
For example, this list:
[nil Bool, True, False, False]
... desugars to this Morte expression:
λ(List : *) → λ(Cons : ∀(head : Bool) → ∀(tail : List) → Li → λ(Nil : List → Cons True (Cons False (Cons False Nil))
desugarPath :: Expr -> [(Expr, Expr)] -> Expr -> Expr PathSource
Convert a path into a Morte expression
For example, this path:
[id cat {a} f {b} g {c}]
... desugars to this Morte expression:
λ(Path : ∀(a : *) → ∀(b : *) → → λ( Ste : ∀(a : *)
→ ∀(b : *) → ∀(c : *) → ∀(head : cat a b) → ∀(tail : Path b c) → Path a c )
→ λ(End : ∀(a : *) → Path a → Step a b c f (Step b c c g (End c))desugarLets :: [Let] -> Expr -> Expr PathSource
Convert a let expression into a Morte expression
For example, this let expression:
let f0 (x00 : _A00) ... (x0j : _A0j) _B0 = b0 .. let fi (xi0 : _Ai0) ... (xij : _Aij) _Bi = bi in e
... desugars to this Morte expression:
( \(f0 : forall (x00 : _A00) -> ... -> forall (x0j : _A0j) -> _B0) -> ... -> \(fi : forall (xi0 : _Ai0) -> ... -> forall (xij : _Aij) -> _Bi) -> e ) (\(x00 : _A00) -> ... -> \(x0j : _A0j) -> b0) ... (\(xi0 : _Ai0) -> ... -> \(xij : _Aij) -> bi)