Created
August 12, 2015 00:06
-
-
Save jeremy-w/c011d413fbb31c888382 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Data.Vect | |
import Data.Fin | |
-- Start by representing our universe as a product type. | |
data Ty = TyInt | TyBool | TyFun Ty Ty | |
interpret : Ty -> Type | |
interpret TyInt = Int | |
interpret TyBool = Bool | |
interpret (TyFun A T) = interpret A -> interpret T | |
data Env = Vect n Ty | |
using (E: Env) | |
data HasType : (i : Fin n) -> Env -> Ty -> Type where | |
Stop : HasType FZ (ty :: E) ty | |
Pop : HasType k E ty -> HasType (FS k) (u :: E) ty | |
data Expr : Env -> Ty -> Type where | |
Var : HasType i E ty -> Expr E ty | |
Val : (x : Int) -> Expr E TyInt | |
Lam : Expr (a :: E) ty -> Expr E (TyFun a ty) | |
App : Expr E (TyFun a ty) -> Expr E a -> Expr E ty | |
Op : (interpret lhs -> interpret rhs -> interpret result) | |
-> Expr E lhs -> Expr E rhs -> Expr E result | |
If : Expr E TyBool | |
-> Lazy (Expr E ty) | |
-> Lazy (Expr E ty) -> Expr E ty |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Looking at this post which came up in a search of the web for "idris how to write typealias", I saw that my original guess of just writing
x = y
to declare the alias was correct.It didn't work as I originally wrote it because I was thinking in terms of a textual substitution. But of course I can't just disappear the
n
argument toVect
, even if I do know I want to fix the type argument.The working definition turns out to be:
and then use
Env n
throughout.