Structurally enforced Free Alternative, without le

Question

There is a nice Free Alternative in the great free package, which lifts a Functor to a left-distributive Alternative.

That is, the claim is that:

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

is an Alternative homomorphism, with liftAlt. And, indeed, it is one, but only for left-distributive Alternative instances.

Of course, in reality, very few Alternative instances are actually left-distributive. Most of the alternative instances that actually matter (parsers, MaybeT f for most Monad f, etc.) are not left-distributive. This fact can be shown by an example where runAlt and liftAlt do not form an Alternative homomorphism:

(writeIORef x False <|> writeIORef True) *> (guard =<< readIORef x)
-- is an IO action that throws an exception
runAlt id $ (liftAlt (writeIORef x False) <|> liftAlt (writeIORef True))
               *> liftAlt (guard =<< readIORef x)
-- is an IO action that throws no exception and returns successfully ()

So runAlt is only an Alternative homomorphism for some Alternatives, but not all. This is because the structure of Alt normalizes all actions to distribute over the left.

Alt is great because, structurally, Alt f is a lawful Applicative and Alternative. There isn't any possible way to construct a value of type Alt f a using the Applicative and Alternative functions that don't follow the laws...the structure of the type itself is what makes it a free Alternative.

Just like, for lists, you can't construct a list using <> and mempty that doesn't respect x <> mempty = x, mempty <> x = x, and associativity.

I've written a Free alternative that doesn't enforce the Applicative and Alternative laws, structurally, but does yield a valid Alternative and Applicative homomorphism with runAlt/liftAlt:

data Alt :: (* -> *) -> * -> * where
    Pure  :: a   -> Alt f a
    Lift  :: f a -> Alt f a
    Empty :: Alt f a
    Ap    :: Alt f (a -> b) -> Alt f a -> Alt f b
    Plus  :: Alt f as -> Alt f as -> Alt f as

instance Functor f => Functor (Alt f) where
    fmap f = \case
      Pure x     -> Pure (f x)
      Lift x     -> Lift (f <$> x)
      Empty      -> Empty
      Ap fs xs   -> Ap ((f .) <$> fs) xs
      Plus xs ys -> Plus (f <$> xs) (f <$> ys)

instance Functor f => Applicative (Alt f) where
    pure  = Pure
    (<*>) = Ap

instance Functor f => Alternative (Alt f) where
    empty = Empty
    (<|>) = Plus

structurally, Alt f is not an actual Applicative, because:

pure f <*> pure x = Ap (Pure f) (Pure x)
pure (f x)        = Pure (f x)

So pure f <*> pure x is not the same as pure (f x), structurally. Not a valid Applicative, right off the bat.

But, with the given runAlt and liftAlt:

liftAlt :: f a -> Alt f a
liftAlt = Lift

runAlt :: Alternative g => (forall x. f x -> g x) -> Alt f a -> g a
runAlt f = \case
  Pure x     -> pure x
  Lift x     -> f x
  Empty      -> empty
  Ap fs xs   -> runAlt f fs <*> runAlt f xs
  Plus xs ys -> runAlt f xs <|> runAlt f ys

And runAlt here does indeed act as a valid Applicative homomorphism with a given natural transformation...

One could say that my new Alt f is a valid Alternative and Applicative when quotiented by the equivalence relationship defined by runAlt, i suppose.

Anyway, this is only slightly unsatisfying. Is there any way to write a free Alternative that is structurally a valid Alternative and Applicative, without enforcing left distributivity?

(In particular, I'm actually interested in one that follows the left catch law, and enforces it structurally. This would be a separate and also interesting thing, but not completely necessary.)

And, if there isn't any way, why not?

Answer 1

Control.Alternative.Free's Alt f produces a left-distributive Alternative for free, even if f isn't Alternative or f is a non-left-distributive Alternative. We can say that, in addition to the well-agreed upon alternative laws

empty <|> x = x
x <|> empty = x
(x <|> y) <|> z = x <|> (y <|> z)
empty <*> f = empty

Alt f also gives left-distribution for free.

(a <|> b) <*> c = (a <*> c) <|> (b <*> c)

Because Alt f is always left distributive (and runAlt . liftAlt = id) liftAlt can never be a homomorphism for non-left-distributive Alternatives. If an Alternative f is not left-distributive, then there exist a, b, and c such that

(a <|> b) <*> c != (a <*> c) <|> (b <*> c)

If liftAlt : f -> Alt f were a homomorphism then

                  (a <|> b) <*> c  !=                   (a <*> c) <|> (b <*> c)                                       -- f is not left-distributive
id               ((a <|> b) <*> c) != id               ((a <*> c) <|> (b <*> c))
runAlt . liftAlt ((a <|> b) <*> c) != runAlt . liftAlt ((a <*> c) <|> (b <*> c))                                      -- runAlt . liftAlt = id
runAlt ((liftAlt a <|> liftAlt b) <*> liftAlt c) != runAlt ((liftAlt a <*> liftAlt c) <|> (liftAlt b <*> liftAlt c))  -- homomorphism
runAlt ((liftAlt a <|> liftAlt b) <*> liftAlt c) != runAlt ((liftAlt a <|> liftAlt b) <*> liftAlt c)                  -- by left-distribution of `Alt`, this is a contradiction

To demonstrate this we need an Alternative that isn't left-distributive. Here's one, FlipAp [].

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)

Along with some laws for left distribution and right distribution, and some examples

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)

We can demonstrate a few properties of lists, FlipAp lists, and runAlt.

Lists are left-distributive, but FlipAp lists aren't

ldExample1 :: Example [Int]
ldExample1 :: Example (FlipAp [] Int)

[[3,4,20,30],[3,4,20,30]]
[FlipAp {unFlipAp = [3,20,4,30]},FlipAp {unFlipAp = [3,4,20,30]}]

Lists aren't right-distributive, but FlipAp lists are

rdExample1 :: Example [Int]
rdExample1 :: Example (FlipAp [] Int)

[[3,4,20,30],[3,20,4,30]]
[FlipAp {unFlipAp = [3,20,4,30]},FlipAp {unFlipAp = [3,20,4,30]}]

Alt is always left-distributive

map (runAlt id) ldExample1 :: Example [Int]
map (runAlt id) ldExample1 :: Example (FlipAp [] Int)

[[3,4,20,30],[3,4,20,30]]
[FlipAp {unFlipAp = [3,4,20,30]},FlipAp {unFlipAp = [3,4,20,30]}]

Alt is never right-distributive

map (runAlt id) rdExample1 :: Example [Int]
map (runAlt id) rdExample1 :: Example (FlipAp [] Int)

[[3,4,20,30],[3,20,4,30]]
[FlipAp {unFlipAp = [3,4,20,30]},FlipAp {unFlipAp = [3,20,4,30]}]

We can defile a right-distributive free alternative in terms of FlipAp and Alt.

runFlipAlt :: forall f g a. Alternative g => (forall x. f x -> g x) -> FlipAp (Alt f) a -> g a
runFlipAlt nt = runAlt nt . unFlipAp

FlipAp Alt is never left-distributive.

map (runFlipAlt id) ldExample1 :: Example [Int]
map (runFlipAlt id) ldExample1 :: Example (FlipAp [] Int)

[[3,20,4,30],[3,4,20,30]]
[FlipAp {unFlipAp = [3,20,4,30]},FlipAp {unFlipAp = [3,4,20,30]}]

FlipAp Alt is always right-distributive

map (runFlipAlt id) rdExample1 :: Example [Int]
map (runFlipAlt id) rdExample1 :: Example (FlipAp [] Int)

[[3,20,4,30],[3,20,4,30]]
[FlipAp {unFlipAp = [3,20,4,30]},FlipAp {unFlipAp = [3,20,4,30]}]

