Typed Interpreter in Haskell

gistfile1.hs

{-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NPlusKPatterns #-}
module Main where

import Prelude hiding (lookup, id)

data Ty = TyBool | TyNat | Ty :~> Ty

type family InterpTy (t :: Ty) :: * where
  InterpTy TyBool    = Bool
  InterpTy TyNat     = Int
  InterpTy (s :~> t) = InterpTy s -> InterpTy t

data Env (ts :: [Ty]) :: * where
  Nil  :: Env '[]
  Cons :: InterpTy t -> Env ts -> Env (t ': ts)

data DeBruijn (ts :: [Ty]) (t :: Ty) :: * where
  Stop :: DeBruijn (t ': ts) t
  Pop  :: DeBruijn ts t -> DeBruijn (s ': ts) t

lookup :: DeBruijn ts t -> Env ts -> InterpTy t
lookup Stop    (Cons t _)  = t
lookup (Pop i) (Cons _ ts) = lookup i ts

data Expr (ts :: [Ty]) (t :: Ty) :: * where
  Var :: DeBruijn ts t -> Expr ts t
  T   :: Expr ts TyBool
  F   :: Expr ts TyBool
  If  :: Expr ts TyBool -> Expr ts a -> Expr ts a -> Expr ts a
  Lam :: Expr (s ': ts) t -> Expr ts (s :~> t)
  App :: Expr ts (s :~> t) -> Expr ts s -> Expr ts t
  Z   :: Expr ts TyNat
  S   :: Expr ts TyNat -> Expr ts TyNat
  Rec :: Expr ts TyNat
      -> Expr ts a
      -> Expr ts (TyNat :~> (a :~> a))
      -> Expr ts a

eval :: Env ts -> Expr ts t -> InterpTy t
eval env (Var i)         = lookup i env
eval env (S n)           = 1 + eval env n
eval _   Z               = 0
eval _   T               = True
eval _   F               = False
eval env (Lam sc)        = \e -> eval (Cons e env) sc
eval env (App f x)       = eval env f $ eval env x
eval env (If c t f)      =
  case eval env c of
       True  -> eval env t
       False -> eval env f
eval env (Rec n x f)     =
  case eval env n of
       0      -> eval env x
       n' + 1 -> eval env f n' (eval env x)

id :: Expr ts (a :~> a)
id = Lam (Var Stop)

inc :: Expr ts (TyNat :~> TyNat)
inc = Lam (S (Var Stop))

plus :: Expr ts (TyNat :~> (TyNat :~> TyNat))
plus =
  Lam (
    Lam (
      Rec (Var (Pop Stop)) (Var Stop) (
        Lam (
          Lam (
            App inc (App (App plus (Var (Pop Stop))) (Var Stop))
          )
        )
      )
    )
  )

main :: IO ()
main = print $ eval Nil (App (App plus (S (S (S Z)))) (S (S Z)))