structurally correct free alternative

structrally-free-alternative.hs

{-# Language GADTs #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language ViewPatterns #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}


import Control.Applicative


data Alt :: (* -> *) -> * -> * where
    Alt :: Alt' empty pure plus f a -> Alt f a

data AltEmpty :: (* -> *) -> * -> * where
    Empty_    :: Alt' True  False False f a -> AltEmpty f a
    NonEmpty_ :: AltNE f a -> AltEmpty f a


data AltNE :: (* -> *) -> * -> * where
    AltNE :: Alt' False pure plus f a -> AltNE f a

empty_ :: Alt' e1 p1 p2 f a -> AltEmpty f a
empty_ x@Empty      = Empty_ x
empty_ x@(Pure _)   = NonEmpty_ (AltNE x)
empty_ x@(Lift _)   = NonEmpty_ (AltNE x)
empty_ x@(Plus _ _) = NonEmpty_ (AltNE x)
empty_ x@(Ap _ _)   = NonEmpty_ (AltNE x)


--           empty   pure    plus
data Alt' :: Bool -> Bool -> Bool -> (* -> *) -> * -> * where
    Empty ::        Alt' True  False False f a
    Pure  :: a   -> Alt' False True  False f a
    Lift  :: f a -> Alt' False False False f a
    
    Plus  :: Alt' False pure1 False f a -> Alt' False pure2 plus2 f a -> Alt' False False True  f a
      -- Empty can't be to the left or right of Plus
      -- empty <|> x = x
      -- x <|> empty = x
      
      -- Plus can't be to the left of Plus
      -- (x <|> y) <|> z = x <|> (y <|> z)
    Ap    :: Alt' False False plus1 f (a -> b) -> Alt' empty False plus2 f a -> Alt' False False False f b
      -- Empty can't be to the left of `Ap`
      -- empty <*> f = empty
    
      -- Pure can't be to the left or right of `Ap`
      -- pure id <*> v = v     
      -- pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
      -- pure f <*> pure x = pure (f x)
      -- u <*> pure y = pure ($ y) <*> u
    
instance Functor f => Functor (Alt' empty pure plus f) where
    fmap _ Empty       = Empty
    fmap f (Pure a)    = Pure (f a)
    fmap f (Plus a as) = Plus (fmap f a) (fmap f as)
    fmap f (Lift a)    = Lift (fmap f a)
    fmap f (Ap g a)    = Ap (fmap (f .) g) a


instance Functor f => Functor (Alt f) where
    fmap f (Alt a) = Alt (fmap f a)


instance Functor f => Applicative (Alt f) where
    pure a = Alt (Pure a)
    
    Alt Empty <*> _ = Alt Empty                          -- empty <*> f = empty
    Alt (Pure f) <*> (Alt x) = Alt (fmap f x)            -- pure f <*> x = fmap f x          (free theorem)
    Alt u <*> (Alt (Pure y)) = Alt (fmap ($ y) u)        -- u <*> pure y = pure ($ y) <*> u
    Alt f@(Lift _)   <*> Alt x@Empty      = Alt (Ap f x)
    Alt f@(Lift _)   <*> Alt x@(Lift _)   = Alt (Ap f x)
    Alt f@(Lift _)   <*> Alt x@(Plus _ _) = Alt (Ap f x)
    Alt f@(Lift _)   <*> Alt x@(Ap _ _)   = Alt (Ap f x)
    Alt f@(Plus _ _) <*> Alt x@Empty      = Alt (Ap f x)
    Alt f@(Plus _ _) <*> Alt x@(Lift _)   = Alt (Ap f x)
    Alt f@(Plus _ _) <*> Alt x@(Plus _ _) = Alt (Ap f x)
    Alt f@(Plus _ _) <*> Alt x@(Ap _ _)   = Alt (Ap f x)
    Alt f@(Ap _ _)   <*> Alt x@Empty      = Alt (Ap f x)
    Alt f@(Ap _ _)   <*> Alt x@(Lift _)   = Alt (Ap f x)
    Alt f@(Ap _ _)   <*> Alt x@(Plus _ _) = Alt (Ap f x)
    Alt f@(Ap _ _)   <*> Alt x@(Ap _ _)   = Alt (Ap f x)
    


instance Functor f => Alternative (Alt f) where
    empty = Alt Empty
    
    Alt Empty <|> x = x                                 -- empty <|> x = x
    x <|> Alt Empty = x                                 -- x <|> empty = x
    Alt (empty_ -> NonEmpty_ a) <|> Alt (empty_ -> NonEmpty_ b) = case a <> b of AltNE c -> Alt c
      where
        (<>) :: AltNE f a -> AltNE f a -> AltNE f a
        AltNE (Plus x y) <> AltNE z = AltNE x <> (AltNE y <> AltNE z)
        AltNE a@(Pure _) <> AltNE b = AltNE (Plus a b)
        AltNE a@(Lift _) <> AltNE b = AltNE (Plus a b)
        AltNE a@(Ap _ _) <> AltNE b = AltNE (Plus a b)
        
liftAlt :: f a -> Alt f a
liftAlt = Alt . Lift

runAlt' :: forall f g x empty pure plus a. Alternative g => (forall x. f x -> g x) -> Alt' empty pure plus f a -> g a
runAlt' u = go
  where
    go :: forall empty pure plus a. Alt' empty pure plus f a -> g a
    go Empty    = empty
    go (Pure a) = pure a
    go (Lift a) = u a
    go (Plus x y) = go x <|> go y
    go (Ap f x)   = go f <*> go x

runAlt :: Alternative g => (forall x. f x -> g x) -> Alt f a -> g a
runAlt u (Alt x) = runAlt' u x


newtype FlipAp f a = FlipAp {unFlipAp :: f a}
  deriving Show


instance Functor f => Functor (FlipAp f) where
    fmap f (FlipAp x) = FlipAp (fmap f x)


instance Applicative f => Applicative (FlipAp f) where
    pure = FlipAp . pure
    (FlipAp f) <*> (FlipAp xs) = FlipAp ((flip ($) <$> xs) <*> f)


instance Alternative f => Alternative (FlipAp f) where
    empty = FlipAp empty
    (FlipAp a) <|> (FlipAp b) = FlipAp (a <|> b)

leftDist :: Alternative f => f (x -> y) -> f (x -> y) -> f x -> Example (f y)
leftDist a b c = [(a <|> b) <*> c, (a <*> c) <|> (b <*> c)]

rightDist :: Alternative f => f (x -> y) -> f x -> f x -> Example (f y)
rightDist a b c = [a <*> (b <|> c), (a <*> b) <|> (a <*> c)]

type Example a = [a]

ldExample1 :: Alternative f => Example (f Int)
ldExample1 = leftDist (pure (+1)) (pure (*10)) (pure 2 <|> pure 3)

rdExample1 :: Alternative f => Example (f Int)
rdExample1 = rightDist (pure (+1) <|> pure (*10)) (pure 2) (pure 3)

main = do
  putStrLn "Left distributive"
  print $ (map (runAlt id) ldExample1 :: Example [Int])
  print $ (map (runAlt id) ldExample1 :: Example (FlipAp [] Int))
  putStrLn "Right distributive"
  print $ (map (runAlt id) rdExample1 :: Example [Int])
  print $ (map (runAlt id) rdExample1 :: Example (FlipAp [] Int))