Permalink
Browse files

Add two mind-blowing examples of the nice generics library we can wri…

…te given only type functions
  • Loading branch information...
1 parent 882af68 commit 3bba012bbd9ba30b5e03903e234f889fcb694308 @batterseapower committed Oct 25, 2010
Showing with 353 additions and 0 deletions.
  1. +143 −0 Generics1.hs
  2. +210 −0 Generics2.hs
View
@@ -0,0 +1,143 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls, ScopedTypeVariables #-}
+
+import Data.Monoid
+
+
+type family Force a :: *
+
+data Forced (a :: *)
+type instance Force (Forced a) = a
+
+
+newtype VarF var term value = AVar { unVar :: String }
+
+data TermF var term value
+ = Var (Force var)
+ | App (Force term) (Force var)
+ | Value (Force value)
+ | Add (Force term) (Force term)
+
+data ValueF var term value
+ = Literal Int
+ | Lambda String (Force term)
+
+data SyntaxAlgebra var term value = SyntaxAlgebra {
+ varAlgebra :: VarF var term value -> Force var,
+ termAlgebra :: TermF var term value -> Force term,
+ valueAlgebra :: ValueF var term value -> Force value
+ }
+
+
+type Fix3_1 f g h = f (FixTag3_1 f g h) (FixTag3_2 f g h) (FixTag3_3 f g h)
+type Fix3_2 f g h = g (FixTag3_1 f g h) (FixTag3_2 f g h) (FixTag3_3 f g h)
+type Fix3_3 f g h = h (FixTag3_1 f g h) (FixTag3_2 f g h) (FixTag3_3 f g h)
+
+data FixTag3_1 f g h
+data FixTag3_2 f g h
+data FixTag3_3 f g h
+type instance Force (FixTag3_1 f g h) = Fix3_1 f g h
+type instance Force (FixTag3_2 f g h) = Fix3_2 f g h
+type instance Force (FixTag3_3 f g h) = Fix3_3 f g h
+
+
+type Var = Fix3_1 VarF TermF ValueF
+type Term = Fix3_2 VarF TermF ValueF
+type Value = Fix3_3 VarF TermF ValueF
+
+
+-- TODO: try doing this as a functor category?
+fmap3VarF :: (Force var -> Force var')
+ -> (Force term -> Force term')
+ -> (Force value -> Force value')
+ -> VarF var term value
+ -> VarF var' term' value'
+fmap3VarF _var _term _value x = case x of
+ AVar x -> AVar x
+
+fmap3TermF :: (Force var -> Force var')
+ -> (Force term -> Force term')
+ -> (Force value -> Force value')
+ -> TermF var term value
+ -> TermF var' term' value'
+fmap3TermF var term value e = case e of
+ Var x -> Var (var x)
+ App e x -> App (term e) (var x)
+ Value v -> Value (value v)
+ Add e1 e2 -> Add (term e1) (term e2)
+
+fmap3ValueF :: (Force var -> Force var')
+ -> (Force term -> Force term')
+ -> (Force value -> Force value')
+ -> ValueF var term value
+ -> ValueF var' term' value'
+fmap3ValueF _var term _value v = case v of
+ Literal l -> Literal l
+ Lambda x e -> Lambda x (term e)
+
+foldMap3VarF :: Monoid m
+ => (Force var -> m)
+ -> (Force term -> m)
+ -> (Force value -> m)
+ -> VarF var term value
+ -> m
+foldMap3VarF _var _term _value x = case x of
+ AVar _ -> mempty
+
+foldMap3TermF :: Monoid m
+ => (Force var -> m)
+ -> (Force term -> m)
+ -> (Force value -> m)
+ -> TermF var term value
+ -> m
+foldMap3TermF var term value e = case e of
+ Var x -> var x
+ App e x -> term e `mappend` var x
+ Value v -> value v
+ Add e1 e2 -> term e1 `mappend` term e2
+
+foldMap3ValueF :: Monoid m
+ => (Force var -> m)
+ -> (Force term -> m)
+ -> (Force value -> m)
+ -> ValueF var term value
+ -> m
+foldMap3ValueF _var term _value v = case v of
+ Literal _ -> mempty
+ Lambda _ e -> term e
+
+
+example :: Value
+example = Lambda "x" $ Add (Value (Literal 1)) (Var (AVar "x")) `App` AVar "x"
+
+
+-- fixAlgebra :: SyntaxAlgebra var term value -> SyntaxAlgebra (Fix3_1 var term value) (Fix3_2 var term value) (Fix3_3 var term value)
+-- fixAlgebra alg = undefined
+
+applyAlgebra :: forall var term value.
+ SyntaxAlgebra var term value
+ -> Term -> Force term
+ -- -> SyntaxAlgebra (FixTag3_1 VarF TermF ValueF) (FixTag3_2 VarF TermF ValueF) (FixTag3_3 VarF TermF ValueF)
+applyAlgebra alg = {- SyntaxAlgebra var term value -- -} term
+ where
+ var :: Var -> Force var
+ var = varAlgebra alg . fmap3VarF var term value
+ term :: Term -> Force term
+ term = termAlgebra alg . fmap3TermF var term value
+ value :: Value -> Force value
+ value = valueAlgebra alg . fmap3ValueF var term value
+
+
+instance Monoid Int where
+ mempty = 0
+ mappend = (+)
+
+main = print result
+ where
+ result = applyAlgebra alg (Value example)
+
+ alg :: SyntaxAlgebra (Forced Int) (Forced Int) (Forced Int)
+ alg = SyntaxAlgebra var term value
+
+ var x = 1 + foldMap3VarF id id id x
+ term e = 1 + foldMap3TermF id id id e
+ value v = 1 + foldMap3ValueF id id id v
View
@@ -0,0 +1,210 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
+
+import Data.Monoid
+
+
+type family ftag :% a :: *
+
+data Parametric0Tag (a :: *)
+type instance Parametric0Tag a :% () = a
+
+data Parametric1Tag (f :: * -> *)
+type instance Parametric1Tag f :% a = f a
+
+data Parametric3Tag (f :: * -> * -> * -> *)
+type instance Parametric3Tag f :% (a, b, c) = f a b c
+
+
+type Force a = a :% ()
+
+
+newtype VarF var term value = AVar { unVar :: String }
+
+data TermF var term value
+ = Var (Force var)
+ | App (Force term) (Force var)
+ | Value (Force value)
+ | Add (Force term) (Force term)
+
+data ValueF var term value
+ = Literal Int
+ | Lambda String (Force term)
+
+data SyntaxAlgebra var term value = SyntaxAlgebra {
+ varAlgebra :: VarF var term value -> Force var,
+ termAlgebra :: TermF var term value -> Force term,
+ valueAlgebra :: ValueF var term value -> Force value
+ }
+
+
+type Fix3_1 f g h = f :% (FixTag3_1 f g h, FixTag3_2 f g h, FixTag3_3 f g h) -- Using :% here requires UndecidableInstances -- fair enough!
+type Fix3_2 f g h = g :% (FixTag3_1 f g h, FixTag3_2 f g h, FixTag3_3 f g h)
+type Fix3_3 f g h = h :% (FixTag3_1 f g h, FixTag3_2 f g h, FixTag3_3 f g h)
+
+data FixTag3_1 f g h
+data FixTag3_2 f g h
+data FixTag3_3 f g h
+type instance FixTag3_1 f g h :% () = Fix3_1 f g h
+type instance FixTag3_2 f g h :% () = Fix3_2 f g h
+type instance FixTag3_3 f g h :% () = Fix3_3 f g h
+
+
+type Var = Fix3_1 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF)
+type Term = Fix3_2 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF)
+type Value = Fix3_3 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF)
+
+
+-- TODO: try doing this as a functor category?
+fmap3VarF :: (Force var -> Force var')
+ -> (Force term -> Force term')
+ -> (Force value -> Force value')
+ -> VarF var term value
+ -> VarF var' term' value'
+fmap3VarF _var _term _value x = case x of
+ AVar x -> AVar x
+
+fmap3TermF :: (Force var -> Force var')
+ -> (Force term -> Force term')
+ -> (Force value -> Force value')
+ -> TermF var term value
+ -> TermF var' term' value'
+fmap3TermF var term value e = case e of
+ Var x -> Var (var x)
+ App e x -> App (term e) (var x)
+ Value v -> Value (value v)
+ Add e1 e2 -> Add (term e1) (term e2)
+
+fmap3ValueF :: (Force var -> Force var')
+ -> (Force term -> Force term')
+ -> (Force value -> Force value')
+ -> ValueF var term value
+ -> ValueF var' term' value'
+fmap3ValueF _var term _value v = case v of
+ Literal l -> Literal l
+ Lambda x e -> Lambda x (term e)
+
+foldMap3VarF :: Monoid m
+ => (Force var -> m)
+ -> (Force term -> m)
+ -> (Force value -> m)
+ -> VarF var term value
+ -> m
+foldMap3VarF _var _term _value x = case x of
+ AVar _ -> mempty
+
+foldMap3TermF :: Monoid m
+ => (Force var -> m)
+ -> (Force term -> m)
+ -> (Force value -> m)
+ -> TermF var term value
+ -> m
+foldMap3TermF var term value e = case e of
+ Var x -> var x
+ App e x -> term e `mappend` var x
+ Value v -> value v
+ Add e1 e2 -> term e1 `mappend` term e2
+
+foldMap3ValueF :: Monoid m
+ => (Force var -> m)
+ -> (Force term -> m)
+ -> (Force value -> m)
+ -> ValueF var term value
+ -> m
+foldMap3ValueF _var term _value v = case v of
+ Literal _ -> mempty
+ Lambda _ e -> term e
+
+
+example :: Value
+example = Lambda "x" $ Add (Value (Literal 1)) (Var (AVar "x")) `App` AVar "x"
+
+
+-- fixAlgebra :: SyntaxAlgebra var term value -> SyntaxAlgebra (Fix3_1 var term value) (Fix3_2 var term value) (Fix3_3 var term value)
+-- fixAlgebra alg = undefined
+
+applyAlgebra :: forall var term value.
+ SyntaxAlgebra var term value
+ -> Term -> Force term
+ -- -> SyntaxAlgebra (FixTag3_1 VarF TermF ValueF) (FixTag3_2 VarF TermF ValueF) (FixTag3_3 VarF TermF ValueF)
+applyAlgebra alg = {- SyntaxAlgebra var term value -- -} term
+ where
+ var :: Var -> Force var
+ var = varAlgebra alg . fmap3VarF var term value
+ term :: Term -> Force term
+ term = termAlgebra alg . fmap3TermF var term value
+ value :: Value -> Force value
+ value = valueAlgebra alg . fmap3ValueF var term value
+
+
+applyHomAlgebra :: SyntaxAlgebra (Parametric0Tag Var) (Parametric0Tag Term) (Parametric0Tag Value)
+ -> Term -> Term
+applyHomAlgebra alg = term
+ where
+ var :: Var -> Var
+ var = varAlgebra alg . fmap3VarF var term value
+ term :: Term -> Term
+ term = termAlgebra alg . fmap3TermF var term value
+ value :: Value -> Value
+ value = valueAlgebra alg . fmap3ValueF var term value
+
+
+data IdTag
+type instance IdTag :% a = a
+
+data ComposeTag f g
+type instance ComposeTag f g :% a = f :% (g :% a)
+
+
+data Annotated ann a = Ann { annotation :: ann, annee :: a }
+
+instance Functor (Annotated ann) where
+ fmap f (Ann ann x) = Ann ann (f x)
+
+type AnnVar annftag = Fix3_1 (ComposeTag annftag (Parametric3Tag VarF)) (ComposeTag annftag (Parametric3Tag TermF)) (ComposeTag annftag (Parametric3Tag ValueF))
+type AnnTerm annftag = Fix3_2 (ComposeTag annftag (Parametric3Tag VarF)) (ComposeTag annftag (Parametric3Tag TermF)) (ComposeTag annftag (Parametric3Tag ValueF))
+type AnnValue annftag = Fix3_3 (ComposeTag annftag (Parametric3Tag VarF)) (ComposeTag annftag (Parametric3Tag TermF)) (ComposeTag annftag (Parametric3Tag ValueF))
+
+annotateWithAlgebra :: forall ann.
+ SyntaxAlgebra ann ann ann
+ -> Term -> AnnTerm (Parametric1Tag (Annotated (Force ann)))
+annotateWithAlgebra alg = term
+ where
+ foo :: VarF ann ann ann -> Force ann
+ foo = varAlgebra alg
+
+ -- Var == Fix3_1 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF)
+ -- == Parametric3Tag VarF :% (FixTag3_1 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF),
+ -- FixTag3_2 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF),
+ -- FixTag3_3 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF))
+ -- == VarF (FixTag3_1 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF))
+ -- (FixTag3_2 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF))
+ -- (FixTag3_3 (Parametric3Tag VarF) (Parametric3Tag TermF) (Parametric3Tag ValueF))
+
+ var :: Var -> AnnVar (Parametric1Tag (Annotated (Force ann)))
+ var x = Ann (varAlgebra alg (fmap3VarF annotation annotation annotation x')) x'
+ where x' = fmap3VarF var term value x
+ term :: Term -> AnnTerm (Parametric1Tag (Annotated (Force ann)))
+ term e = Ann (termAlgebra alg (fmap3TermF annotation annotation annotation e')) e'
+ where e' = fmap3TermF var term value e
+ value :: Value -> AnnValue (Parametric1Tag (Annotated (Force ann)))
+ value v = Ann (valueAlgebra alg (fmap3ValueF annotation annotation annotation v')) v'
+ where v' = fmap3ValueF var term value v
+
+
+instance Monoid Int where
+ mempty = 0
+ mappend = (+)
+
+main = do
+ print result
+ print (annotation example_annotated)
+ where
+ result = applyAlgebra alg (Value example)
+ example_annotated = annotateWithAlgebra alg (Value example)
+
+ alg :: SyntaxAlgebra (Parametric0Tag Int) (Parametric0Tag Int) (Parametric0Tag Int)
+ alg = SyntaxAlgebra var term value
+
+ var x = 1 + foldMap3VarF id id id x
+ term e = 1 + foldMap3TermF id id id e
+ value v = 1 + foldMap3ValueF id id id v

0 comments on commit 3bba012

Please sign in to comment.