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

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

@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
``````

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
``````

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

@rednaZ Do you have some example in mind?

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

I will have to try later.

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.

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.

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.)

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.

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.

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)

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.

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

@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`?

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.

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

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`?

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

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`.

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

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

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?

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

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.

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

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?

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)

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.

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)

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

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`.

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.

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 2`is 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`?