interpreter.idr

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

What I really want is just a type alias. Perhaps data is not the right way to declare that? Just a massive let, or in the using perhaps?

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 to Vect, even if I do know I want to fix the type argument.

The working definition turns out to be:

Env : Nat -> Type
Env n = Vect n Ty

and then use Env n throughout.