Playing with higher-order free monads

Free.hs

{-# LANGUAGE
    DeriveFunctor,
    DerivingVia,
    StandaloneDeriving,
    DataKinds,
    PolyKinds,
    RankNTypes,
    InstanceSigs,
    GADTs,
    TypeFamilies,
    TypeOperators
  #-}
module Free where

import Control.Applicative
import Data.Kind

data Free f a where
  Pure :: a -> Free f a
  Impure :: f (Free f a) -> Free f a

deriving instance Functor f => Functor (Free f)
deriving via (WrappedMonad (Free f)) instance Functor f => Applicative (Free f)

instance Functor f => Monad (Free f) where
  return :: a -> Free f a
  return = Pure

  (>>=) :: Free f a -> (a -> Free f b) -> Free f b
  (>>=) u0 f = subst f u0 where
    subst f (Pure x) = f x
    subst f (Impure u) = Impure (fmap (subst f) u)

data Freer f a where
  Purer :: a -> Freer f a
  Impurer :: (x -> Freer f a) -> f x -> Freer f a

deriving instance Functor (Freer f)
deriving via (WrappedMonad (Freer f)) instance Applicative (Freer f)

instance Monad (Freer f) where
  return :: a -> Freer f a
  return = Purer

  (>>=) :: Freer f a -> (a -> Freer f b) -> Freer f b
  (>>=) u0 f = subst f u0 where
    subst f (Purer x) = f x
    subst f (Impurer u e) = Impurer (fmap (subst f) u) e

--         f              g
-- (~>) :: (k -> Type) -> (k -> Type) -> Type
type f ~> g = forall (a :: k). f a -> g a

foldFreer :: Monad m => (f ~> m) -> Freer f ~> m
foldFreer _ (Purer x) = pure x
foldFreer h (Impurer u e) = h e >>= fmap (foldFreer h) u

newtype Fix1 :: ((k -> Type) -> (k -> Type)) -> (k -> Type) where
  WrapFix1 :: f (Fix1 f) a -> Fix1 f a

data (f :: (k -> Type) -> (k -> Type)) :.+.: (g :: (k -> Type) -> (k -> Type))
  :: (k -> Type) -> k -> Type where
  L :: f w a -> (f :.+.: g) w a
  R :: g w a -> (f :.+.: g) w a

data Free1 :: ((k -> Type) -> (k -> Type)) -> (k -> Type) -> (k -> Type) where
  Pure1   :: w a -> Free1 f w a
  Impure1 :: f (Free1 f w) a -> Free1 f w a

class Functor1 (m :: (k -> Type) -> (k -> Type)) where
  map1 :: (p ~> q) -> (m p ~> m q)
  -- map = fmap

class Monad1 (m :: (k -> Type) -> (k -> Type)) where
  pure1 :: p ~> m p
  subst1 :: (p ~> m q) -> (m p ~> m q)
  -- A naming convention: subst = flip (>>=)

instance Functor1 f => Monad1 (Free1 f) where
  pure1 :: p ~> Free1 f p
  pure1 = Pure1

  subst1 :: (p ~> Free1 f q) -> (Free1 f p ~> Free1 f q)
  subst1 f (Pure1 x) = f x
  subst1 f (Impure1 u) = Impure1 (map1 (subst1 f) u)

instance Monad1 Freer where
  pure1 :: p ~> Freer p
  pure1 = Impurer Purer

  subst1 :: (p ~> Freer q) -> (Freer p ~> Freer q)
  subst1 = foldFreer

data Freer1 :: ((k -> Type) -> (k -> Type)) -> (k -> Type) -> (k -> Type) where
  Purer1   :: w a -> Freer1 f w a
  Impurer1 :: (x ~> Freer1 f w) -> f x a -> Freer1 f w a

instance Monad1 (Freer1 f) where
  pure1 :: p ~> Freer1 f p
  pure1 = Purer1

  subst1 :: (p ~> Freer1 f q) -> (Freer1 f p ~> Freer1 f q)
  subst1 f (Purer1 x) = f x
  subst1 f (Impurer1 u e) = Impurer1 (subst1 f . u) e

type f ~~> g = forall p a. f p a -> g p a

foldFree1 :: Monad1 m => (f ~~> m) -> (Free1 f ~~> m)
foldFree1 f (Pure1 x) = pure1 x
foldFree1 f (Impure1 u) = subst1 (foldFree1 f) (f u)

foldFreer1 :: Monad1 m => (f ~~> m) -> (Freer1 f ~~> m)
foldFreer1 f (Purer1 x) = pure1 x
foldFreer1 f (Impurer1 u e) = subst1 (foldFreer1 f . u) (f e)

type family Fst (ab :: (k1, k2)) :: k1 where
  Fst '(a, _) = a

type family Snd (ab :: (k1, k2)) :: k2 where
  Snd '(_, b) = b

newtype Uncurry1 :: (k1 -> k2 -> Type) -> ((k1, k2) -> Type) where
  WrapUncurry1 :: f (Fst ab) (Snd ab) -> Uncurry1 f ab

data Curry1 :: ((k1, k2) -> Type) -> k1 -> k2 -> Type where
  WrapCurry1 :: f ab -> Curry1 f (Fst ab) (Snd ab)

-- Freer1 with a lot of Curry
newtype SpicyFreer1 :: ((k -> Type, k) -> Type) -> ((k -> Type, k) -> Type) where
  WrapSpicyFreer1 :: Uncurry1 (Freer1 (Curry1 f)) s -> SpicyFreer1 f s

unwrapSpicyFreer1 :: SpicyFreer1 p ab -> Freer1 (Curry1 p) (Fst ab) (Snd ab)
unwrapSpicyFreer1 (WrapSpicyFreer1 (WrapUncurry1 u)) = u

instance Monad1 SpicyFreer1 where
  pure1 :: p ~> SpicyFreer1 p
  pure1 = WrapSpicyFreer1 . WrapUncurry1 . Impurer1 Purer1 . WrapCurry1

  subst1 :: (p ~> SpicyFreer1 q) -> (SpicyFreer1 p ~> SpicyFreer1 q)
  subst1 f (WrapSpicyFreer1 (WrapUncurry1 u)) =
    WrapSpicyFreer1 (WrapUncurry1
      (foldFreer1 (\(WrapCurry1 x) -> unwrapSpicyFreer1 (f x)) u))
  -- Looking past the wrapping...
  --   subst1 = foldFreer1

type StoreTy k = (k -> Type, k)
type Store k j = (k -> j, k)

-- fix :: (Store k j -> j) -> j
-- freer :: (Store (Store k j) j) -> j
-- freer :: ((k -> j) -> (k -> j)) -> (k -> j) -> k -> j
-- freer f w a = w a + f (freer f w) a

-- Identity1 :: (k -> Type) -> (k -> Type)
-- Identity1 :: StoreTy k -> Type

-- Freer1 :: (StoreTy k -> Type) -> (StoreTy k -> Type)
-- Freer1 :: StoreTy (StoreTy k) -> Type
--
-- Freer1 :: (StoreTy (StoreTy k) -> Type) -> (StoreTy (StoreTy k) -> Type)
-- Freer1 :: StoreTy (StoreTy (StoreTy k)) -> Type
--
-- StoreTy (StoreTy k) = ((k -> Type, k) -> Type, (k -> Type, k))