Skip to content

Instantly share code, notes, and snippets.

Last active March 12, 2017 00:32
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
What would you like to do?
-- Defining some Maybe values...
-- These could just as well have been database lookups or something else
x : Maybe Nat
x = Just 42
y : Maybe String
y = Just "hello idris"
z : Maybe Nat
z = Just 4
-- we wish to sum the above values, -but only if all of them exist...
-- we might start out doing it this way.. Typing match case stuff until our fingers fall off..
addStuffBad : Maybe Nat
addStuffBad =
case x of
Nothing => Nothing
(Just x') =>
case y of
Nothing => Nothing
(Just y') =>
case z of
Nothing => Nothing
(Just z') => Just (x' + length y' + z')
-- then we discover the allmighty Bind function.. and carefully count parentheses
addStuffBetter : Maybe Nat
addStuffBetter =
x >>= (\x' =>
y >>= (\y' =>
z >>= (\z' =>
Just (x' + length y' + z'))))
-- finaly we learn about the existence of the neat do syntax... syntax sugar!, yummy!
addStuffNeat : Maybe Nat
addStuffNeat =
do x' <- x
y' <- y
z' <- z
pure (x' + length y' + z')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment