Files for the PL presentation on (free) monads

Composition.hs

#!/usr/bin/env stack
-- stack script --resolver lts-19.30
{-# LANGUAGE GADTs, ViewPatterns, ScopedTypeVariables, InstanceSigs, MultiParamTypeClasses, DeriveFunctor, StandaloneDeriving, UnicodeSyntax, ImportQualifiedPost #-}

import Control.Applicative (liftA2)
import Control.Monad (join)
import Data.Proxy (Proxy (Proxy))

--

data Product f g a = Pair { fstP ∷ f a, sndP ∷ g a }

instance (Functor f, Functor g) ⇒ Functor (Product f g) where
    fmap f (Pair x y) = Pair (fmap f x) (fmap f y)

instance (Applicative f, Applicative g) ⇒ Applicative (Product f g) where
    pure a = Pair (pure a) (pure a)
    Pair f g <*> Pair x y = Pair (f <*> x) (g <*> y)

instance (Monad f, Monad g) ⇒ Monad (Product f g) where
    Pair m n >>= k = Pair (m >>= fstP . k) (n >>= sndP . k)

--

newtype Compose f g a = Compose { getCompose ∷ f (g a) }
    deriving Eq

instance (Functor f, Functor g) ⇒ Functor (Compose f g) where
    fmap f (Compose x) = Compose (fmap (fmap f) x)
    -- f ∷ a → b
    -- fmap f ∷ f a → f b
    -- fmap (fmap f) ∷ g (f a) → g (f b)

instance (Applicative f, Applicative g) ⇒ Applicative (Compose f g) where
    pure a = Compose (pure (pure a))
    Compose f <*> Compose x = Compose (liftA2 (<*>) f x)


-- data Maybe a = Just a | Nothing
-- data Proxy a = Proxy

-- Counterexample for Monads:
bindC ∷ (m ~ Compose Maybe Proxy) ⇒ m a → (a → m b) → m b
bindC (Compose (Just Proxy)) k = Compose (Just Proxy)
bindC (Compose Nothing)      k = Compose Nothing

kC ∷ (m ~ Compose Maybe Proxy) ⇒ Bool → m Int
kC True = Compose (Just Proxy)
kC False = Compose Nothing

lawC ∷ Bool
lawC = (pure True `bindC` kC) == kC True
    && (pure False `bindC` kC) == kC False

-- pure x == Compose (Just Proxy)
-- pure x >>= k = ⟨something that doesn't depend on x⟩
--              ≠ k x




data Sum f g a = InL (f a) | InR (g a)

instance (Functor f, Functor g) ⇒ Functor (Sum f g) where
    fmap f (InL x) = InL (fmap f x)
    fmap f (InR x) = InR (fmap f x)

-- Sum of Applicatives is not always an Applicative


-- Monad instance for Compose
class Distributive f g where
    dist ∷ f (g a) → g (f a)

-- f (g (f (g a))) -> f (g a)

instance (Monad f, Monad g, Distributive g f) ⇒ Monad (Compose f g) where
    Compose x >>= k = Compose $ join $ fmap (fmap join . dist . fmap (getCompose . k)) x

-- Note:
--  (∀ f. Functor f ⇒ Distributive f g) ⇒ (∃ x. (g a) ≃ (x → a))

main ∷ IO ()
main = do
    putStrLn "Hello, world!"

    putStrLn $ "lawC = " ++ show lawC

FreeMonad.hs

#!/usr/bin/env stack
-- stack script --resolver lts-19.30
{-# LANGUAGE UndecidableInstances, StandaloneDeriving, UnicodeSyntax, ImportQualifiedPost #-}

module Main where

import Data.Functor.Identity (Identity (..))
import Control.Monad (ap)

-- A Monoid m has:
--  A unit          ε : 1 → m
--  Binary operator + : m × m → m
--  Associativity  : ∀ a b c. a + (b + c) ≌ (a + b) + c
--  Left identity  : ∀ a. ε + a ≌ a
--  Right identity : ∀ a. a + ε ≌ a
--
-- Here,
--  ≌ : the notion of equality
--  → : morphisms
--  × : the notion of product
--  1 : the product identity

-- The category of endofunctors:
--   f → g := ∀ a. f a → g a
--   f × g := Compose f g      (λ a. f (g a))
--   1     := Identity         (λ a. a)
--
-- So a Monoid in the category of endofunctors has:
--   A unit          ε : 1 → m
--                     ≃ ∀ a. a → m a
--   Binary operator + : m × m → m
--                     ≃ ∀ a. m (m a) → m a

data Free f a
    = Pure a
    | Impure (f (Free f a))

deriving instance (Show a, Show (f (Free f a))) ⇒ Show (Free f a)
deriving instance (Eq a, Eq (f (Free f a))) ⇒ Eq (Free f a)

instance Functor f ⇒ Functor (Free f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Impure m) = Impure (fmap (fmap f) m)

instance Functor f ⇒ Applicative (Free f) where
    pure = Pure
    (<*>) = ap

instance Functor f ⇒ Monad (Free f) where
    Pure a >>= k = k a
    Impure m >>= k = Impure (fmap (>>= k) m)



lift ∷ Functor f ⇒ f a → Free f a
lift x = Impure (fmap pure x)


ex1, ex2 ∷ Free Identity [Int]
(ex1, ex2) = (foo >>= \x → bar x >>= baz, (foo >>= bar) >>= baz)
    where
        foo = Impure (Identity (Pure [1]))
        bar x = Impure (Identity (Pure (x ++ [2])))
        baz x = Impure (Identity (Pure (x ++ [3])))

main ∷ IO ()
main = do
    putStrLn "Free Monad example"
    putStrLn $ "ex1 = " ++ show ex1
    putStrLn $ "ex2 = " ++ show ex2
    putStrLn $ "ex1 == ex2 = " ++ show (ex1 == ex2)

FreeStructure.hs

#!/usr/bin/env stack
-- stack script --resolver lts-19.30
{-# LANGUAGE UnicodeSyntax, ImportQualifiedPost #-}

module Main where

import Data.List.NonEmpty qualified as NE


-- A "Free Structure" is a mapping from a type to another type s.t.
-- * The new type satisfies the given structure
-- * There is an injection from the original type into the new type
--
-- "The Free Structure" satisfies the above where
-- * For every other free structure, there is an injection into it
-- (Universal Property)


-- Implement the minimum requirements of a magma for any type
-- * there is a binary operator
data FreeMagma a
    = Single a
    | Plus (FreeMagma a) (FreeMagma a)
    deriving Eq

instance Show a ⇒ Show (FreeMagma a) where
    show (Single a) = show a
    show (Plus a b) = "(" ++ show a ++ " + " ++ show b ++ ")"

-- Note: FreeMagma's binary operator is not associative
ex1, ex2 ∷ FreeMagma Int
(ex1, ex2) = (foo `Plus` (bar `Plus` baz), (foo `Plus` bar) `Plus` baz)
    where
        foo = Single 1
        bar = Single 2
        baz = Single 3

-- Implements the minimum requirements of a semigroup for any type
-- * there is a binary operator
-- * the binary operator is associative
type FreeSemigroup = NE.NonEmpty

ex3, ex4 ∷ FreeSemigroup Int
(ex3, ex4) = (foo <> (bar <> baz), (foo <> bar) <> baz)
    where
        foo = NE.singleton 1
        bar = NE.singleton 2
        baz = NE.singleton 3

-- Implements the minimum requirements of a monoid for any type
-- * there is a binary operator
-- * there is a zero element
-- * the binary operator is associative
-- * the zero element is the left and right identity of the binary operator
type FreeMonoid = []

ex5, ex6 ∷ FreeMonoid Int
(ex5, ex6) = (empty <> (foo <> (bar <> baz)), ((foo <> bar) <> baz) <> empty)
    where
        foo = [1]
        bar = [2]
        baz = [3]
        empty = []


main ∷ IO ()
main = do
    putStrLn "Free Magma examples"
    putStrLn $ "ex1 = 1 + (2 + 3) = " ++ show ex1
    putStrLn $ "ex2 = (1 + 2) + 3 = " ++ show ex2
    putStrLn $ "ex1 == ex2 = " ++ show (ex1 == ex2)
    putStrLn ""

    putStrLn "Free Semigroup examples"
    putStrLn $ "ex3 = 1 + (2 + 3) = " ++ show (NE.toList ex3)
    putStrLn $ "ex4 = (1 + 2) + 3 = " ++ show (NE.toList ex4)
    putStrLn $ "ex3 == ex4 = " ++ show (ex3 == ex4)
    putStrLn ""

    putStrLn "Free Monoid examples"
    putStrLn $ "ex5 = ∅ + (1 + (2 + 3)) = " ++ show ex5
    putStrLn $ "ex6 = ((1 + 2) + 3) + ∅ = " ++ show ex6
    putStrLn $ "ex5 == ex6 = " ++ show (ex5 == ex6)
    putStrLn ""

Teletype.hs

#!/usr/bin/env stack
-- stack script --resolver lts-19.30
{-# LANGUAGE DeriveFunctor, StandaloneDeriving, UnicodeSyntax, ImportQualifiedPost #-}

module Main where

import Prelude hiding (read)
import Control.Monad.Free (Free (..), liftF)
import Control.Monad.Trans.Writer.Strict
import Control.Monad.Trans.Reader

-- type Teletype1 a = WriterT String (Reader String) a

data Teletype a
    = Write String a
    | Read (String → a)
    deriving Functor

write ∷ String → Free Teletype ()
write str = liftF (Write str ())

read ∷ Free Teletype String
read = liftF (Read id)

echoServer ∷ Free Teletype ()
echoServer = do
    msg ← read
    case msg of
        "" → pure ()
        "quit" → pure ()
        _ → do
            write msg
            echoServer

interpretIO ∷ Free Teletype a → IO a
interpretIO m =
    case m of
        Pure a → pure a
        Free (Write msg k) → do
            putStrLn msg
            interpretIO k
        Free (Read k) → do
            line ← getLine
            interpretIO (k line)

interpretList ∷ Free Teletype a → [String] → (a, [String])
interpretList m input = go m input []
    where
        go ∷ Free Teletype a → [String] → [String] → (a, [String])
        go m input output =
            case m of
                Pure a → (a, reverse output)
                Free (Write msg k) → go k input (msg : output)
                Free (Read k) →
                    case input of
                        []     → go (k "") [] output
                        x : xs → go (k x) xs output

interpretIOLimit ∷ Free Teletype () → Int → IO (Maybe (Free Teletype ()))
interpretIOLimit m 0 = do
    putStrLn "Limit reached!"
    pure (Just m)
interpretIOLimit m n =
    case m of
        Pure () → pure Nothing
        Free (Write msg k) → do
            putStrLn msg
            interpretIOLimit k (n - 1)
        Free (Read k) → do
            line ← getLine
            interpretIOLimit (k line) (n - 1)

main ∷ IO ()
main = do
    putStrLn "Starting echo server..."

    -- print $ interpretList echoServer ["foo", "bar", "baz"]
    -- interpretIO echoServer
    -- rest ← interpretIOLimit echoServer 5
    -- case rest of
    --     Nothing → pure ()
    --     Just rest → do
    --         putStrLn "Continue?"
    --         resp ← getLine
    --         case resp of
    --             'y' : _ → interpretIO rest
    --             _ → pure ()