[Haskell-cafe] Sequence of lifting transformation operators

Taeer Bar-Yam taeer at necsi.edu
Tue Jan 31 04:37:25 UTC 2017

This is (IMO) very similar in use-case to Idris' bang-notation. I'll give a brief
summary of what that is and then explain the pros/cons that I see between them.

In Idris the do notation has the added notation that
do return $ !a + !b
would desugar to
  a' <- a
  b' <- b
  return $ a' + b'

So !a unwraps a higher up and then uses the unwrapped version.
Thus if you want to apply a function to apply a function to some wrapped and
some unwrapped values:
do return $ f !a b !c !d

- Idris notation is (IMO) more visually appealing.
  - In particular, it puts the information about which arguments are lifted next
    to the arguments themselves, which matches our intuition about what's going on
- While it matches our intuition, it does *not* match what's actually going on,
  so that's a con.
- Idris notation can lift things more than once:
  do return $ f !!a !b !!!!c
- Idris notation is syntactic sugar, not a first-class operator
  - So that means no currying, no passing it in as an argument, etc. (though
    with lambdas this is not as bad as it otherwise would be)
- Idris notation is for monads, so it would not work for things that are
  applicative but not monads (though I'm not entirely sure what falls into this

What do you y'all think? Do they operate in different enough spaces that they
should both exist (like applicatives and moands), or is one clearly better?


More information about the Haskell-Cafe mailing list