Created
April 16, 2021 08:01
-
-
Save AndrasKovacs/ab9d89b6a710f2014e8d3273c89db411 to your computer and use it in GitHub Desktop.
NbE with case commutation for sum types
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
{-# language Strict, BangPatterns, LambdaCase, ViewPatterns, OverloadedStrings #-} | |
{-# options_ghc -Wincomplete-patterns #-} | |
-- NbE with case commutation for sum types. | |
import Data.Maybe | |
import Data.String | |
type Name = String | |
data Tm | |
= Var Name | |
| App Tm Tm | |
| Lam Name Tm | |
| Let Name Tm Tm | |
| Unit | |
| Case Tm Name Tm Name Tm | |
| Inl Tm | |
| Inr Tm | |
deriving Show | |
data Val | |
= VVar Name | |
| VApp Val Val | |
| VLam Name (Val -> Val) | |
| VUnit | |
| VCase Val Name (Val -> Val) Name (Val -> Val) | |
| VInl Val | |
| VInr Val | |
type Env = [(Name, Val)] | |
app :: Val -> Val -> Val | |
app t u = case t of | |
VLam _ t -> t u | |
VCase t x l y r -> VCase t x (\v -> app (l v) u) | |
y (\v -> app (r v) u) | |
t -> VApp t u | |
vcase :: Val -> Name -> (Val -> Val) -> Name -> (Val -> Val) -> Val | |
vcase t x l y r = case t of | |
VInl t -> l t | |
VInr t -> r t | |
VCase t x' l' y' r' -> VCase t x' (\u -> vcase (l' u) x l y r) | |
y' (\u -> vcase (r' u) x l y r) | |
t -> VCase t x l y r | |
eval :: Env -> Tm -> Val | |
eval env t = let | |
go = eval env | |
goBind x t u = eval ((x, u):env) t | |
in case t of | |
Var x -> fromJust $ lookup x env | |
App t u -> app (go t) (go u) | |
Lam x t -> VLam x (goBind x t) | |
Let x t u -> goBind x u (go t) | |
Unit -> VUnit | |
Case t x l y r -> vcase (go t) x (goBind x l) y (goBind y r) | |
Inl t -> VInl (go t) | |
Inr t -> VInr (go t) | |
quote :: [Name] -> Val -> Tm | |
quote ns t = let | |
go = quote ns | |
goBind x t = quote (x:ns) (t (VVar x)) | |
fsh x | elem x ns = fsh (x ++ "'") | |
| True = x | |
in case t of | |
VVar x -> Var x | |
VApp t u -> App (go t) (go u) | |
VLam (fsh -> x) t -> Lam x (goBind x t) | |
VUnit -> Unit | |
VCase t (fsh -> x) l (fsh -> y) r -> Case (go t) x (goBind x l) y (goBind y r) | |
VInl t -> Inl (go t) | |
VInr t -> Inr (go t) | |
nf :: Tm -> Tm | |
nf = quote [] . eval [] | |
-------------------------------------------------------------------------------- | |
instance IsString Tm where fromString = Var | |
infixl 7 $$ | |
($$) = App | |
ite b t f = Case b "_" t "_" f | |
true = Inl Unit | |
false = Inr Unit | |
comp = Lam "f" $ Lam "g" $ Lam "x" $ "f" $$ ("g" $$ "x") | |
not' = Lam "b" $ ite "b" false true |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment