themoritz · January 11, 2025 15:44 · Apr 5, 2017 · Apr 3, 2017 · Mar 31, 2017
diff --git a/IxFix.hs b/IxFix.hs
@@ -42,7 +42,7 @@ coproduct f g = \case
   L e -> f e
   R b -> g b
 
--- Indexed product
+-- Product
 data (f :*: g) r
   = Pair (f r) (g r)
 

diff --git a/IxFix.hs b/IxFix.hs
@@ -5,7 +5,7 @@
 {-# LANGUAGE RankNTypes    #-}
 {-# LANGUAGE TypeOperators #-}
 
-module IxFix where
+module Indexed where
 
 -- Natural transformation..
 infixr 5 ~>
@@ -24,7 +24,7 @@ newtype K a b = K { getK :: a }
   deriving (Functor)
 
 -- Indexed functors
-class IxFunctor (f :: (k -> *) -> (k -> *)) where
+class IxFunctor (f :: (k -> *) -> k -> *) where
   imap :: (a ~> b) -> (f a ~> f b)
 
 -- Indexed coproduct
@@ -42,6 +42,10 @@ coproduct f g = \case
   L e -> f e
   R b -> g b
 
+-- Indexed product
+data (f :*: g) r
+  = Pair (f r) (g r)
+
 -- Indexed fixed point
 newtype IxFix f i = Fix { unfix :: f (IxFix f) i }
 
@@ -59,6 +63,12 @@ ana coalg = Fix . imap (ana coalg) . coalg
 ana' :: IxFunctor f => (a .~> f (K a)) -> (a .~> IxFix f)
 ana' coalg = ana (coalg . getK) . K
 
+para :: IxFunctor f => (f (IxFix f :*: a) ~> a) -> (IxFix f ~> a)
+para alg = alg . imap (\r -> Pair r (para alg r)) . unfix
+
+para' :: IxFunctor f => (f (IxFix f :*: (K a)) ~>. a) -> (IxFix f ~>. a)
+para' alg = alg . imap (\r -> Pair r (para (K . alg) r)) . unfix
+
 -- AST -------------------------------------------------------------------------
 
 data AstIx = Expr | Binder
@@ -107,4 +117,4 @@ pretty = cata' (coproduct goExpr goBinder)
 --------------------------------------------------------------------------------
 
 main :: IO ()
-main = putStrLn $ pretty exampleAst
+main = putStrLn $ pretty exampleAst
diff --git a/IxFix.hs b/IxFix.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE DataKinds     #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GADTs         #-}
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TypeOperators #-}
+
+module IxFix where
+
+-- Natural transformation..
+infixr 5 ~>
+type f ~> g = forall i. f i -> g i
+
+-- .. with constant on the left
+infixr 5 .~>
+type f .~> g = forall i. f -> g i
+
+-- .. with constant on the right
+infixr 5 ~>.
+type f ~>. g = forall i. f i -> g
+
+-- Constant functor
+newtype K a b = K { getK :: a }
+  deriving (Functor)
+
+-- Indexed functors
+class IxFunctor (f :: (k -> *) -> (k -> *)) where
+  imap :: (a ~> b) -> (f a ~> f b)
+
+-- Indexed coproduct
+data (f :+: g) (r :: k -> *) (ix :: k)
+  = L (f r ix)
+  | R (g r ix)
+
+instance (IxFunctor f, IxFunctor g) => IxFunctor (f :+: g) where
+  imap f = \case
+    L x -> L (imap f x)
+    R x -> R (imap f x)
+
+coproduct :: (f r ix -> a) -> (g r ix -> a) -> (f :+: g) r ix -> a
+coproduct f g = \case
+  L e -> f e
+  R b -> g b
+
+-- Indexed fixed point
+newtype IxFix f i = Fix { unfix :: f (IxFix f) i }
+
+-- Recursion Schemes -----------------------------------------------------------
+
+cata :: IxFunctor f => (f a ~> a) -> (IxFix f ~> a)
+cata alg = alg . imap (cata alg) . unfix
+
+cata' :: IxFunctor f => (f (K a) ~>. a) -> (IxFix f ~>. a)
+cata' alg = getK . cata (K . alg)
+
+ana :: IxFunctor f => (a ~> f a) -> (a ~> IxFix f)
+ana coalg = Fix . imap (ana coalg) . coalg
+
+ana' :: IxFunctor f => (a .~> f (K a)) -> (a .~> IxFix f)
+ana' coalg = ana (coalg . getK) . K
+
+-- AST -------------------------------------------------------------------------
+
+data AstIx = Expr | Binder
+
+data ExprF (r :: AstIx -> *) (ix :: AstIx) where
+  Var :: String -> ExprF r 'Expr
+  Abs :: r 'Binder -> r 'Expr -> ExprF r 'Expr
+
+instance IxFunctor ExprF where
+  imap f = \case
+    Var t -> Var t
+    Abs binder a -> Abs (f binder) (f a)
+
+data BinderF (r :: AstIx -> *) (ix :: AstIx) where
+  VarBinder :: String -> BinderF r 'Binder
+  ConstructorBinder :: String -> [r 'Binder] -> BinderF r 'Binder
+
+instance IxFunctor BinderF where
+  imap f = \case
+    VarBinder t -> VarBinder t
+    ConstructorBinder t bs -> ConstructorBinder t (map f bs)
+
+type Ast = IxFix (ExprF :+: BinderF)
+
+-- Usage -----------------------------------------------------------------------
+
+exampleAst :: Ast 'Expr
+exampleAst = Fix $ L $ Abs constrBinder var
+  where
+    var = Fix $ L $ Var "baz"
+    constrBinder = Fix $ R $ ConstructorBinder "bar" [binder]
+    binder = Fix $ R $ VarBinder "foo"
+
+pretty :: Ast i -> String
+pretty = cata' (coproduct goExpr goBinder)
+  where
+  goExpr :: ExprF (K String) ~>. String
+  goExpr = \case
+    Var t -> t
+    Abs (K b) (K e) -> "\\" ++ b ++ " -> " ++ e
+  goBinder :: BinderF (K String) ~>. String
+  goBinder = \case
+    VarBinder t -> t
+    ConstructorBinder t bs -> t ++ mconcat (map ((" " ++ ) . getK) bs)
+
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main = putStrLn $ pretty exampleAst