Monads in Lean

5 points by abhin4v

jkoppel

Do-notation and typeclasses are among the best ideas in Haskell. Good to see another language pick them up.

Fun fact: when monads were first introduced into Haskell, the proposed syntax was to do everything like list comprehensions.

So instead of:

x = do
  a <- Map.get m "key"
  b <- Map.get m a
  return b

You would write

[b | a <- Map.get m "key", b <- Map.get m a]

tcard

And funnily enough, inversely, you can do list comprehensions with monads:

x = [ (a, b) | a <- [1, 2], b <- [3, 4]]
  
y = do
  a <- [ 1, 2 ]
  b <- [ 3, 4 ]
  [(a, b)]

-- Both return [(1,3),(1,4),(2,3),(2,4)]

pervognsen

I didn't see a mention of Lean's extensions to do-notation that make it more like conventional imperative programming and perhaps how that ties into program verification, which if you're already familiar with monads and do-notation might be more interesting.