Free.hs

{-# OPTIONS_GHC -fglasgow-exts #-}
{-# Language LambdaCase #-}
{-# Language TypeApplications #-}
{-# Language ScopedTypeVariables #-}
{-# Language ExplicitForAll #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language TypeFamilies #-}
{-# Language DataKinds #-}
{-# Language EmptyCase #-}
{-# Language UndecidableInstances #-}

module Free where

import Control.Category
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Reader

import Prelude hiding (and, (.), id)

-- Natural Transformation.
--
newtype f ~> g = Nat { runNat :: forall x. f x -> g x }

instance Category (~>) where
    id = Nat id

    Nat f . Nat g = Nat (f . g)

-- Isomorphism.
--
data f <~> g = (:<~>) { iForth :: f ~> g, iBack :: g ~> f }

(<~>) :: (forall x. f x -> g x) -> (forall x. g x -> f x) -> f <~> g
forth <~> back = Nat forth :<~> Nat back

infix 4 <~>, :<~>

instance Category (<~>) where
    id = id <~> id

    (a :<~> b) . (c :<~> d) = a . c :<~> d . b

-- Groupoid inversion.
--
inv :: (f <~> g) -> (g <~> f)
inv (a :<~> b) = (b :<~> a)

-- Functor sum.
--
data (f :\/ g) a = InL (f a) | InR (g a)
    deriving (Functor, Foldable, Traversable)

type (\/) = (:\/)

infixr 5 \/

-- Sum eliminator.
--
(\/) :: (f a -> c) -> (g a -> c) -> ((f \/ g) a -> c)
left \/ right = \case
    InL f -> left f
    InR g -> right g

-- Merging 2 transforms into transform of sum.
--
bimapping :: (f ~> g) -> (e ~> h) -> (f \/ e) ~> (g \/ h)
bimapping (Nat left) (Nat right) = Nat $ InL . left \/ InR . right

-- Merging 2 isos into transform of sum.
--
bimapped :: (f <~> g) -> (e <~> h) -> (f \/ e) <~> (g \/ h)
bimapped (a :<~> b) (c :<~> d) =
    bimapping a c :<~> bimapping b d

-- Commutativity.
--
commuted :: (f \/ (g \/ h)) <~> (g \/ (f \/ h))
commuted = commute :<~> commute

-- Commutativity.
--
commute :: (f \/ (g \/ h)) ~> (g \/ (f \/ h))
commute = Nat $ InR . InL \/ InL \/ InR . InR

-- Associativity.
--
assoc :: ((f \/ g) \/ h) <~> (f \/ (g \/ h))
assoc = (InL \/ InR . InL) \/ InR . InR
     <~> InL . InL \/ (InL . InR \/ InR)

-- Neutral element for sum.
--
data Empty a
    deriving (Functor, Foldable, Traversable)

-- x == 0 + x, left unit.
--
unit :: g <~> (Empty \/ g)
unit = InR <~> (\case) \/ id

-- Isomorphism applies to given side of the sum.
--
left  :: (a <~> b) -> (a \/ x) <~> (b \/ x)
right :: (a <~> b) -> (x \/ a) <~> (x \/ b)
left  (forth :<~> back) = bimapping forth id :<~> bimapping back id
right (forth :<~> back) = bimapping id forth :<~> bimapping id back

-- Transform applies to given side of the sum.
--
leanLeft  :: (a ~> b) -> (a \/ x) ~> (b \/ x)
leanRight :: (a ~> b) -> (x \/ a) ~> (x \/ b)
leanLeft  forth = bimapping forth id
leanRight forth = bimapping id forth

-- Attempt to make a Union of given functors.
--
data family   AnyOf           :: [* -> *] -> * -> *
data instance AnyOf '[]      a = End { getEnd :: Empty          a }
data instance AnyOf (f ': g) a = Or  { getOr  :: (f \/ AnyOf g) a }

-- Coinduction end.
--
nil :: Empty <~> AnyOf '[]
nil = End <~> getEnd

-- Conduction step.
--
cons :: (f \/ AnyOf g) <~> AnyOf (f ': g)
cons = Or <~> getOr

-- Isomorphism between list and unfolded sum.
--
class List xs effs | xs -> effs, effs -> xs where
    list :: AnyOf xs <~> effs

instance List '[] Empty where
    list = inv nil

instance List xs effs => List (x ': xs) (x \/ effs) where
    list = inv cons >>> right list

-- Member x xs b a == (b ++ [x] ++ a =:= xs).
--
-- Commenting out "x xs -> b a" makes it compile, but then "interpret"
--  is unable to infer "b" and "a"
--
class Member x xs b a | x b a -> xs, x xs -> b a where
    split :: xs <~> (b \/ (x \/ a))

instance {-# OVERLAPPING #-}
    Member x (x \/ xs) Empty xs
  where
    split = unit

instance
    Member f xs b a
  =>
    Member f (g \/ xs) (g \/ b) a
  where
    split = right split
        >>> inv assoc

-- If there is an effect "f", and we can transform it into "g", make transformation
--  prserving order of the effects.
--
transform :: forall f g effs0 effs1 b a. (Member f effs0 b a, Member g effs1 b a) => (f ~> g) -> (effs0 ~> effs1)
transform nat
    =   iForth    (split @f @effs0 @b @a)
    >>> leanRight (leanLeft nat)
    >>> iBack     (split @g @effs1 @b @a)

-- Monomorphised version of the "transform".
--
interpret :: (f ~> g) -> (f \/ effs) ~> (g \/ effs)
interpret = transform

-- -- interpret :: (f ~> m) -> (g ~> m) -> (f \/ g) ~> m
-- -- interpret = select

-- -- readline :: IO <: effs => effs String
-- -- readline = inject getLine

-- -- env :: Reader env <: effs => effs env
-- -- env = inject (ask :: Reader env env)

-- -- with :: forall env effs a. State env <: effs => Monad effs => (env -> env) -> effs a -> effs a
-- -- with f action = do
-- --     was <- inject (get @env :: State env env)
-- --     inject (modify f :: State env ())
-- --     res <- action
-- --     inject (put was :: State env ())
-- --     return res