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.
Note that Andrej Bauer gives a similar implementation but with the type signature
katsch::((a->Exceptionab)->Exceptionac)->Maybea
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).
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:
letmfx=letk=ref0inletyn=(k:=max!kn;xn)infy;!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.)
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.
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 catchare 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::(forallm.Monadm=>(a->mb)->mr)->Maybea
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 catchare 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)
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 putStris 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::Monadm=>((a->mb)->mr)->Maybea
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
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<$>k1pure<$>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
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)->(forallm.Monadm=>ma->mb->mc)
even though there exists an isotypical function with a different order of effects.
In Unison, all values are technically in sort of "extensible effects" monad that provides needed sequencing - and thus you never lift, you just "specialize"
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
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:
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.
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)
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)
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::forallm.Monadm=>mBoolverytrue=pureTrue
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)->Intk3=\g->g1+g2
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 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?
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.
@Kim-Ee Yeoh would this qualify?:
It's not hard to implement the other too using the same functionality under
State
:@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.
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.
That is not actually a problem but a feature. You can get the argument of the first invocation if you want it.
But the other more serious problem remains of course.
TheMatten said:
Note that Andrej Bauer gives a similar implementation but with the type signature
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:
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)
becomeskatsch (\g -> return 42)
.And
catch (\g -> \x -> g (g x))
becomeskatsch (\g -> return (\x -> do { y <- g x; z <- g y; return z }))
.And
catch (\g -> g 1 + g 2)
becomeskatsch (\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.)
If it means to avoid short-circuiting through rest of computation and just returning the result, then that's what
Cont
does compared toEither
.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 bindingsThat 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.
"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:
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
: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.
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")m
is existential from the point ofcatch
, so the input functiona -> m b
can use literally anym
it wants, and thus it's not necessarily pure. Plus I'm not really sure how you implement exceptional behaviour just usingMonad
(ignoringfail
, which was a quirk that is already solved in recent GHC versions)TheMatten said:
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 underliftM2
is ... well, an image of a pure function. The image is not effectful in the same way thatputStr
is effectful.An
m
existential from the point ofcatch
would make theforall m
unnecessary. The type signature would then becomeThis is not
catch
.Have you tried implementing
catch
with the type signature given earlier? It will clarify things.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 pickm
" - 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 pickm
. 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?
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 tocatch
?:heart:
but in case of
k3
, ordering matters, whileg 1 + g 2
in lazy language could be evaluated different ways depending on user ofk3
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 HaskellWhat is HS?
Haskell
TheMatten said:
Fine, let's fix that order then.
So we have
even though there exists an isotypical function with a different order of effects.
Where is
so that we can pass
lift k{1,2,3}
tocatch
?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:But if you want to use
b
, thenlift
is not strong enough to give you that - it can only provide you withm b
, which may depend onm
.(You could replace
()
withforall b. b
BTW - whereb
is scoped over wholelift
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:
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?
AFAIK they're pretty canonical implementation of algebraic effects, see e.g. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/algeff-tr-2016-v2.pdf
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:
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:
TheMatten said:
You've lost me about the use of
b
making the input function effectful.Isn't it obvious that all the following are pure?
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
so that we can feed
lift k{1,2,3}
into?
We make progress in this convo by either
lift
lift
cannot be written in existing HaskellIf it's the latter, we can then proceed to investigate what's missing that we can add to the language.
If in definition of
catch
you say that you can providea -> m b
, you're saying that user can getb
as long as they can both providea
and get it fromm
- that means that they have to thread throughm
, because they have to account for possibility ofm
being something other thanpure
and thus possibility ofb
not being directly retrievable, but they can't justfmap
inside, because thatm
can depend ona
according to the signature - thus they have to account for effects, even though they're not using them in their implemetantionFirst two are (you can use
pure
), but the third isn't - even though it only does effects throughg
, 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:
This leaves me even more confused than before. How can
m
depend ona
? 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 functionforall a. a -> a
can only be one.Similarly I call
verytrue
in the snippet below pure, notwithstanding the presence ofm
, although I concede that there are good arguments to call it lifted pure instead of unqualified pure.Also, this focus on
catch
seems entirely misplaced. We havecatch
. We don't havelift
. Why can't we writelift
?How is
k3
not pure?! Here, I'll even give you the type signature: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 ofliftM2
is not disputed, is it? But we don't havelift
. Why?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 particularlift
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
.I mean as in "effect in result can depend on that input argument"
Yeah, that's the point
From perspective of pure language,
g
is not pure and not of typeInt -> Int
liftM2
can define ordering, because it retrievesf a b
decomposed into it's parts - butlift
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 ink3 = \g -> g 1 + g 2
is as incorrect as it is bizarre, especially when I've already explicitly scoped the type ofk3 :: (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
?