November 2013 – Page 2 – bor0's reflective blog

isSpace' x = x == ' '

removeFirst [] = []
removeFirst (x:xs) = if isSpace' x then removeFirst xs else (x:xs)

break' p xs = break'' p xs []
where
    break'' p (x:xs) ys = if (p x) then (ys, x:xs) else break'' p xs (ys ++ [x])
    break'' _ []     ys = (ys, "")

words' x = words'' ("", x)
where
    words'' (_, "") = []
    words'' (a, b) = [q] ++ words'' (q, r)
      where
        q = fst (break' isSpace' b)
        r = removeFirst (snd (break' isSpace' b))

The Probably Monad is same as the Maybe Monad, so this is how I had it defined:

data Probably x = Nope | Kinda x deriving (Show)

instance Monad Probably where
    Kinda x >>= f = f x
    Nope >>= f = Nope
    return = Kinda

add x y = x >>= (\x -> y >>= (\y -> return (x + y)))
-- Example: add (add (Kinda 1) (Kinda 2)) (Kinda 4)

Proof:

1. Left identity:
return a >>= f ≡ f a
“return a” by definition is “Kinda a”, and so the bind operator is defined as “Kinda a >>= f ≡ f a”.
So with these two definitions, we have shown that “return a >>= f ≡ f a”.

2. Right identity:
m >>= return ≡ m
If we let m equal “Kinda n”, then we have “Kinda n >>= return ≡ Kinda n”, but by definition of the binding operator,
we have that “Kinda n >>= return = return n”, and so “return n”. So, by definition of return, we have “Kinda n”, which is m.

3. Associativity:
(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
If we let m equal “Kinda n”, then we have:
LHS: (Kinda n >>= f) >>= g ≡ (f n) >>= g
RHS: Kinda n >>= (\x -> f x >>= g) ≡ (\x -> f x >>= g) n ≡ f n >>= g

Month: November 2013

Haskell words implementation

Implementation of a Monad with proof