Effects representation in Haskell - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Kim-Ee Yeoh

How about this thing that Haskell still doesn't have?

http://math.andrej.com/2008/11/17/not-all-computational-effects-are-monads/

It puts the lie in the claim that Haskell is the world's finest imperative language.

TheMatten

@Kim-Ee Yeoh would this qualify?:

catch :: ((a -> Cont (Maybe a) b) -> Cont (Maybe a) c) -> Maybe a
catch f = evalCont $ Nothing <$ f \x -> shift \_ -> pure $ Just x
> catch (\g -> pure 42)
Nothing
> catch (\g -> pure \x -> g =<< g x)
Nothing
> catch (\g -> (+) <$> g 1 <*> g 2)
Just 1
TheMatten

It's not hard to implement the other too using the same functionality under State:

type Timeout a b = StateT Integer (Cont (Maybe a)) b

tick :: a -> Timeout b a
tick a = do
  t <- get
  if t - 1 < 0
    then lift $ shift \_ -> pure Nothing
    else put $ t - 1
  pure a

timeout :: Integer -> Timeout a a -> Maybe a
timeout n = flip runCont Just . flip evalStateT n
> timeout 5 (do x <- tick 7; y <- tick 5; return (x + y))
Just 12
> timeout 1 (do x <- tick 7; y <- tick 5; return (x + y))
Nothing
> timeout 5 let omega n = tick (n + 1) >>= omega in omega 0
Nothing
rednaZ

@TheMatten I do not know Cont so I might be missing your point but would the state monad not have sufficed?

TheMatten

@rednaZ Do you have some example in mind?

rednaZ

Ah, the problem might be coming up with a b.

rednaZ

I will have to try later.

rednaZ

So I tried it out and I guess, you already knew this, but here is the result anyway.

catch :: ((a -> State (Maybe a) b) -> State (Maybe a) c) -> Maybe a
catch f =
  execState (f g) Nothing
  where
    g :: a -> State (Maybe a) b
    g a =
      put (Just a) *>
      pure undefined
> catch (\g -> pure 42)
Nothing

> catch (\g -> pure (\x -> g =<< g x))
Nothing

> catch (\g -> (+) <$> g 1 <*> g 2)
Just 2

> catch (\g -> do {result <- g False; case result of {False -> pure True; True -> pure False}})
*** Exception: Prelude.undefined

So the two glaring problems are that we do not get the argument of the first invocation but of the last one and that divergence might happen where it is not supposed to.

rednaZ

we do not get the argument of the first invocation but of the last one

That is not actually a problem but a feature. You can get the argument of the first invocation if you want it.

catch :: ((a -> State (Maybe a) b) -> State (Maybe a) c) -> Maybe a
catch f =
  execState (f g) Nothing
  where
    g :: a -> State (Maybe a) b
    g a =
      modify (Just . fromMaybe a) *>
      pure undefined
> catch (\g -> pure 42)
Nothing

> catch (\g -> pure (\x -> g =<< g x))
Nothing

> catch (\g -> (+) <$> g 1 <*> g 2)
Just 1

> catch (\g -> do {result <- g False; case result of {False -> pure True; True -> pure False}})
*** Exception: Prelude.undefined

But the other more serious problem remains of course.

Kim-Ee Yeoh

TheMatten said:

Kim-Ee Yeoh would this qualify?:

catch :: ((a -> Cont (Maybe a) b) -> Cont (Maybe a) c) -> Maybe a
catch f = evalCont $ Nothing <$ f \x -> shift \_ -> pure $ Just x

Note that Andrej Bauer gives a similar implementation but with the type signature

katsch :: ((a -> Exception a b) -> Exception a c) -> Maybe a

As he notes, "This works but is unsatisfactory. I don’t want to simulate catch with exceptions. Is there a way to do catch directly? I do not know, since it is not even clear to me that we have a monad" (emphasis mine).

The backstory is actually here:

http://math.andrej.com/2006/03/27/sometimes-all-functions-are-continuous/

starting with the paragraph "The program m is called a modulus of continuity functional ...."

The function catch/katsch can be thought of as a simplification of the function m, written in Ocaml in the blogpost:

let m f x =
  let k = ref 0 in
  let y n = (k := max !k n; x n) in
    f y ; !k

Notice how in Ocaml, the modulus function doesn't monadify its type signature. This is crucial. It means that the function f given as input to m doesn't need to be retrofitted with effect combinators plastered all over it.

This manual retrofitting/rewriting of what is essentially a pure function must be performed for every function given as input to m.

Back to the first blogpost with catch: For instance, catch (\g -> 42) becomes katsch (\g -> return 42).

And catch (\g -> \x -> g (g x)) becomes katsch (\g -> return (\x -> do { y <- g x; z <- g y; return z })).

And catch (\g -> g 1 + g 2) becomes katsch (\g -> do { x <- g 1; y <- g 2; return (x + y)}).

I hope you see how intolerable this is. And this is how Haskell loses out to Ocaml for the title of world's finest imperative language.

(p.s. I actually don't hack Ocaml and find those *ML references an irredeemable spot of impurity on the language.)

TheMatten

Is there a way to do catch directly?

If it means to avoid short-circuiting through rest of computation and just returning the result, then that's what Cont does compared to Either.

But it probably means to not have to thread it through monadic context - in that case, that's nature of effectful computations in pure language - you have to have some notion of "threading", whether it's implicit on syntax level (Unison), or explicit (Haskell) - and in lazy language, you really need at least some syntax to distinguish it, though it could be more subtle, like e.g. do block that analyses types to automatically lift application into applicative operators in bindings

Notice how in Ocaml, the modulus function doesn't monadify its type signature.

That means that Ocaml isn't a pure language and assumes implicit context in all code - result is that first-class contexts are not as useful, because most interesting effects tend to be defined through this implicit one and thus can't be restricted or intercepted - you could enforce guidelines to not use it and model effects with first class structures and then... you end up with monads.

This manual retrofitting/rewriting of what is essentially a pure function must be performed for every function given as input to m.

"what is essentially" is actually "isn't" if we're precise - it's this tradeoff that if we want this mechanism to be actually useful, we have to stop "cheating" by using implicit context just to remove some syntactic overhead. I don't see why this is "intolerable" - it's a trade-off you learn to work with to get different advantages, and it's mostly straightforward plumbing. I think this plumbing could be made better, but it's not a trivial problem (probably reason why current approach is still status quo). While solution of OCaml and other languages is to just "give up" - fair enough, that works good enough for big chunk of software, but it's not an actual solution to the problem.

Kim-Ee Yeoh

TheMatten said:

This manual retrofitting/rewriting of what is essentially a pure function must be performed for every function given as input to m.

"what is essentially" is actually "isn't" if we're precise - it's this tradeoff that if we want this mechanism to be actually useful, we have to stop "cheating" by using implicit context just to remove some syntactic overhead.

It is understandable for catch to employ effects to produce its result. No-one is disputing that.

But the inputs to catch are pure. So why do they have to be rewritten with effect combinators?

Just to drive the point home, here's a type signature for a perfectly implementable catch:

catch :: (forall m. Monad m => (a -> m b) -> m r) -> Maybe a

Universal effect parametricity of the function input sets a tight effect upper bound on it. The input function can be no more effectful than when m = Identity. In other words, the input has to be pure!

All this points to something missing in Haskell. We should fix this.

TheMatten

It is understandable for catch to be effectful. No-one is disputing that.

But the inputs to catch are pure. So why do they have to be rewritten with effect combinators?

I guess it's actually the opposite way - catch is referentially transparent from the outside, while function passed in is effectful (catch is sort of an "effect interpreter")

The input function can be no more effectful than when m = Identity. In other words, the input has to be pure!

m is existential from the point of catch, so the input function a -> m b can use literally any m it wants, and thus it's not necessarily pure. Plus I'm not really sure how you implement exceptional behaviour just using Monad (ignoring fail, which was a quirk that is already solved in recent GHC versions)

Kim-Ee Yeoh

TheMatten said:

I guess it's actually the opposite way - catch is referentially transparent from the outside, while function passed in is effectful (catch is sort of an "effect interpreter")

I agree that catch is like an effect interpreter. But when you say that the function passed in is effectful, that is not quite the case.

We say that the Boolean function (&&) is pure. We also say that the image of it under liftM2 is ... well, an image of a pure function. The image is not effectful in the same way that putStr is effectful.

m is existential from the point of catch, so the input function a -> m b can use literally any m it wants, and thus it's not necessarily pure. Plus I'm not really sure how you implement exceptional behaviour just using Monad (ignoring fail, which was a quirk that is already solved in recent GHC versions)

An m existential from the point of catch would make the forall m unnecessary. The type signature would then become

broken :: Monad m => ((a -> m b) -> m r) -> Maybe a

This is not catch.

Have you tried implementing catch with the type signature given earlier? It will clarify things.

TheMatten

We say that the Boolean function (&&) is pure. We also say that the image of it under liftM2 is ... well, an image of a pure function. The image is not effectful in the same way that putStr is effectful.

You may use lifted pure functions throughout the function, but at some point you're going to use the provided callback, which is effectful, and thus the ultimate result is effectful too.

Sorry, I meant it as "catch gets to pick m" - it sounds to be the opposite the way I said it :sweat_smile: But the point still holds

Kim-Ee Yeoh

@TheMatten I think we are making progress in this conversation. I appreciate your participation in it.

So yes, catch gets to pick m. And lifted pure functions are a thing.

So if we return to the original catch scenario, why can't we lift the inputs to catch? Where are the effect combinators to do that?

-- These are the inputs to catch
k1 = \g -> 42
k2 = \g -> \x -> g (g x)
k3 = \g -> g 1 + g 2

Consider that Haskell wouldn't take off the way it did if we had to rewrite (&&) each time we used it in an effectful context.

Haskell wouldn't take off the way it did if we didn't have liftM2 and friends.

Where are the lift combinators for k1, k2, k3 to serve as input to catch?

TheMatten

I think we are making progress in this conversation. I appreciate your participation in it.

:heart:

Where are the lift combinators for k1, k2, k3 to serve as input to catch?

pure <$> k1
pure <$> k2

but in case of k3, ordering matters, while g 1 + g 2 in lazy language could be evaluated different ways depending on user of k3 and behaviour of (+). I've seen HS developers mention multiple times that reason they kept searching for solution to make effects in pure language possible (HS didn't use monads from the beginning), instead of making language impure, was that there wasn't other sensible option in presence of laziness.

TheMatten

In strict language, order of g 1 + g 2 is usually defined as "left-to-right, inside-to-outside", and really, Unison would let you write it like this while tracking effects properly, because it would be equivalent to (+) <$> g 1 <*> g 2 in Haskell

Kim-Ee Yeoh

TheMatten said:

In strict language, order of g 1 + g 2 is usually defined as "left-to-right, inside-to-outside", and really, Unison would let you write it like this while tracking effects properly, because it would be equivalent to (+) <$> g 1 <*> g 2 in Haskell

Fine, let's fix that order then.

So we have

liftM2 :: (a -> b -> c) -> (forall m. Monad m => m a -> m b -> m c)

even though there exists an isotypical function with a different order of effects.

Where is

lift :: ((a -> b) -> c) -> (forall m. Monad m => (a -> m b) -> m c)

so that we can pass lift k{1,2,3} to catch?

Kim-Ee Yeoh

Do you have a response other than, "Well that lift is in Unison, it's not in Haskell"?

TheMatten

Once you "prove" that you don't use b (using which would make your function effectful), you can do that:

lift' :: ((a -> ()) -> c) -> (forall m. Monad m => (a -> m b) -> m c)
lift' f = pure . f . (() <$)

But if you want to use b, then lift is not strong enough to give you that - it can only provide you with m b, which may depend on m.

TheMatten

(You could replace () with forall b. b BTW - where b is scoped over whole lift argument of course)

TheMatten

In Unison, all values are technically in sort of "extensible effects" monad that provides needed sequencing - and thus you never lift, you just "specialize"

Kim-Ee Yeoh

TheMatten said:

In Unison, all values are technically in sort of "extensible effects" monad that provides needed sequencing - and thus you never lift, you just "specialize"

You're saying that lift appears in Unison in the best way possible: invisibly and pre-applied to all the expressions it can possibly apply to.

The type system of Unison should be interesting. All a search yields is a parenthetical remark from

https://www.unisonweb.org/docs/language-reference/#user-defined-data-types

stating that "(See Types for an informal description of Unison's type system.)" This does not give confidence that the type system is fully cooked.

Do you know of an authoritative description of Unison's type system?

Kim-Ee Yeoh

That can't be it. I want the type system to Unison. The only language explicitly mentioned in the link you gave is Koka.

At this link: https://www.unisonweb.org/docs/language-reference/#types

