{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -fno-warn-all-missed-specialisations #-}
{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}

-- Inspired on Data types a la carte

module Free.AlaCarte where

import Data.Kind

infixr 8 :+:

type (:+:) :: forall {k}. (k -> Type) -> (k -> Type) -> k -> Type
data (f :+: g) e = Left' (f e) | Right' (g e) deriving ((forall a b. (a -> b) -> (:+:) f g a -> (:+:) f g b)
-> (forall a b. a -> (:+:) f g b -> (:+:) f g a)
-> Functor (f :+: g)
forall a b. a -> (:+:) f g b -> (:+:) f g a
forall a b. (a -> b) -> (:+:) f g a -> (:+:) f g b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
a -> (:+:) f g b -> (:+:) f g a
forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> (:+:) f g a -> (:+:) f g b
$cfmap :: forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> (:+:) f g a -> (:+:) f g b
fmap :: forall a b. (a -> b) -> (:+:) f g a -> (:+:) f g b
$c<$ :: forall (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
a -> (:+:) f g b -> (:+:) f g a
<$ :: forall a b. a -> (:+:) f g b -> (:+:) f g a
Functor)

type (:<:) :: (Type -> Type) -> (Type -> Type) -> Constraint
class (Functor sub, Functor sup) => sub :<: sup where
  inj :: sub a -> sup a
  prj :: sup a -> Maybe (sub a)

instance (Functor f) => f :<: f where
  {-# INLINEABLE inj #-}
  inj :: f a -> f a
  inj :: forall a. f a -> f a
inj = f a -> f a
forall a. a -> a
id

  {-# INLINEABLE prj #-}
  prj :: f a -> Maybe (f a)
  prj :: forall a. f a -> Maybe (f a)
prj = f a -> Maybe (f a)
forall a. a -> Maybe a
Just

instance (Functor f, Functor g) => f :<: (f :+: g) where
  {-# INLINEABLE inj #-}
  inj :: f a -> (f :+: g) a
  inj :: forall a. f a -> (:+:) f g a
inj = f a -> (:+:) f g a
forall {k} (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Left'

  {-# INLINEABLE prj #-}
  prj :: (f :+: g) a -> Maybe (f a)
  prj :: forall a. (:+:) f g a -> Maybe (f a)
prj = \case
    Left' f a
e -> f a -> Maybe (f a)
forall a. a -> Maybe a
Just f a
e
    Right' g a
_e -> Maybe (f a)
forall a. Maybe a
Nothing

instance {-# OVERLAPPABLE #-} (Functor f, Functor g, f :<: g, Functor h) => f :<: (h :+: g) where
  {-# INLINEABLE inj #-}
  inj :: f a -> (h :+: g) a
  inj :: forall a. f a -> (:+:) h g a
inj = g a -> (:+:) h g a
forall {k} (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Right' (g a -> (:+:) h g a) -> (f a -> g a) -> f a -> (:+:) h g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
forall a. f a -> g a
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj

  {-# INLINEABLE prj #-}
  prj :: (h :+: g) a -> Maybe (f a)
  prj :: forall a. (:+:) h g a -> Maybe (f a)
prj = \case
    Left' h a
_e -> Maybe (f a)
forall a. Maybe a
Nothing
    Right' g a
e -> g a -> Maybe (f a)
forall a. g a -> Maybe (f a)
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sup a -> Maybe (sub a)
prj g a
e

type Free :: (Type -> Type) -> Type -> Type
data Free f a
  = Pure a
  | Impure (f (Free f a))
  deriving ((forall a b. (a -> b) -> Free f a -> Free f b)
-> (forall a b. a -> Free f b -> Free f a) -> Functor (Free f)
forall a b. a -> Free f b -> Free f a
forall a b. (a -> b) -> Free f a -> Free f b
forall (f :: * -> *) a b. Functor f => a -> Free f b -> Free f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Free f a -> Free f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Free f a -> Free f b
fmap :: forall a b. (a -> b) -> Free f a -> Free f b
$c<$ :: forall (f :: * -> *) a b. Functor f => a -> Free f b -> Free f a
<$ :: forall a b. a -> Free f b -> Free f a
Functor)

instance (Functor f) => Applicative (Free f) where
  {-# INLINEABLE pure #-}
  pure :: a -> Free f a
  pure :: forall a. a -> Free f a
pure = a -> Free f a
forall (f :: * -> *) a. a -> Free f a
Pure

  {-# INLINEABLE (<*>) #-}
  (<*>) :: Free f (a -> b) -> Free f a -> Free f b
  Pure a -> b
f <*> :: forall a b. Free f (a -> b) -> Free f a -> Free f b
<*> Free f a
t = (a -> b) -> Free f a -> Free f b
forall a b. (a -> b) -> Free f a -> Free f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Free f a
t
  Impure f (Free f (a -> b))
f <*> Free f a
t = f (Free f b) -> Free f b
forall (f :: * -> *) a. f (Free f a) -> Free f a
Impure ((Free f (a -> b) -> Free f b)
-> f (Free f (a -> b)) -> f (Free f b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Free f (a -> b) -> Free f a -> Free f b
forall a b. Free f (a -> b) -> Free f a -> Free f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Free f a
t) f (Free f (a -> b))
f)

instance (Functor f) => Monad (Free f) where
  {-# INLINEABLE (>>=) #-}
  (>>=) :: Free f a -> (a -> Free f b) -> Free f b
  Pure a
x >>= :: forall a b. Free f a -> (a -> Free f b) -> Free f b
>>= a -> Free f b
f = a -> Free f b
f a
x
  Impure f (Free f a)
t >>= a -> Free f b
f = f (Free f b) -> Free f b
forall (f :: * -> *) a. f (Free f a) -> Free f a
Impure ((Free f a -> Free f b) -> f (Free f a) -> f (Free f b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Free f a -> (a -> Free f b) -> Free f b
forall a b. Free f a -> (a -> Free f b) -> Free f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Free f b
f) f (Free f a)
t)

foldFree ::
  forall f a b.
  (Functor f) =>
  (a -> b) ->
  (f b -> b) ->
  Free f a ->
  b
foldFree :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> (f b -> b) -> Free f a -> b
foldFree a -> b
pure' f b -> b
impure = Free f a -> b
go
  where
    go :: Free f a -> b
    go :: Free f a -> b
go = \case
      Pure a
x -> a -> b
pure' a
x
      Impure f (Free f a)
t -> f b -> b
impure ((Free f a -> b) -> f (Free f a) -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Free f a -> b
go f (Free f a)
t)

exec :: (Exec f) => Free f a -> IO a
exec :: forall (f :: * -> *) a. Exec f => Free f a -> IO a
exec = (a -> IO a) -> (f (IO a) -> IO a) -> Free f a -> IO a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> (f b -> b) -> Free f a -> b
foldFree a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return f (IO a) -> IO a
forall a. f (IO a) -> IO a
forall (f :: * -> *) a. Exec f => f (IO a) -> IO a
execAlgebra

instance (Exec f, Exec g) => Exec (f :+: g) where
  {-# INLINEABLE execAlgebra #-}
  execAlgebra :: forall a. (:+:) f g (IO a) -> IO a
execAlgebra = \case
    Left' f (IO a)
e -> f (IO a) -> IO a
forall a. f (IO a) -> IO a
forall (f :: * -> *) a. Exec f => f (IO a) -> IO a
execAlgebra f (IO a)
e
    Right' g (IO a)
e -> g (IO a) -> IO a
forall a. g (IO a) -> IO a
forall (f :: * -> *) a. Exec f => f (IO a) -> IO a
execAlgebra g (IO a)
e

type Exec :: (Type -> Type) -> Constraint
class (Functor f) => Exec f where
  execAlgebra :: f (IO a) -> IO a

injectFree :: (g :<: f) => g (Free f a) -> Free f a
injectFree :: forall (g :: * -> *) (f :: * -> *) a.
(g :<: f) =>
g (Free f a) -> Free f a
injectFree = f (Free f a) -> Free f a
forall (f :: * -> *) a. f (Free f a) -> Free f a
Impure (f (Free f a) -> Free f a)
-> (g (Free f a) -> f (Free f a)) -> g (Free f a) -> Free f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g (Free f a) -> f (Free f a)
forall a. g a -> f a
forall (sub :: * -> *) (sup :: * -> *) a.
(sub :<: sup) =>
sub a -> sup a
inj