Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- — explicit type recursion with functors and catamorphisms
- newtype Mu f = In (f (Mu f))
- unIn (In x) = x
- cata phi = phi . fmap (cata phi) . unIn
- — base functor and data type for natural numbers,
- — using locally-defined «eliminators»
- data N c = Z | S c
- instance Functor N where
- fmap g Z = Z
- fmap g (S x) = S (g x)
- type Nat = Mu N
- zero = In Z
- suck n = In (S n)
- add m = cata phi where
- phi Z = m
- phi (S f) = suck f
- mult m = cata phi where
- phi Z = zero
- phi (S f) = add m f
- — explicit products and their functorial action
- data Prod e c = Pair c e
- outl (Pair x y) = x
- outr (Pair x y) = y
- fork f g x = Pair (f x) (g x)
- instance Functor (Prod e) where
- fmap g = fork (g . outl) outr
- — comonads, the categorical «opposite» of monads
- class Functor n => Comonad n where
- extr :: n a -> a
- dupl :: n a -> n (n a)
- instance Comonad (Prod e) where
- extr = outl
- dupl = fork id outr
- gcata :: (Functor f, Comonad n) =>
- (forall a. f (n a) -> n (f a))
- -> (f (n c) -> c) -> Mu f -> c
- gcata dist phi = extr . cata (fmap phi . dist . fmap dupl)
- zygo chi = gcata (fork (fmap outl) (chi . fmap outr))
- para :: Functor f => (f (Prod (Mu f) c) -> c) -> Mu f -> c
- para = zygo In
- fac = para phi where
- phi Z = suck zero
- phi (S (Pair f n)) = mult f (suck n)
- int = cata phi where
- phi Z = 0
- phi (S f) = 1 + f
- instance Show (Mu N) where
- show = show . int
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement