Type level recursion schemes

TLRecursionSchemes.hs

{-# 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