Skip to content

Instantly share code, notes, and snippets.

@themoritz

themoritz/IxFix.hs

Last active January 11, 2025 15:44
Show Gist options
  • Save themoritz/189907f2ee41c572554eb67ffda4b130 to your computer and use it in GitHub Desktop.
Save themoritz/189907f2ee41c572554eb67ffda4b130 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
IxFix.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Indexed 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
-- Product
data (f :*: g) r
= Pair (f r) (g r)
-- 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
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
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment