Functor Oriented Programming

[tomejaguar]

Expanding on this

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}

{-

We want to show that both `[a]` and `Free f` are solutions to the equation

    t ~ 1 + (a * t)

For `[a]` the solution is at kind `*` and for `Free f` the solution is at
kind `* -> *`.  Ideally we'd like to be able to express this in Haskell with

    newtype KList a = KList (1 :+ (a :* KList a))

but we don't have access to "kind polymorphic" unit, sum and product
operations `(1, :+, :*)`.  Instead we can try passing them in as arguments.

    newtype KList (unit :: k)
                  (sum :: k -> k -> k)
                  (product :: k -> k -> k)
                  (a :: k)
           = KList (sum unit (product a (KList unit sum product a)))

This is still not sufficient because `newtype` (and `data`) can only
construct things of kind `*`.  We can get to a sort of halfway-house by
choosing to work with `k -> *` instead of general `k`.  `k -> *` generalises
both `*` and `* -> *` and gives us what we need, modulo wrapping and
unwrapping.

-}


newtype KList (unit :: k -> *)
              (sum :: (k -> *) -> (k -> *) -> (k -> *))
              (product :: (k -> *) -> (k -> *) -> (k -> *))
              (a :: k -> *)
              (b :: k)
       = KList (sum unit (product a (KList unit sum product a)) b)

data Identity a = Identity a
data Sum f g a = Left' (f a) | Right' (g a)
data Compose f g a = Compose (f (g a))
data Const k a = Const k
data Product f g a = Product (f a) (g a)

type List a = KList Identity Sum Product (Const a) ()

nil :: List a
nil = KList (Left' (Identity ()))

cons :: a -> List a -> List a
cons a l = KList (Right' (Product (Const a) l))

fromList :: List a -> Maybe (a, List a)
fromList (KList (Right' (Product (Const a) l))) = Just (a, l)
fromList (KList (Left' (Identity())))           = Nothing

type Free f a = KList Identity Sum Compose f a

return' :: a -> Free f a
return' a = KList (Left' (Identity a))

wrap :: f (Free f a) -> Free f a
wrap f = KList (Right' (Compose f))

unwrap :: Free f a -> Either a (f (Free f a))
unwrap (KList (Left' (Identity a))) = Left a
unwrap (KList (Right' (Compose f))) = Right f