Up until now I haven't told you anything that you didn't already imply by saying that liftAlt : f -> Alt f is an Alternative homomorphism, but only for left-distributive Alternative instances. But I have shown you a free-alternative that isn't left-distributive (it's trivially right-distributive instead).

A structurally valid free Alternative

This section answers the bulk of your question, is there a structurally valid free Alternative that isn't left-distributive? Yes.

This isn't an efficient implementation; it's purpose is to demonstrate that it exists and that some version of it can be arrived at in a straight-forward manner.

To make a structurally valid free Alternative I am doing two things. The first is to create a data structure that can't represent any of the Alternative laws; if it can't represent the law then a structure can't be constructed independently of the type class to violate it. This is the same trick used to make lists structurally obey the Alternative associativity law; there's no list that can represent the left-associated (x <|> y) <|> z. The second part is to make sure the operations obey the laws. A list can't represent the left association law, but an implementation of <|> could still violate it, like x <|> y = x ++ reverse y.

The following structure can't be constructed to represent any of the Alternative laws.

{-# Language GADTs #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}

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

--           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

It's a Functor

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)

And it's Applicative. Because the structure can't represent the laws, when we encounter a term containing one of the unpreventable expressions we're forced to convert it into something else. The laws tell us what to do.

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)

All of those Aps could be covered by a pair of view patterns, but it doesn't make it any simpler.

It's also an Alternative. For this we'll use a view pattern to divide the cases into the empty and non-empty cases, and an extra type to store the proof that they're non-empty

{-# Language ViewPatterns #-}

import Control.Applicative

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)

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)  -- (x <|> y) <|> x = x <|> (y <|> 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 and runAlt

{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}

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

This new Alt f doesn't provide either left-distribution or right-distribution for free, and therefore runAlt id :: Alt f a -> g a preserves how distributive g is.

Lists are still left-distributive, but FlipAp lists aren't.

map (runAlt id) ldExample1 :: Example [Int]
map (runAlt id) ldExample1 :: Example (FlipAp [] Int)

[[3,4,20,30],[3,4,20,30]]
[FlipAp {unFlipAp = [3,20,4,30]},FlipAp {unFlipAp = [3,4,20,30]}]

List's aren't right-distributive, but FlipAp lists still are

map (runAlt id) rdExample1 :: Example [Int]
map (runAlt id) rdExample1 :: Example (FlipAp [] Int)

[[3,4,20,30],[3,20,4,30]]
[FlipAp {unFlipAp = [3,20,4,30]},FlipAp {unFlipAp = [3,20,4,30]}]

Source code for this section

Structurally valid left-catch free Alternative

To control which laws we want we can add them to the structurally free alternative we made earlier.

To add left-catch we'll modify the structure so it can't represent it. Left catch is

(pure a) <|> x = pure a

To keep Alt' from representing it we'll exclude pure from what's allowed to the left of Plus.

--           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 False 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)

      -- Pure can't be to the left of Plus
      -- (pure a) <|> x = pure a

    ...

This results in a compiler error in the implementation of Alternative Alt

Couldn't match type ‘'True’ with ‘'False’
Expected type: Alt' 'False 'False 'False f a1
  Actual type: Alt' 'False pure2 plus2 f a1
In the first argument of ‘Plus’, namely ‘a’
In the first argument of ‘AltNE’, namely ‘(Plus a b)

Which we can fix by appealing to our new law, (pure a) <|> x = pure a

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 a@(Pure _) <> _ = AltNE a                                -- (pure a) <|> x = pure a
        AltNE (Plus x y) <> AltNE z = AltNE x <> (AltNE y <> AltNE z)  -- (x <|> y) <|> x = x <|> (y <|> z)
        AltNE a@(Lift _) <> AltNE b = AltNE (Plus a b)
        AltNE a@(Ap _ _) <> AltNE b = AltNE (Plus a b)