we get: "Formally, Unison’s type system is an implementation of the system described by Joshua Dunfield and Neelakantan R. Krishnaswami in their 2013 paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism." https://arxiv.org/abs/1306.6032

It then goes on to say: "Unison extends that type system with, pattern matching, scoped type variables, ability types (also known as algebraic effects). See the section on Abilities for details on ability types."

And in the Abilities section we find this:

Unison's system of abilities (often called "algebraic effects" in the literature) is based on the Frank language by Sam Lindley, Conor McBride, and Craig McLaughlin. Unison diverges slightly from the scheme detailed in this paper. In particular:

  • Unison's ability polymorphism is provided by ordinary polymorphic types, and a Unison type with an empty ability set explicitly disallows any abilities. In Frank, the empty ability set implies an ability-polymorphic type.

  • Unison doesn't overload function application syntax to do ability handling; instead it has a separate handle construct for this purpose.

So what we are seeing is something cobbled together from at least 2 if not more papers with a dollop of Original Research (as wikipedia would describe it) spooned in for good measure.

How could things go wrong?!

Never mind a proof of soundness, it appears it's too much to ask for just ONE document describing the type system. Unison, it calls itself.

TheMatten

Hmm, yeah, would be nice for it to have formally proved soundness, but I guess it works good enough as an example here to get the idea about design space

Kim-Ee Yeoh

It's nice to savor the fruit of a proof of soundness and let the juice seep and nourish the programs written in the safety of the embodying type system.

What we should ask is where does such a tree come from?

And I submit that the answer lies in articulated and communicated design.

I've been informed that what I'm writing about Unison reads like kvetching for kvetching's sake.

That's far from the truth.

I write from a tradition that upholds the value of reflective work. The more complicated, novel, and unexplored the space; the more note-taking, reflection, and clarification-requesting dialogue is required.

Edsger Dijkstra is no longer with us. But Leslie Lamport is. And here he is underlining the need for a specification, a blueprint before building anything:

YouTube - Leslie Lamport: Thinking Above the Code

Drawing up a blueprint of a house is an example of reflective work. One imagines what one is building before reaching for the wood, the saws, the hammer, and the nails.

That's how Haskell was created. A large team of people with different ideas of what the language should look like, sifted through the best of them, and imagined a reality better than each one of them--on their own--could have visualized.

And once they've captured a clear vision of what they wanted to create, then--and only then--did they sit down at the keyboard to turn it into reality.

Not before.

Without specs, without blueprints, without documents describing the underpinnings of the design choices, any programming language exacts a massive tax on devs writing programs in it. Namely, the losers of such a language pay the imagination tax that the language designers absconded from.

Are there at least notes about the various design choices of Unison? I hope there are. And I'm not merely alluding to how GHC's repo is replete with notes all over.

Searching on "haskell design choices" will give you documents that have explored the design space of various aspects of Haskell.

Are there such documents pertaining to Unison?

TheMatten

