TT is the internal language of Idris. The Idris source code is converted to TT code which can then be converted to various back ends.
TT syntax
Terms, t ::= c (constant) | x (variable) | b.t (binding) | t t (application) | T (type constructor) | D (data constructor) Binders, b::= λ x:t (abstraction) | let x->t :t (let binding) |x :t (function space) Constants, c::= Typei (type universes) | i (integer literal) | str (string literal)
Example of TT
Idris> :let a=1
Idris> `(a+1)
App (App (App (App (P Ref
(NS (UN "+") ["Interfaces", "Prelude"])
(Bind (UN "ty")
(Pi (TType (UVar "./Prelude/Interfaces.idr" 2339))
(TType (UVar "./Prelude/Interfaces.idr" 2341)))
(Bind (UN "__interface")
(Pi (App (P (TCon 0 0)
(NS (UN "Num") ["Interfaces", "Prelude"])
Erased)
(V 0))
(TType (UVar "./Prelude/Interfaces.idr" 2342)))
(Bind (UN "__pi_arg")
(Pi (V 1) (TType (UVar "./Prelude/Interfaces.idr" 2343)))
(Bind (UN "__pi_arg3")
(Pi (V 2)
(TType (UVar "./Prelude/Interfaces.idr" 2344)))
(V 3))))))
(TConst (AType (ATInt ITBig))))
(P Ref
(NS (SN (ImplementationN (NS (UN "Num") ["Interfaces", "Prelude"])
["Integer"]))
["Interfaces", "Prelude"])
(App (P (TCon 184 1) (NS (UN "Num") ["Interfaces", "Prelude"]) Erased)
(TConst (AType (ATInt ITBig))))))
(P Ref (UN "a") (TConst (AType (ATInt ITBig)))))
(App (App (App (P Ref
(NS (UN "fromInteger") ["Interfaces", "Prelude"])
(Bind (UN "ty")
(Pi (TType (UVar "./Prelude/Interfaces.idr" 2362))
(TType (UVar "./Prelude/Interfaces.idr" 2364)))
(Bind (UN "__interface")
(Pi (App (P (TCon 0 0)
(NS (UN "Num") ["Interfaces", "Prelude"])
Erased)
(V 0))
(TType (UVar "./Prelude/Interfaces.idr" 2365)))
(Bind (UN "__pi_arg")
(Pi (TConst (AType (ATInt ITBig)))
(TType (UVar "./Prelude/Interfaces.idr" 2366)))
(V 2)))))
(TConst (AType (ATInt ITBig))))
(P Ref
(NS (SN (ImplementationN (NS (UN "Num") ["Interfaces", "Prelude"])
["Integer"]))
["Interfaces", "Prelude"])
(App (P (TCon 184 1) (NS (UN "Num") ["Interfaces", "Prelude"]) Erased)
(TConst (AType (ATInt ITBig))))))
(TConst (BI 1))) : TT
|
Structure of TT
This diagram represents the structure of TT as defined in the code here.
TT Representation Inside Library
TT can be represented by Idris users so that it can be used for elaborator reflection etc. See full code here: Idris1 Idris2
blue idris1 red idris2 |
||| Types of named references data NameType = ||| A reference which is just bound, e.g. by intro Bound | ||| A reference to a de Bruijn-indexed variable Ref | Func ||| Data constructor with tag and number DCon Int Int | DataCon : (tag : Int) -> (arity : Nat) ||| Type constructor with tag and number TCon Int Int TyCon : (tag : Int) -> (arity : Nat) ||| Types annotations for bound variables in different ||| binding contexts ||| ||| @ tmTy the terms that can occur inside the binder, as type ||| annotations or bound values data Binder : (tmTy : Type) -> Type where ||| Lambdas ||| ||| @ ty the type of the argument Lam : (ty : a) -> Binder a ||| Function types. ||| ||| @ kind The kind of arrow. Only relevant when dealing with ||| uniqueness, so you can usually pretend that this ||| field doesn't exist. For ordinary functions, use the ||| type of types here. Pi : (ty, kind : a) -> Binder a ||| A let binder ||| ||| @ ty the type of the bound variable ||| @ val the bound value Let : (ty, val : a) -> Binder a ||| A hole that can occur during elaboration, and must be filled ||| ||| @ ty the type of the value that will eventually be put into the hole Hole : (ty : a) -> Binder a ||| A hole that will later become a top-level metavariable GHole : (ty : a) -> Binder a ||| A hole with a solution in it. Computationally inert. ||| ||| @ ty the type of the value in the hole ||| @ val the value in the hole Guess : (ty, val : a) -> Binder a ||| A pattern variable. These bindings surround the terms that make ||| up the left and right sides of pattern-matching definition ||| clauses. ||| ||| @ ty the type of the pattern variable PVar : (ty : a) -> Binder a ||| The type of a pattern binding. This is to `PVar` as `Pi` is to ||| `Lam`. ||| ||| @ ty the type of the pattern variable PVTy : (ty : a) -> Binder a public export data Constant = I Int | BI Integer | Str String | Ch Char | Db Double | WorldVal | IntType | IntegerType | StringType | CharType | DoubleType | WorldType public export data Name = UN String | MN String Int | NS (List String) Name public export data Count = M0 | M1 | MW public export data PiInfo = ImplicitArg | ExplicitArg | AutoImplicit public export data IsVar : Name -> Nat -> List Name -> Type where First : IsVar n Z (n :: ns) Later : IsVar n i ns -> IsVar n (S i) (m :: ns) public export data LazyReason = LInf | LLazy | LUnknown ||| The various universes involved in the uniqueness mechanism data Universe = NullType | UniqueType | AllTypes ||| Reflection of the well typed core language data TT : List Name -> ||| A reference to some name (P for Parameter) P NameType TTName TT | ||| de Bruijn variables V Int | ||| Bind a variable Bind TTName (Binder TT) TT | ||| Apply one term to another App TT TT | ||| Embed a constant TConst Const | ||| Erased terms Erased | ||| The type of types along (with universe constraints) TType TTUExp | ||| Alternative universes for dealing with uniqueness UType Universe Local : FC -> (idx : Nat) -> (n : Name) -> (0 prf : IsVar name idx vars) -> TT vars Ref : FC -> NameType -> Name -> TT vars Pi : FC -> Count -> PiInfo -> (x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) -> TT vars Lam : FC -> Count -> PiInfo -> (x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) -> TT vars App : FC -> TT vars -> TT vars -> TT vars TDelayed : FC -> LazyReason -> TT vars -> TT vars TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars TForce : FC -> TT vars -> TT vars PrimVal : FC -> Constant -> TT vars Erased : FC -> TT vars TType : FC -> TT vars |
TT Example (Idris 1)
Here we define a very simple datatype. A Boolean-like structure with two constructors 'T' and 'F'.
In the diagram below:
- Red shows how we would declare & define in Idris source code.
- Green shows how we would declare & define in elaborator reflection.
- Blue shows how this is mapped to TT code.
Here is a function that uses it:
There are two main ‘tactics’ associated with generating datatypes:
- declareDatatype
- defineDatatype
Which declare and define the datatype as the names suggest.
| These ‘tactics’ and the data structures associated with them are listed in the tables later on this page, for now, here is a summary: |  |
| As a first example, the following boolean-like type can be constructed. When the compiler has run it will be available to us as if we had compiled it in the usual way: | data Two : Type where F : Two T : Two |
Also a couple of functions to use the type. Like this: |
perm1: Two -> Two perm1 F = F perm1 T = T perm2: Two -> Two perm2 F = T perm2 T = F |
Instead of entering this as Idris source code as above we can enter it in TT-like form using elaborator reflection as in the following code:
%language ElabReflection
module TwoDef
addTwo : Elab ()
addTwo = do
let twoname : TTName = `{{TwoDef.Two}}
let F2 = `{{TwoDef.F}}
let T2 = `{{TwoDef.T}}
declareDatatype $ Declare twoname [] `(Type)
defineDatatype $ DefineDatatype twoname [
Constructor `{{F}} [] (Var `{{TwoDef.Two}}),
Constructor `{{T}} [] (Var `{{TwoDef.Two}})
]
let perm1 = `{{TwoDef.perm1}}
declareType (Declare perm1 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
defineFunction $ DefineFun perm1 [
MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var F2),
MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var T2)
]
let perm2 = `{{TwoDef.perm2}}
declareType (Declare perm2 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
defineFunction $ DefineFun perm2 [
MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var T2),
MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var F2)
]
%runElab addTwo |
This is a lot more messy and complicated compared to the Idris code but it may be possible to do things Idris source can't. The objective here is just to try to understand this TT code.
We can also go in the other direction, from Idris -> TT, by using Quasiquotation:
*elabExTwoDef> T
T : Two
*elabExTwoDef> `(T)
P (DCon 1 0)
(NS (UN "T") ["TwoDef"])
(P (TCon 0 0) (NS (UN "Two") ["TwoDef"]) Erased) : TT
*elabExTwoDef> `(perm1 T)
App (P Ref
(NS (UN "perm1") ["TwoDef"])
(Bind (UN "code")
(Pi (P (TCon 63 0) (NS (UN "Two") ["TwoDef"]) Erased) (UType AllTypes))
(P (TCon 63 0) (NS (UN "Two") ["TwoDef"]) Erased)))
(P (DCon 1 0)
(NS (UN "T") ["TwoDef"])
(P (TCon 0 0) (NS (UN "Two") ["TwoDef"]) Erased)) : TT
*elabExTwoDef> `(perm2 T)
App (P Ref
(NS (UN "perm2") ["TwoDef"])
(Bind (UN "code")
(Pi (P (TCon 63 0) (NS (UN "Two") ["TwoDef"]) Erased) (UType AllTypes))
(P (TCon 63 0) (NS (UN "Two") ["TwoDef"]) Erased)))
(P (DCon 1 0)
(NS (UN "T") ["TwoDef"])
(P (TCon 0 0) (NS (UN "Two") ["TwoDef"]) Erased)) : TT
*elabExTwoDef> `(perm1 F)
App (P Ref
(NS (UN "perm1") ["TwoDef"])
(Bind (UN "code")
(Pi (P (TCon 63 0) (NS (UN "Two") ["TwoDef"]) Erased) (UType AllTypes))
(P (TCon 63 0) (NS (UN "Two") ["TwoDef"]) Erased)))
(P (DCon 0 0)
(NS (UN "F") ["TwoDef"])
(P (TCon 0 0) (NS (UN "Two") ["TwoDef"]) Erased)) : TT
|
We can also get the TT code like this:
*elabExTwoDef> addTwo
Prim__BindElab (Prim__DeclareDatatype (Declare (NS (UN "Two") ["TwoDef"])
[]
RType))
(\__bindx =>
Prim__BindElab (defineDatatype (DefineDatatype (NS (UN "Two") ["TwoDef"])
[Constructor (UN "F")
[]
(Var (NS (UN "Two")
["TwoDef"])),
Constructor (UN "T")
[]
(Var (NS (UN "Two")
["TwoDef"]))]))
(\__bindx =>
Prim__BindElab (declareType (Declare (NS (UN "perm1")
["TwoDef"])
[MkFunArg (UN "code")
(Var (NS (UN "Two")
["TwoDef"]))
Explicit
NotErased]
(Var (NS (UN "Two")
["TwoDef"]))))
(\__bindx =>
Prim__BindElab (defineFunction (DefineFun (NS (UN "perm1")
["TwoDef"])
[MkFunClause (RApp (Var (NS (UN "perm1")
["TwoDef"]))
(Var (NS (UN "F")
["TwoDef"])))
(Var (NS (UN "F")
["TwoDef"])),
MkFunClause (RApp (Var (NS (UN "perm1")
["TwoDef"]))
(Var (NS (UN "T")
["TwoDef"])))
(Var (NS (UN "T")
["TwoDef"]))]))
(\__bindx =>
Prim__BindElab (declareType (Declare (NS (UN "perm2")
["TwoDef"])
[MkFunArg (UN "code")
(Var (NS (UN "Two")
["TwoDef"]))
Explicit
NotErased]
(Var (NS (UN "Two")
["TwoDef"]))))
(\__bindx =>
defineFunction (DefineFun (NS (UN "perm2")
["TwoDef"])
[MkFunClause (RApp (Var (NS (UN "perm1")
["TwoDef"]))
(Var (NS (UN "F")
["TwoDef"])))
(Var (NS (UN "T")
["TwoDef"])),
MkFunClause (RApp (Var (NS (UN "perm1")
["TwoDef"]))
(Var (NS (UN "T")
["TwoDef"])))
(Var (NS (UN "F")
["TwoDef"]))])))))) : Elab ()
*elabExTwoDef>
|
