Skip to content

Instantly share code, notes, and snippets.

@yellowflash
Last active Oct 11, 2018
Embed
What would you like to do?
Purescript implementation of a dependent typed language.
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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment