Skip to content

Instantly share code, notes, and snippets.

@sjoerdvisscher

sjoerdvisscher/litorn.hs

Created December 22, 2010 16:16
Show Gist options
  • Save sjoerdvisscher/751702 to your computer and use it in GitHub Desktop.
Save sjoerdvisscher/751702 to your computer and use it in GitHub Desktop.
Download ZIP
Generic programming with indexed types (ala Conor McBride)
Raw
litorn.hs
{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, UndecidableInstances, RankNTypes, MultiParamTypeClasses, TypeSynonymInstances #-}
data End i
data Arg s r
data Rec i r
type family Apply f a :: *
data Univ desc is r i where
End :: is i -> Univ (End i) is r i
Arg :: s j -> Univ (Apply rest j) is r i -> Univ (Arg s rest) is r i
Rec :: r j -> Univ rest is r i -> Univ (Rec j rest) is r i
data Fix d is i = In { out :: Univ d is (Fix d is) i }
con :: is i -> (Univ (End i) is r i -> Univ d is (Fix d is) j) -> Fix d is j
con i f = In $ f (End i)
getIndex :: Fix d is i -> is i
getIndex (In x) = getIndex' x
where
getIndex' :: Univ d is r i -> is i
getIndex' (End i) = i
getIndex' (Arg _ rest) = getIndex' rest
getIndex' (Rec _ rest) = getIndex' rest
newtype K a i = K { unK :: a }
data Const d
type instance Apply (Const d) a = d
type l :*: r = Arg l (Const r)
data L
data R
data LR i where
L :: LR L
R :: LR R
data LRF l r
type instance Apply (LRF l r) L = l
type instance Apply (LRF l r) R = r
type l :+: r = Arg LR (LRF l r)
type x :~> y = forall i. x i -> y i
hmap :: (x :~> y) -> Univ d is x :~> Univ d is y
hmap _ (End i) = End i
hmap f (Arg s rest) = Arg s (hmap f rest)
hmap f (Rec x rest) = Rec (f x) (hmap f rest)
fold :: (Univ d is x :~> x) -> Fix d is :~> x
fold phi = phi . hmap (fold phi) . out
type NatD = End () :+: Rec () (End ())
type Nat = Fix NatD (K ()) ()
zero :: Nat
zero = con (K ()) $ Arg L
suc :: Nat -> Nat
suc n = con (K ()) $ Arg R . Rec n
addA :: Nat -> Univ NatD (K ()) (K Nat) :~> K Nat
addA y (Arg L (End _)) = K y
addA _ (Arg R (Rec (K n) (End _))) = K $ suc n
add :: Nat -> Nat -> Nat
add x y = unK $ fold (addA y) x
data Z
data S n
data N i where
Z :: N Z
S :: N n -> N (S n)
type family AddN a b :: *
type instance AddN Z b = b
type instance AddN (S n) b = S (AddN n b)
data VecF
type instance Apply VecF n = Rec n (End (S n))
type VecD a = End Z :+: (K a :*: Arg N VecF)
type Vec a = Fix (VecD a) N
nil :: Vec a Z
nil = con Z $ Arg L
cons :: a -> Vec a n -> Vec a (S n)
cons x xs = con (S n) $ Arg R . Arg (K x) . Arg n . Rec xs
where n = getIndex xs
data ConcatF a n m = ConcatF { getConcatF :: Vec a (AddN m n) }
concatA :: Vec a n -> Univ (VecD a) N (ConcatF a n) :~> ConcatF a n
concatA ys (Arg L (End _)) = ConcatF ys
concatA _ (Arg R (Arg (K x) (Arg _ (Rec (ConcatF xs) (End _))))) = ConcatF $ cons x xs
concat :: Vec a m -> Vec a n -> Vec a (AddN m n)
concat xs ys = getConcatF $ fold (concatA ys) xs
class Fam fam where
data DescF fam :: *
from :: fam a -> a -> Univ (Arg fam (DescF fam)) fam (I0 fam) a
to :: fam a -> Univ (Arg fam (DescF fam)) fam (I0 fam) a -> a
class IsFamMember fam a where proof :: fam a
newtype I0 fam a = I0 { unI0 :: IsFamMember fam a => a }
compos :: Fam fam => (forall a. fam a -> a -> a) -> fam a -> a -> a
compos f p = to p . hmap (\(I0 x) -> I0 $ f proof x) . from p
data Expr = Const Int
| Add Expr Expr
| Mul Expr Expr
| EVar Var
| Let Decl Expr
data Decl = Var := Expr
| Seq Decl Decl
type Var = String
data AST i where
Expr :: AST Expr
Decl :: AST Decl
Var :: AST Var
instance IsFamMember AST Expr where proof = Expr
instance IsFamMember AST Decl where proof = Decl
instance IsFamMember AST Var where proof = Var
type instance Apply (DescF AST) Expr =
(K Int :*: End Expr)
:+: (Rec Expr (Rec Expr (End Expr)))
:+: (Rec Expr (Rec Expr (End Expr)))
:+: (Rec Var (End Expr))
:+: (Rec Decl (Rec Expr (End Expr)))
type instance Apply (DescF AST) Decl =
(Rec Var (Rec Expr (End Decl)))
:+: (Rec Decl (Rec Decl (End Decl)))
type instance Apply (DescF AST) Var =
(K String :*: End Var)
instance Fam AST where
from Expr (Const i) = Arg Expr . Arg L . Arg L . Arg L . Arg L . Arg (K i) $ End Expr
from Expr (Add e1 e2) = Arg Expr . Arg L . Arg L . Arg L . Arg R . Rec (I0 e1) . Rec (I0 e2) $ End Expr
from Expr (Mul e1 e2) = Arg Expr . Arg L . Arg L . Arg R . Rec (I0 e1) . Rec (I0 e2) $ End Expr
from Expr (EVar v) = Arg Expr . Arg L . Arg R . Rec (I0 v) $ End Expr
from Expr (Let d e) = Arg Expr . Arg R . Rec (I0 d) . Rec (I0 e) $ End Expr
from Decl (v := e) = Arg Decl . Arg L . Rec (I0 v) . Rec (I0 e) $ End Decl
from Decl (Seq d1 d2) = Arg Decl . Arg R . Rec (I0 d1) . Rec (I0 d2) $ End Decl
from Var s = Arg Var . Arg (K s) $ End Var
to Expr (Arg Expr (Arg L (Arg L (Arg L (Arg L (Arg (K i) (End Expr))))))) = Const i
to Expr (Arg Expr (Arg L (Arg L (Arg L (Arg R (Rec (I0 e1) (Rec (I0 e2) (End Expr)))))))) = Add e1 e2
to Expr (Arg Expr (Arg L (Arg L (Arg R (Rec (I0 e1) (Rec (I0 e2) (End Expr))))))) = Mul e1 e2
to Expr (Arg Expr (Arg L (Arg R (Rec (I0 v) (End Expr))))) = EVar v
to Expr (Arg Expr (Arg R (Rec (I0 d) (Rec (I0 e) (End Expr))))) = Let d e
to Decl (Arg Decl (Arg L (Rec (I0 v) (Rec (I0 e) (End Decl))))) = v := e
to Decl (Arg Decl (Arg R (Rec (I0 d1) (Rec (I0 d2) (End Decl))))) = Seq d1 d2
to Var (Arg Var (Arg (K s) (End Var))) = s
renameVar :: Expr -> Expr
renameVar = renameVar' Expr
where
renameVar' :: AST a -> a -> a
renameVar' Var s = s ++ "_"
renameVar' p x = compos renameVar' p x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment