Skip to content

Instantly share code, notes, and snippets.

@LSLeary

LSLeary/Rec.hs

Last active January 24, 2026 09:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save LSLeary/98763e62f6fe4a2d629f74b38b9f2e45 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save LSLeary/98763e62f6fe4a2d629f74b38b9f2e45 to your computer and use it in GitHub Desktop.
Download ZIP
Almost obnoxious levels of duality in fixed-points.
Raw
Rec.hs
{-# LANGUAGE NoStarIsType, QuantifiedConstraints, BlockArguments, LambdaCase #-}
module Rec (
LFP, fold, inL , outL, rec,
GFP, unfold, outG, inG , corec,
HFunctor(..), FuncTrans,
LFPF, foldF, inLF , outLF, recF,
GFPF, unfoldF, outGF, inGF , corecF,
) where
import Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))
import Data.Kind (Type, Constraint)
import Control.Category ((>>>), (<<<))
import Control.Arrow ((&&&), (|||))
type FixPoint k = (k -> k) -> k
-- duality helpers
type (-->) = (->)
type a <-- b = b --> a
type (+) = Either
type (*) = (,)
type LFP :: FixPoint Type
newtype LFP f where
LFP :: { with :: forall x. f x --> x -> x } -> LFP f
type GFP :: FixPoint Type
data GFP f where
GFP :: { coalg :: f x <-- x, seed :: x } -> GFP f
fold :: f a --> a -> LFP f --> a
unfold :: f a <-- a -> GFP f <-- a
fold alg = \LFP{with} -> with alg
unfold coalg = GFP coalg
inL :: Functor f => f (LFP f) --> LFP f
outG :: Functor f => f (GFP f) <-- GFP f
inL fLFP = LFP \alg -> alg <<< fmap ( fold alg) $ fLFP
outG GFP{coalg,seed} = coalg >>> fmap (unfold coalg) $ seed
outL :: Functor f => LFP f --> f (LFP f)
inG :: Functor f => GFP f <-- f (GFP f)
outL = fold $ fmap inL
inG = unfold $ fmap outG
rec :: Functor f => f (LFP f * a) --> a -> LFP f --> a
corec :: Functor f => f (GFP f + a) <-- a -> GFP f <-- a
rec alg = snd <<< fold ((inL <<< fmap fst ) &&& alg)
corec coalg = Right >>> unfold ((outG >>> fmap Left) ||| coalg)
-- duality helpers
type f ~> g = forall x. f x --> g x
type f <~ g = forall x. f x <-- g x
type (|*|) = Product
type (|+|) = Sum
class HFunctor h where
hmap :: Functor f => f ~> g -> h f ~> h g
type FuncTrans h = forall f. Functor f => Functor (h f) :: Constraint
type LFPF :: FixPoint (Type -> Type)
newtype LFPF h a where
LFPF :: { withF :: forall f. Functor f => h f ~> f -> f a } -> LFPF h a
deriving Functor
type GFPF :: FixPoint (Type -> Type)
data GFPF h a where
GFPF :: Functor f => { coalgF :: h f <~ f, seedF :: f a } -> GFPF h a
deriving instance Functor (GFPF h)
foldF :: Functor f => h f ~> f -> LFPF h ~> f
unfoldF :: Functor f => h f <~ f -> GFPF h <~ f
foldF algF = \LFPF{withF} -> withF algF
unfoldF coalgF = GFPF coalgF
inLF :: HFunctor h => h (LFPF h) ~> LFPF h
outGF :: HFunctor h => h (GFPF h) <~ GFPF h
inLF fLFPF = LFPF \algF -> algF <<< hmap ( foldF algF) $ fLFPF
outGF GFPF{coalgF,seedF} = coalgF >>> hmap (unfoldF coalgF) $ seedF
outLF :: (HFunctor h, FuncTrans h) => LFPF h ~> h (LFPF h)
inGF :: (HFunctor h, FuncTrans h) => GFPF h <~ h (GFPF h)
outLF = foldF (hmap inLF )
inGF = unfoldF (hmap outGF)
recF :: (HFunctor h, Functor f) => h (LFPF h |*| f) ~> f -> LFPF h ~> f
corecF :: (HFunctor h, Functor f) => h (GFPF h |+| f) <~ f -> GFPF h <~ f
recF algF = sndF <<< foldF ((inLF <<< hmap fstF) ~&&&~ algF)
corecF coalgF = InR >>> unfoldF ((outGF >>> hmap InL ) ~|||~ coalgF)
-- more duality helpers
fstF :: f |*| g ~> f -- dual to InL :: f |+| g <~ f
sndF :: f |*| g ~> g -- dual to InR :: f |+| g <~ g
fstF (Pair fa _) = fa
sndF (Pair _ ga) = ga
(~&&&~) :: a --> f b -> a --> g b -> a --> (f |*| g) b
(~|||~) :: a <-- f b -> a <-- g b -> a <-- (f |+| g) b
f ~&&&~ g = \x -> Pair (f x) (g x)
f ~|||~ g = \case
InL fa -> f fa
InR ga -> g ga
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment