Skip to content
Browse files

lambda calculi a'la carte

  • Loading branch information...
1 parent 28fdfc8 commit 48a0a79872d8afeae85a35f71e68828239b41f9a @mak committed
Showing with 100 additions and 0 deletions.
  1. +100 −0 Types.hs
View
100 Types.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE
+ TypeOperators
+ , DeriveFunctor
+ , MultiParamTypeClasses
+ , FlexibleInstances
+ , OverlappingInstances
+ , NoMonomorphismRestriction
+ , IncoherentInstances
+ , OverloadedStrings
+ #-}
+
+module Types where
+
+import Data.Set (Set)
+import qualified Data.Set as S
+import GHC.Exts
+
+{-
+class Term t where
+ type V :: * -> *
+ eval :: t (T a) -> t (T a)
+ fv :: t (T a) -> Set (V a)
+ --subst :: t a -> v -> t1 -> t t1
+-}
+
+infixr :+:
+data (f :+: g ) a = Inl (f a) | Inr (g a)
+ deriving Functor
+newtype Fix f = In {out :: f (Fix f)}
+
+class (Functor sub, Functor sup) => sub :<: sup where
+ inj :: sub a -> sup a
+
+instance Functor f => (:<:) f f where
+ inj = id
+instance (Functor f , Functor g) => (:<:) f (f :+: g) where
+ inj = Inl
+instance (Functor f , Functor g, Functor h, f :<: g) => (:<:) f (h :+: g) where
+ inj = Inr . inj
+
+inject = In . inj
+
+cata phi = phi . fmap (cata phi) . out
+
+type VarE = Var ()
+
+class Term t where
+ fvAlg :: t (Set VarE) -> Set VarE
+ substAlg :: (t :<: t1) => t a -> Fix t1 -> VarE -> Fix t1
+
+ -- evalAlg :: t V -> V
+
+instance (Term f,Term g) => Term (f :+: g) where
+ fvAlg (Inl x) = fvAlg x
+ fvAlg (Inr x) = fvAlg x
+
+data Var a = Var String Int
+ deriving (Functor,Ord,Eq)
+
+var x n = inject $ Var x n
+castVar :: Var a -> Var b
+castVar (Var x n) = Var x n
+
+instance Show (Var v) where
+ show (Var v n) = v ++ show n
+
+instance IsString (Var v) where
+ fromString x = Var "x" 0
+
+instance Term Var where
+ fvAlg = S.singleton . castVar
+ substAlg v t w | castVar v == w = t
+ substAlg (Var x n) _ _ = var x n
+
+data Lam v a = Lam (Var v) a
+ deriving Functor
+lam x t = inject $ Lam x t
+
+instance Term (Lam v) where
+ fvAlg (Lam v s) = (castVar v) `S.delete` s
+
+instance (:<:) (Lam v) (Lam v1) where
+ inj (Lam v x) = Lam (castVar v) x
+
+data App t = App t t
+ deriving Functor
+app t1 t2 = inject $ App t1 t2
+
+instance Term App where
+ fvAlg (App s1 s2) = s1 `S.union` s2
+ substAlg (App t t2) v r = app (substAlg t v r) (substAlg t2 v r)
+
+type Expr v = Fix (Var :+: App :+: Lam v)
+
+test :: Expr v
+test = let x0 = var "x" 0
+ y0 = var "y" 0
+ in app (lam (Var "x" 0) x0) y0
+
+fv = cata fvAlg

0 comments on commit 48a0a79

Please sign in to comment.
Something went wrong with that request. Please try again.