Purescript implementation of a dependent typed language.

Godel.purs

module Godel.Core where
  
import Control.Monad (bind, pure)
import Control.Monad.Eff.Console (log)
import Data.Either (Either(..))
import Data.Eq (class Eq, (==))
import Data.Map (Map, empty, insert, lookup)
import Data.Maybe (Maybe(..))
import Data.Show (class Show, show)
import Prelude (otherwise, negate, (+), (-), (>=), ($), (<>))

data Expr = Star | Var String Int | Lambda String Expr Expr | Pi String Expr Expr | App Expr Expr
data Ctx = Ctx Int (Map Int Judgement)
data Err = Err
data Judgement = Typed Expr Expr

derive instance eqExpr :: Eq Expr
instance showExpr :: Show Expr where
  show Star = "*"
  show (Var name _) = name
  show (Lambda pname ptype body) = "λ (" <> pname <> ": " <> (show ptype) <> "), " <> (show body)
  show (Pi pname ptype body) = "∀ (" <> pname <> ": " <> (show ptype) <> "), " <> (show body)
  show (App fn arg) = "(" <> (show fn) <> " " <> (show arg) <> ")"

instance showErr :: Show Err where
  show Err = "err"

instance showJudgement :: Show Judgement where
  show (Typed value typ) = (show value) <> ": " <> (show typ)

at :: Ctx -> Int -> Either Err Judgement
at (Ctx _ subs) index =  case lookup index subs of 
    (Just (Typed value typ)) -> Right $ Typed (shift 0 index value) (shift 0 index typ)
    Nothing -> Left Err

add :: Judgement -> Ctx -> Ctx
add judgement (Ctx depth subs) = Ctx (depth + 1) (insert depth judgement subs)

shift :: Int -> Int -> Expr -> Expr
shift _ _ Star = Star
shift n k (Var name index) | index >= n = Var name (index + k)
                            | otherwise = Var name index
shift n k (Lambda pname ptype body) = Lambda pname (shift n k ptype) (shift (n + 1) k body)
shift n k (Pi pname ptype body) = Pi pname (shift n k ptype) (shift (n + 1) k body)
shift n k (App fn arg) = App (shift n k fn) (shift n k arg)


unshift :: Int -> Expr -> Expr
unshift n = shift (negate n) 0

apply :: Ctx -> Judgement -> Judgement -> Either Err Judgement
apply ctx (Typed (Lambda _ _ body) (Pi _ ptype _)) (Typed argval argtype) 
        | ptype == argtype =  do
          (Typed bval btype) <- eval (add (Typed (shift 0 1 argval) (shift 0 1 argtype)) ctx) body
          eval ctx (unshift 1 bval)
apply ctx (Typed fn (Pi pname ptype btype)) (Typed argval argtype)
        | ptype == argtype = do 
          (Typed btval bttype) <- eval (add (Typed (shift 0 1 argval) (shift 0 1 argtype)) ctx) btype
          pure $ Typed (App fn argval) (Pi pname ptype (unshift 1 btval))
apply _ _ _ = Left Err


eval :: Ctx -> Expr -> Either Err Judgement
eval ctx Star = Right $ Typed Star Star
eval ctx (Var name index) = at ctx index
eval ctx (Lambda pname ptype body) = do
  (Typed ptvalue _) <- eval ctx ptype
  (Typed bvalue btype) <- eval (add (Typed (Var pname 0) ptvalue) ctx) body
  pure $ Typed (Lambda pname ptvalue bvalue) (Pi pname ptvalue btype)
eval ctx (Pi pname ptype body) = do
  (Typed ptvalue _) <- eval ctx ptype
  (Typed bvalue _) <- eval (add (Typed (Var pname 0) ptvalue) ctx) body
  pure $ Typed (Pi pname ptvalue bvalue) Star
eval ctx (App fn arg) = do
  fntyped <- eval ctx fn
  argtyped <- eval ctx arg
  apply ctx fntyped argtyped
    
main = log $ show $ eval (Ctx 0 empty) (Lambda "x" Star (App (Lambda "x" Star (Var "x" 0)) (Var "x" 0)))