Simply-Typed Lambda Calculus written in "glorious" "dependent" Haskell.

STLC.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}


module Main (test01, test02, main) where

import Data.Kind


data Elem :: k -> [k] -> Type where
  Here  :: Elem x (x : xs)
  There :: Elem x xs -> Elem x (y : xs)


data HList :: [Type] -> Type where
  HNil  :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)


headHL :: HList (head ': tail) -> head
headHL (HCons x _) = x


data Expr :: [ProgramType] -> ProgramType -> Type where

  Ann :: Expr context programType
      -> ProgramTypeSingleton programType
      -> Expr context programType

  Var :: Elem programType context
      -> Expr context programType

  App :: Expr context (input :=> output)
      -> Expr context input
      -> Expr context output

  Lam :: ProgramTypeSingleton programType
      -> Expr (programType : context) bodyType
      -> Expr context (programType :=> bodyType)


data ProgramType
  = ProgramTypeInt
  | ProgramType :=> ProgramType


data ProgramTypeSingleton :: ProgramType -> Type where

  ProgramTypeIntSingleton
    :: ProgramTypeSingleton ProgramTypeInt

  ProgramTypeFunctionSingleton
    :: ProgramTypeSingleton input
    -> ProgramTypeSingleton output
    -> ProgramTypeSingleton (input :=> output)


type family ProgramTypeToType (ptype :: ProgramType) :: Type where

  ProgramTypeToType ProgramTypeInt
    = Int

  ProgramTypeToType (input :=> output)
     = ProgramTypeToType input
    -> ProgramTypeToType output


type family ContextToTypeList (ptype :: [ProgramType]) :: [Type] where

  ContextToTypeList '[]
    = '[]

  ContextToTypeList (x : xs)
    = ProgramTypeToType x
    : ContextToTypeList xs


get :: Elem x xs -> HList xs -> x
get  Here       (HCons x  _) = x
get (There ref) (HCons _ xs) = get ref xs


ptypeRefToTypeRef
  :: Elem programType context
  -> Elem (ProgramTypeToType programType)
          (ContextToTypeList context)

ptypeRefToTypeRef = \case
  Here      -> Here
  There ref -> There (ptypeRefToTypeRef ref)


eval
  :: Expr context programType
  -> HList (ContextToTypeList context)
  -> ProgramTypeToType programType

eval expr context
  = case expr of
      Ann expr _ ->
        eval expr context

      Var ref ->
        get (ptypeRefToTypeRef ref) context

      App f x ->
        (eval f context)
        (eval x context)

      Lam _ body ->
        \x -> eval body (HCons x context)

stlcID :: Expr '[] (ProgramTypeInt :=> ProgramTypeInt)
stlcID = Lam ProgramTypeIntSingleton (Var Here)

stlcAPPLY
  :: Expr '[]
      (   (ProgramTypeInt :=> ProgramTypeInt)
      :=> (ProgramTypeInt :=> ProgramTypeInt)
      )
stlcAPPLY
  = Lam (ProgramTypeFunctionSingleton ProgramTypeIntSingleton ProgramTypeIntSingleton)
  $ Lam ProgramTypeIntSingleton (App (Var (There Here)) (Var Here))

test01 = eval stlcAPPLY HNil (+1) 2
test02 = eval stlcID HNil 2

main :: IO ()
main = do
  print test01 -- 3
  print test02 -- 2