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

I'm working on The Well-Typed Interpreter section from the tutorial.

I don't want to have to write Vect n Ty umpteen times, and that's not terribly meaningful, either, so I tried to create a more meaningful type alias using data Env = Vect n Ty.

The code using Env throughout instead of Vect n Ty fails to typecheck, but I don't understand why:

> idris -c interpreter.idr                                                                                                    [1]
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.18-
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./interpreter.idr
interpreter.idr:15:24:When elaborating type of Main.Stop:
When elaborating an application of Main.HasType:
        Can't unify
                Vect (S n) a (Type of x :: xs)
        with
                Env (Expected type)
interpreter.idr:19:13:When elaborating type of Var:
No such variable HasType

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.