Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Type-level glambda
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Requires GHC 8.8 or later
module TypeLevelGlambda where
import Data.Kind
type FlipConst a b = b
data ArithOp :: Type -> Type where
Plus, Minus, Times, Divide, Mod :: ArithOp Int
Less, LessE, Greater, GreaterE, Equals :: ArithOp Bool
data Elem :: forall a. [a] -> a -> Type where
EZ :: Elem (x:xs) x
ES :: Elem xs x -> Elem (y:xs) x
data Exp :: [Type] -> Type -> Type where
Var :: Elem ctx ty -> Exp ctx ty
Lam :: Exp (arg:ctx) res -> Exp ctx (arg -> res)
App :: Exp ctx (arg -> res) -> Exp ctx arg -> Exp ctx res
Arith :: Exp ctx Int -> ArithOp ty -> Exp ctx Int -> Exp ctx ty
Cond :: Exp ctx Bool -> Exp ctx ty -> Exp ctx ty -> Exp ctx ty
Fix :: Exp ctx (ty -> ty) -> Exp ctx ty
IntE :: Int -> Exp ctx Int
BoolE :: Bool -> Exp ctx Bool
infixr 5 ++, `LenProp`
type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
'[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)
data LenProp :: forall a. [a] -> [a] -> [a] -> Type where
LenNil :: ('[] `LenProp` ys) ys
LenCons :: (xs `LenProp` ys) r -> ((x:xs) `LenProp` ys) (x:r)
type family Shift (e :: Exp ts2 ty) :: Exp (t:ts2) ty where
Shift e = ShiftGo LenNil e
type family ShiftGo (lp :: FlipConst t ((ts1 `LenProp` ts2) r))
(e :: Exp r ty) :: Exp (ts1 ++ t:ts2) ty where
ShiftGo @t lp (Var v) = Var (ShiftElem @t lp v)
ShiftGo @t lp (Lam body) = Lam (ShiftGo @t (LenCons lp) body)
ShiftGo @t lp (App e1 e2) = App (ShiftGo @t lp e1) (ShiftGo @t lp e2)
ShiftGo @t lp (Arith e1 op e2) = Arith (ShiftGo @t lp e1) op (ShiftGo @t lp e2)
ShiftGo @t lp (Cond e1 e2 e3) = Cond (ShiftGo @t lp e1) (ShiftGo @t lp e2) (ShiftGo @t lp e3)
ShiftGo @t lp (Fix e) = Fix (ShiftGo @t lp e)
ShiftGo @_ _ (IntE n) = IntE n
ShiftGo @_ _ (BoolE b) = BoolE b
type family ShiftElem (lp :: FlipConst t ((ts1 `LenProp` ts2) r))
(e :: Elem r x) :: Elem (ts1 ++ t:ts2) x where
ShiftElem @_ LenNil e = ES e
ShiftElem @_ (LenCons _) EZ = EZ
ShiftElem @t (LenCons l) (ES e) = ES (ShiftElem @t l e)
type family Subst (exp1 :: Exp ts2 s) (exp2 :: Exp (s:ts2) t) :: Exp ts2 t where
Subst exp1 exp2 = SubstGo exp1 LenNil exp2
type family SubstGo (exp1 :: Exp ts2 s)
(lp :: (ts1 `LenProp` s:ts2) r)
(exp2 :: Exp r t) :: Exp (ts1 ++ ts2) t where
SubstGo e len (Var v) = SubstVar e len v
SubstGo e len (Lam body) = Lam (SubstGo e (LenCons len) body)
SubstGo e len (App e1 e2) = App (SubstGo e len e1) (SubstGo e len e2)
SubstGo e len (Arith e1 op e2) = Arith (SubstGo e len e1) op (SubstGo e len e2)
SubstGo e len (Cond e1 e2 e3) = Cond (SubstGo e len e1) (SubstGo e len e2) (SubstGo e len e3)
SubstGo e len (Fix e') = Fix (SubstGo e len e')
SubstGo _ _ (IntE n) = IntE n
SubstGo _ _ (BoolE b) = BoolE b
type family SubstVar (exp :: Exp ts2 s)
(lp :: (ts1 `LenProp` s:ts2) r)
(el :: Elem r t) :: Exp (ts1 ++ ts2) t where
SubstVar e LenNil EZ = e
SubstVar _ LenNil (ES v) = Var v
SubstVar _ (LenCons _) EZ = Var EZ
SubstVar e (LenCons len) (ES v) = Shift (SubstVar e len v)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment