The ICFP'22 playlist has been published to YouTube

Links
#1

Playlist link

My personal highlights with short summaries:

14 Likes
#2

  • Which one is augustss’s keynote presentation about Verse?

  • Those still confused by

    return :: Monad m => a -> m a

    …can now rejoice - presumably the progress towards “pure imperativity” will also include the addition of while (...) statements at the end of every do-block.

#3

I don’t think he gave a keynote at ICFP this year. You are linking to IFL which is a different conference.

Koka already had that functionality for a few years already. I also think Koka’s algebraic effect approach is nicer than Lean’s monad transformers. But yeah, I think it is better to stick to pure functional programming.

#4

Koka already had that functionality for a few years already […]

… while (...) statements at the end of every do-block? :-D

Blunders and chuckles aside, the presentation on implementing strong call-by-need is somewhat reminiscent of a recent (2016) exploration of head reduction: the reduction of expressions to head normal form, rather than just weak-head normal form - something to look at (more closely!) later, when the slides from that presentation are available…

#5

Ah, Paul Downen is a coauthor of That exploration of head reduction that and he has also contributed to the work on introduction and elimination, left and right this year. It seems to use some of the same ideas, so that might also be interesting to look at more closely. He is also a coauthor of compiling with classical connectives which seems to share similar ideas.

This line of research has given us GHC join points, but it seems like it can give much more if a language is based on it from the ground up like Duo.

#6

Speaking from experience, the Lean extensions to do-notation are actually quite nice to use in practice, and I don’t think that they deserve being made fun of.

If we accept that do notation is nicer in many contexts than manually writing out >>=, then why shouldn’t we also think it’s plausible that let mut can be nicer than a local invocation of runStateT, or that the early return statement can be a nice syntactic sugar for a local invocation of runExceptT?

I’d love to see some of these things in GHC myself.

5 Likes
#7

I agree that it looks compelling.

However, do notation is basically just a way to avoid indentation and parentheses while this let mut is much more complicated. Many beginners already have trouble understanding the rules of do notation. And from personal experience helping a student write Koka code, I can say that the rules for local mutable state are much more difficult to understand. For example try to understand this issue.

Also, I think we should keep unidiomatic things hard to write. There usually is a good way to write your code using higher order functions without having to resort to local mutable state. So, it would mostly be useful for when you are translating imperative code (like the Lean people are doing) or if you are more familiar with imperative code than functional code. I expect that adding special syntax like that will prevent people from truly learning to appreciate higher order functional programming.

There’s a similar divide in array languages where Accelerate and Futhark use pointfree functional combinators while Dex uses imperative pointful for loops. I think I prefer the pointfree functional combinator style.

4 Likes
#8

I’m just guessing here: there probably are a great many other “syntactic sugar crystals” from other languages that people would love to see in Haskell, too - when does this process of accretion stop?

We already support the syntax for some esoteric language called Do - shall we also add lisp, fortran, algol, ada, smalltalk, prolog, sml, java, and intercal-notation too? At that rate, people will soon be able to write Haskell using C++ syntax.

But if you really want to add more semantically-significant keywords - seq, but like its namesake definition in Miranda(R) and Lazy ML: properly sequential in it’s order of evaluation.

Wasn’t one of the proclaimed benefits of having higher-order functions not needing so much “syntactic sugar”, by abstracting out patterns of control as reusable definitions?
But if we have reached the limits of what can be practically refactored, perhaps it’s time for a proper macro system like Clean has, instead of e.g. growing the collection of built-in “synonyms”…

#9

I agree that there are clearly lots of engineering issues to solve. But I don’t agree that the manual encodings of these things are easier to read and maintain - the semantics of actual mutability are difficult, but as a syntax for StateT, I think it’s pretty nice. But now we’re basically down to matters of taste and “don’t knock it 'til you’ve tried it”, which are usually not interesting discussions to have, or matters of engineering, error messages, and approachability, which are interesting but difficult and don’t make sense outside the context of a specific proposal.

I just really don’t like seeing work going on in other language communities, especially work that’s good enough for ICFP, get dismissed out of hand with sarcasm. I think it makes us intellectually worse off as a community to ignore the world around us.

9 Likes
#10

Something I’d add is that the purpose and target audience and intended sort of code to be written in Lean is different than in Haskell. So often syntactic features that may make sense for one audience and set of purposes don’t make sense for another.

If I’m a haskeller working in my language of choice, I may prefer to write and think in an FP style. But if I’m using lean to encode and verify an algorithm presented imperatively, then using features that encode that algorithm as close to its imperative presentation/specification as possible may well be a much easier way to think.

3 Likes
#11

What you’re saying makes sense, but it doesn’t correspond with the way I’ve used those features in Lean. They really do replace local uses of runStateT and friends with something that’s easier for me to read and reason about. Sometimes local, encapsulated mutation or early loop termination is just an easier way to describe something than re-encoding into another form. It’s far from always the case that I’d reach for those, but sometimes they’re just nice to have.

4 Likes
#12

Apparently someone else thought these were “good enough” for public release, too:

…they currently have a combined citation count of zero.

#13

I’m not arguing for manual examples like those presented in the paper. Instead, you should write proper functional code. For example the paper presents a “succinct” locally imperative implementation of findM:

def List.findM? (p : α → m Bool) (xs : List α) : m (Option α) := do
  for x in xs do
    let b ← p x
    if b then
      return some x
  return none

But in Haskell you can write it as an even more succinct composition of more and less common combinators:

findM :: Monad m => (a -> m Bool) -> [a] -> m (Maybe a)
findM p = runMaybeT . asum . map (MaybeT . guardedM p)

where

guardedM :: Functor f => (a -> f Bool) -> a -> f (Maybe a)
guardedM p x = (x <$) . guard <$> p x

Failing to mention idiomatic functional alternatives like these is a flaw in the paper. Only during the presentation Sebastian Ullrich briefly mentions “I mean yeah maybe there’s also some completely different way to write this code” (at 2:19), but then he immediately deflects with “but we did stumble over these patterns again and again”.

Is there an inverse operation to >>= (kinda)
#14

I would actually write the example like this, using Lean’s equivalent of Idris’s !-notation:

def List.findM? [Monad m] (p : α → m Bool) (xs : List α) : m (Option α) := do
  for x in xs do
    if (← p x) then
      return some x
  return none

As a fairly seasoned Haskeller, I find the combinator version fun, but I don’t think it’s actually easier to read, write, or understand than this version here. Nor do I think that it provides any more powerful opportunities for insight or any additional reasoning principles that would make me prefer it. I’m not saying that style of code never has its place, but this particular example is one where I think the extended do-notation is really great.

But now we’re back to individual idiosyncrasies as well as things about which reasonable people can disagree :slight_smile:

5 Likes
#15

HasFuse - Haskell with FUNDIO-based side effects:

  • non-strict semantics;

  • observable effects like mutation;

  • no alternate notation/syntax needed.

Enjoy.

#16

I’d totally take the extended do notation over the dumb one we have in Haskell. Local mutation and early return are quite useful features… Better than -XNonDecreasingIndentation and 5 closing braces of do-blocks, I suppose. I’m grateful I don’t have to look at that code so often.

But perhaps rather than waiting for someone championing a GHC proposal, I should simply move on to Koka :man_shrugging:

But in Haskell you can write it as an even more succinct composition of more and less common combinators:

I’d totally take the Lean definition of findM. It’s so much more elementary! I can grasp its definition in 5s, whereas that’s the time it would take me to figure out what asum does to a [MaybeT m a], where each element is some guardedM. No thanks, I like early return. I also like the Idris notation.

3 Likes
#17

Perhaps it would just be easier to have miranda or haskell-notation in the likes of Java or C++: mountains of [observable] effect-free code ascending from the vast wastelands of effect-addled imperativity with all the buzz reserved words and associated “semantics” that [almost] everyone else just can’t get enough of…

#18

MaybeT is early return (going back all the way to Moggi’s work on monads and monad transformers.)

This is going to sound very ivory tower-y, but I am not convinced that your preferences are based on anything more than just familiarity with imperative code. I would love to be proven wrong about this, but I fear that would require a very long and expensive research project.

And here’s a much more concrete benefit of the functional style: you can change the behavior of the function to return all possible results, instead of just the first one, by changing MaybeT to ListT (or monadic streams like from the vector-stream package although that has no alternative instance yet, I believe.) That’s a trivial change.

If you want to do that in imperative style then you either have to basically write a completely different function, or extend the language even further with something like Python’s yield.

4 Likes
#19

I’ve been thinking more about it; you can actually already get very close with just a custom transformer (actually it is just ExceptT with different names):

findM :: Monad m => (a -> m Bool) -> [a] -> m (Maybe a)
findM p xs = runEarlyT do
  for_ xs \x -> do
    b <- lift (p x)
    when b (earlyReturn (Just x))
  pure Nothing

So really the only difference with the new Lean syntax is that it requires two extra functions: runEarlyT and lift.

Click to expand the full implementation: 
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BlockArguments #-}
import Control.Monad ( ap, when )
import Control.Monad.Trans.Class ( MonadTrans(..) )
import Data.Foldable ( for_ )

newtype EarlyT r m a = EarlyT (m (Either r a)) deriving Functor

instance Monad m => Applicative (EarlyT r m) where
  pure x = EarlyT (pure (Right x))
  (<*>) = ap

instance Monad m => Monad (EarlyT r m) where
  EarlyT m >>= k = EarlyT $
    m >>= \case
      Left x -> pure (Left x)
      Right x | EarlyT y <- k x -> y

instance MonadTrans (EarlyT r) where
  lift :: Monad m => m a -> EarlyT r m a
  lift x = EarlyT (fmap Right x)

earlyReturn :: Applicative m => r -> EarlyT r m a
earlyReturn = EarlyT . pure . Left

runEarlyT :: Monad m => EarlyT a m a -> m a
runEarlyT (EarlyT m) = m >>= \case
  Left y -> pure y
  Right y -> pure y

findM :: Monad m => (a -> m Bool) -> [a] -> m (Maybe a)
findM p xs = runEarlyT do
  for_ xs \x -> do
    b <- lift (p x)
    when b (earlyReturn (Just x))
  pure Nothing
3 Likes
Foldl traverses with State, foldr traverses with anything
Fun with Eithers