WellTypedInterpreter.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module WellTypedInterpreter where

-- The Well-Typed Interpreter
-- References: https://idris2.readthedocs.io/en/latest/tutorial/interp.html

import Data.Kind (Type)

data Typ
  = TyInt
  | TyBool
  | TyFun Typ Typ

type Env :: [Typ] -> Type
data Env a where
  Nil :: Env '[]
  Cons :: Interp t -> Env ctxt -> Env (t ': ctxt)

type Interp :: Typ -> Type
type family Interp a where
  Interp TyInt = Integer
  Interp TyBool = Bool
  Interp (TyFun a b) = Interp a -> Interp b

type HasTyp :: [Typ] -> Typ -> Type
data HasTyp a b where
  Stop :: HasTyp (t : ctxt) t
  Pop :: HasTyp ctxt t -> HasTyp (t ': ctxt) t

type Expr :: [Typ] -> Typ -> Type
data Expr a b where
  Var :: HasTyp ctxt t -> Expr ctxt t
  Val :: Integer -> Expr ctxt TyInt
  Lam ::
    Expr (a ': ctxt) t ->
    Expr ctxt (TyFun a t)
  App ::
    Expr ctxt (TyFun a b) ->
    Expr ctxt a ->
    Expr ctxt b
  Op ::
    (Interp a -> Interp b -> Interp c) ->
    Expr ctxt a ->
    Expr ctxt b ->
    Expr ctxt c
  If ::
    Expr ctxt TyBool ->
    Expr ctxt a ->
    Expr ctxt a ->
    Expr ctxt a

lookup' :: HasTyp ctxt t -> Env ctxt -> Interp t
lookup' Stop (Cons x xs) = x
lookup' (Pop k) (Cons _ xs) = lookup' k xs

interp' :: Env ctxt -> Expr ctxt t -> Interp t
interp' ctxt = \case
  Val x -> x
  Var i -> lookup' i ctxt
  Lam l -> \x -> interp' (Cons x ctxt) l
  App f a -> interp' ctxt f (interp' ctxt a)
  Op op x y -> op (interp' ctxt x) (interp' ctxt y)
  If p c a ->
    if interp' ctxt p
      then interp' ctxt c
      else interp' ctxt a

interp :: Expr '[] t -> Interp t
interp = interp' Nil

add :: Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

fact :: Expr ctxt (TyFun TyInt TyInt)
fact =
  Lam
    ( If
        (Op (==) (Var Stop) (Val 0))
        (Val 1)
        ( Op
            (*)
            (App fact (Op (-) (Var Stop) (Val 1)))
            (Var Stop)
        )
    )

x = interp add