EitherApplicativeLaws.hs

-- Законы аппликативных функторов выполняются для 
-- стандартного представителя (Either e)

instance Applicative (Either e) where
    pure          = Right

    Left  e <*> _ = Left e
    Right f <*> r = fmap f r

instance Functor (Either a) where
    fmap _ (Left x) = Left x
    fmap f (Right y) = Right (f y)


-- Докажем Identity
pure id <*> v == v
-- для типа Either, то есть
v = Left lv | Right rv
-- Разберем варианты

pure id <*> Left lv     -- определение pure для Either
== Right id <*> Left lv -- определение <*> для Either
== fmap id (Left lv)    -- определение fmap для Either
== Left lv
-- ok for Left 

pure id <*> Right rv     -- определение pure для Either
== Right id <*> Right rv -- определение <*> для Either
== fmap id (Right rv)    -- определение fmap для Either
== Right (id rv)         -- определение id
== Right rv
-- ok for Right 

-- QED



-- Докажем Composition
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
-- для типа Either, то есть
-- для u,v,w
- = Left l- | Right r-

-- Рассмотрим Right повсюду
pure (.) <*> u <*> v <*> w         -- определение pure для Either
== Right (.) <*> u <*> v <*> w     -- определение <*> для Either
== fmap (.) (Right ru) <*> v <*> w -- определение fmap для Either
== Right (ru .) <*> v <*> w        -- определение <*> для Either
== fmap (ru .) (Right rv) <*> w    -- определение fmap для Either
== Right (ru . rv) <*> w           -- определение <*> для Either
== fmap (ru . rv) (Right rw)       -- определение fmap для Either
== Right ((ru . rv) rw)            -- определение (.)
== Right (ru (rv rw))

u <*> (v <*> w)                    -- 
== (Right ru) <*> (v <*> w)        -- определение <*> для Either
== fmap ru ((Right rv) <*> w)      -- определение <*> для Either
== fmap ru (fmap rv (Right rw))    -- определение fmap для Either
== fmap ru (Right (rv rw))         -- определение fmap  для Either
== Right (ru (rv rw))

-- На любом (Left l) вернётся первый Left и в л.ч. и в п.ч.

-- QED



-- Докажем Homomorphism
pure f <*> pure x = pure (f x)
-- для типа Either 

pure f <*> pure x         -- определение pure для Either
== Right f <*> Right x    -- определение <*> для Either
== fmap f (Right x)       -- определение fmap  для Either
== Right (f x)            -- определение pure для Either
== pure (f x)

-- QED



-- Докажем Interchange
u <*> pure y = pure ($ y) <*> u
-- для типа Either 
-- для типа Either, то есть
v = Left a | Right b
-- Разберем варианты

Left lu <*> pure y          -- определение <*> для Either
== Left lu

pure ($ y) <*> Left lu      -- определение pure для Either
== Right ($ y) <*> Left lu  -- определение <*> для Either
== fmap ($ y) (Left lu)     -- определение fmap  для Either
== Left lu
-- ok for Left 

Right ru <*> pure y         -- определение <*> для Either
== fmap ru (pure y)         -- определение pure для Either
== fmap ru (Right y)        -- определение fmap  для Either
== Right (ru y)

pure ($ y) <*> Right ru     -- определение pure для Either
== Right ($ y) <*> Right ru -- определение <*> для Either
== fmap ($ y) (Right ru)    -- определение fmap  для Either
== Right (ru $ y)
-- ok for Right

-- QED