I'm not arguing with you, but I wasn't really interested in talking about Unison - I just used it as an example of design that makes use of strictness that I'm familiar with
If we want to talk about need for strong design (about which I agree with you fully), we should probably move it into separate topic :smile:
(I mean, I should probably split this discussion from this topic, because it's not really related too :big_smile: - edit: done)

Kim-Ee Yeoh

TheMatten said:

Once you "prove" that you don't use b (using which would make your function effectful), you can do that:

lift' :: ((a -> ()) -> c) -> (forall m. Monad m => (a -> m b) -> m c)
lift' f = pure . f . (() <$)

But if you want to use b, then lift is not strong enough to give you that - it can only provide you with m b, which may depend on m.

TheMatten said:

(You could replace () with forall b. b BTW - where b is scoped over whole lift argument of course)

You've lost me about the use of b making the input function effectful.

Isn't it obvious that all the following are pure?

-- These are the inputs to catch
k1 = \g -> 42
k2 = \g -> \x -> g (g x)
k3 = \g -> g 1 + g 2

They all have the type signature (A -> B) -> C, for appropriately pure type values of A, B, and C.

Let me repeat the request: where is this function

lift :: ((a -> b) -> c) -> (forall m. Monad m => (a -> m b) -> m c)

so that we can feed lift k{1,2,3} into

catch :: (forall m. Monad m => (a -> m b) -> m c) -> Maybe a

?

We make progress in this convo by either

  1. Providing lift
  2. Showing that lift cannot be written in existing Haskell

If it's the latter, we can then proceed to investigate what's missing that we can add to the language.

TheMatten

You've lost me about the use of b making the input function effectful.

If in definition of catch you say that you can provide a -> m b, you're saying that user can get b as long as they can both provide a and get it from m - that means that they have to thread through m, because they have to account for possibility of m being something other than pure and thus possibility of b not being directly retrievable, but they can't just fmap inside, because that m can depend on a according to the signature - thus they have to account for effects, even though they're not using them in their implemetantion

Isn't it obvious that all the following are pure?

First two are (you can use pure), but the third isn't - even though it only does effects through g, it does them - and in that case ordering matters, but pure code in Haskell doesn't give you any.
So I'm going to say that 2. holds, because lazy semantics is in a sense "bigger" than strict, providing multiple orders of evaluation which would result in different behaviour in presence of effects. Solution is to either ditch laziness globally (getting strict language), or locally (using e.g. applicative operators or special syntax to specify order)

TheMatten

In those local pieces of code, you can then "specialize" easily, because they have their order of evaluation specified (enough)

Kim-Ee Yeoh

TheMatten said:

You've lost me about the use of b making the input function effectful

If in definition of catch you say that you can provide a -> m b, you're saying that user can get b as long as they can both provide a and get it from m - that means that they have to thread through m, because they have to account for possibility of m being something other than pure and thus possibility of b not being directly retrievable, but they can't just fmap inside, because that m can depend on a according to the signature - thus they have to account for effects, even though they're not using them in their implemetantion

This leaves me even more confused than before. How can m depend on a? There are no dependent types anywhere!

You are aware that universal polymorphism is an extremely constraining attribute? A function Nat -> Nat could be any infinite number of possibilities. But a function forall a. a -> a can only be one.

Similarly I call verytrue in the snippet below pure, notwithstanding the presence of m, although I concede that there are good arguments to call it lifted pure instead of unqualified pure.

verytrue :: forall m. Monad m => m Bool
verytrue = pure True

Also, this focus on catch seems entirely misplaced. We have catch. We don't have lift. Why can't we write lift?

First two are (you can use pure), but the third isn't - even though it only does effects through g, it does them - and in that case ordering matters, but pure code in Haskell doesn't give you any.

How is k3 not pure?! Here, I'll even give you the type signature:

k3 :: (Int -> Int) -> Int
k3 = \g -> g 1 + g 2

You say that "ordering matters" as if that's what's blocking us from writing lift. Well, liftM2 as I mentioned earlier has a choice of order as well. The existence of liftM2 is not disputed, is it? But we don't have lift. Why?

So I'm going to say that 2. holds, because lazy semantics is in a sense "bigger" than strict, providing multiple orders of evaluation which would result in different behaviour in presence of effects. Solution is to either ditch laziness globally (getting strict language), or locally (using e.g. applicative operators or special syntax to specify order)

Your reason doesn't hit the nail. Despite lazy semantics being bigger than strict, we have a whole bunch of effect combinators like fmap, >>=, liftM2 that lift the smaller into the bigger. But the particular lift that we want is missing. Why?

I hate repeating myself like this. But this convo seems to keep veering off the rails. Focus on the missing lift.

TheMatten

This leaves me even more confused than before. How can m depend on a? There are no dependent types anywhere!

I mean as in "effect in result can depend on that input argument"

You are aware that universal polymorphism is an extremely constraining attribute? A function Nat -> Nat could be any infinite number of possibilities. But a function forall a. a -> a can only be one.

Yeah, that's the point

How is k3 not pure?! Here, I'll even give you the type signature:

From perspective of pure language, g is not pure and not of type Int -> Int

The existence of liftM2 is not disputed, is it?

liftM2 can define ordering, because it retrieves f a b decomposed into it's parts - but lift as declared above is trying to somehow inspect it's argument to do that - that's what meta-level constructs can do, but not normal functions.

Kim-Ee Yeoh

Gatekeepers don't have friends, they have bootlickers instead. That said, I must say that your assertion that g is not pure in k3 = \g -> g 1 + g 2is as incorrect as it is bizarre, especially when I've already explicitly scoped the type of k3 :: (Int -> Int) -> Int.

What "perspective of pure language" is this that leads you to such a judgment? Have you considered that such a perspective may be misleading?

Be it as it may, in the interest of being constructive, what minimal construct--whether meta-level or otherwise--do you see as being required to write such a lift?