Skip to content

Instantly share code, notes, and snippets.

@xgrommx
Last active January 19, 2021 19:06
Show Gist options
  • Save xgrommx/2e128a1130bce7d6cf891fa046eab500 to your computer and use it in GitHub Desktop.
Save xgrommx/2e128a1130bce7d6cf891fa046eab500 to your computer and use it in GitHub Desktop.
Type level recursion schemes
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module TLRecursionSchemes where
import qualified GHC.TypeLits as TL
import Fcf ( If, Map, type (=<<), type (@@), Eval, Exp, type (<=), type (>) )
import Fcf.Data.Nat ( Nat, type (<=), type (>) )
import Data.Type.Equality ( type (:~:)(..) )
data ListF a b = ConsF a b | NilF
type instance Eval (Map f 'NilF) = 'NilF
type instance Eval (Map f ('ConsF a b)) = 'ConsF a (Eval (f b))
type family Base (t :: k) :: k -> k
type instance Base [a] = ListF a
newtype Fix f = Fix (f (Fix f))
type instance Base (Fix a) = a
data Project :: a -> Exp (Base a a)
type instance Eval (Project '[]) = 'NilF
type instance Eval (Project (x ': xs)) = 'ConsF x xs
type instance Eval (Project ('Fix a)) = a
data Embed :: Base a a -> Exp a
type instance Eval (Embed 'NilF) = '[]
type instance Eval (Embed ('ConsF x xs)) = x ': xs
type instance Eval (Embed a) = 'Fix a
type Algebra f a = f a -> Exp a
type GAlgebra w f a = f (w a) -> Exp a
type PAlgebra f a = GAlgebra ((,) f) (Base f) a
type CoAlgebra f a = a -> Exp (f a)
data Cata :: Algebra (Base t) a -> t -> Exp a
type instance Eval (Cata alg x) = alg @@ Eval (Map (Cata alg) (Project @@ x))
data ParaH :: PAlgebra t a -> t -> Exp (t, a)
type instance Eval (ParaH alg x) = '(x, Para alg @@ x)
data Para :: PAlgebra t a -> t -> Exp a
type instance Eval (Para alg x) = alg @@ Eval (Map (ParaH alg) (Project @@ x))
data Ana :: CoAlgebra (Base t) a -> a -> Exp t
type instance Eval (Ana coalg a) = Embed @@ Eval (Map (Ana coalg) (coalg @@ a))
data LengthAlg :: Algebra (ListF a) Nat
type instance Eval (LengthAlg 'NilF) = 0
type instance Eval (LengthAlg ('ConsF a b)) = 1 TL.+ b
data Length :: [a] -> Exp Nat
type instance Eval (Length as) = Cata LengthAlg @@ as
-- >>> :kind! (Eval (Length '[1,2,3,4,5]))
-- (Eval (Length '[1,2,3,4,5])) :: Nat
-- = 5
data RangeCoalg :: CoAlgebra (ListF Nat) Nat
type instance Eval (RangeCoalg n) = If (Eval (n > 0)) ('ConsF n (n TL.- 1)) 'NilF
data Range :: Nat -> Exp [Nat]
type instance Eval (Range n) = Ana RangeCoalg @@ n
-- >>> :kind! (Eval (Range 10) :: [Nat])
-- (Eval (Range 10) :: [Nat]) :: [Nat]
-- = '[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]
data TakeCoalg :: CoAlgebra (ListF a) ([a], Nat)
type instance Eval (TakeCoalg '( '[], n)) = 'NilF
type instance Eval (TakeCoalg '(x ': xs, n)) = If (Eval (n <= 0)) 'NilF ('ConsF x '(xs, n TL.- 1))
data Take :: Nat -> [a] -> Exp [a]
type instance Eval (Take n as) = Ana TakeCoalg @@ '(as, n)
-- >>> :kind! (Eval (Take 4 '[1,2,3,4,5]))
-- (Eval (Take 4 '[1,2,3,4,5])) :: [Nat]
-- = '[1, 2, 3, 4]
data TailsAlg :: PAlgebra [a] [[a]]
type instance Eval (TailsAlg 'NilF) = '[]
type instance Eval (TailsAlg ('ConsF a '(as, res))) = (a ': as) ': res
data Tails :: [a] -> Exp [[a]]
type instance Eval (Tails as) = Para TailsAlg @@ as
-- >>> :kind! Eval (Tails '[1,2,3])
-- Eval (Tails '[1,2,3]) :: [[Nat]]
-- = '[ '[1, 2, 3], '[2, 3], '[3]]
data SlidingAlg :: Nat -> PAlgebra [a] [[a]]
type instance Eval (SlidingAlg _ 'NilF) = '[]
type instance Eval (SlidingAlg n ('ConsF a '(as, past))) = Eval (Take n (a ': as)) ': past
data Sliding :: Nat -> [a] -> Exp [[a]]
type instance Eval (Sliding n as) = Para (SlidingAlg n) @@ as
-- >>> :kind! Eval (Sliding 2 '[1,2,3,4,5,6,7])
-- Eval (Sliding 2 '[1,2,3,4,5,6,7]) :: [[Nat]]
-- = '[ '[1, 2], '[2, 3], '[3, 4], '[4, 5], '[5, 6], '[6, 7], '[7]]
type family Rewrite (e :: a :~: b) (x :: a) :: b
type instance Rewrite Refl x = x
data ToFixH :: (Fix (Base t) :~: y) -> t -> Exp y
type instance Eval (ToFixH p x) = Rewrite p (Cata Embed @@ x)
type ToFix = ToFixH Refl
data FromFix :: Fix (Base t) -> Exp t
type instance Eval (FromFix x) = Cata Embed @@ x
-- >>> :kind! (FromFix @@ (ToFix @@ [1,2,3,4,5,6,7]) :: [Nat])
-- (FromFix @@ (ToFix @@ [1,2,3,4,5,6,7]) :: [Nat]) :: [Nat]
-- = '[1, 2, 3, 4, 5, 6, 7]
data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a
type instance Eval (Hylo alg coalg a) = Eval (alg =<< Map (Hylo alg coalg) =<< coalg a)
data LengthAndRange :: Nat -> Exp Nat
type instance Eval (LengthAndRange n) = Hylo LengthAlg RangeCoalg @@ n
-- >>> :kind! (Eval (LengthAndRange 100))
-- (Eval (LengthAndRange 100)) :: Nat
-- = 100
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment