Last active
October 11, 2018 10:14
-
-
Save yellowflash/662eef1cfce2d79c2bac212adfceb14b to your computer and use it in GitHub Desktop.
Purescript implementation of a dependent typed language.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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