Re: RFC: Add HasCallStack constraint to partial Data.List functions.
-1 for the reasons Henrik has listed Dominic Steinitz dominic@steinitz.org http://idontgetoutmuch.org Twitter: @idontgetoutmuch
On 5 Jun 2021, at 11:10, libraries-request@haskell.org wrote:
Re: RFC: Add HasCallStack constraint to partial Data.List functions.
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed. So, may I propose a slightly different way forward? Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial. * We have some room in how we relate IsPartial to HasCallStack. We could say that IsPartial is just a synonym for HasCallStack (e.g. with type IsPartial = HasCallStack). But perhaps better would be to somehow give users control over whether they want the HasCallStack mechanism to be able to solve IsPartial constraints. Maybe some users would prefer not to be able to satisfy IsPartial constraints immediately, but instead to require an acknowledgement in their code that they're doing something partial. For example: partialityIsOK :: String -> (IsPartial => r) -> r elements xs = map (partialityIsOK "lists returned by `group` are always non-empty" head) (group xs) The partialityIsOK function has a more involved type than I would like, but it's very usable in practice. Of course, such a thing only makes sense if IsPartial cannot automatically be satisfied. Getting this to work properly probably needs an extra language feature (maybe make IsPartial magically built-in?), but it might provide a declarative, yet operationally practical way forward here. Richard
On Jun 6, 2021, at 12:49 PM, Dominic Steinitz <dominic@steinitz.org> wrote:
-1 for the reasons Henrik has listed
Dominic Steinitz dominic@steinitz.org <mailto:dominic@steinitz.org> http://idontgetoutmuch.org Twitter: @idontgetoutmuch
On 5 Jun 2021, at 11:10, libraries-request@haskell.org <mailto:libraries-request@haskell.org> wrote:
Re: RFC: Add HasCallStack constraint to partial Data.List functions.
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
On Tue, 8 Jun 2021, at 6:36 PM, Richard Eisenberg wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial.
I don't think this is true. Take: foo :: Int -> Bool foo _ = head [True] Clearly foo is total - it is defined for all of its inputs. That it uses a partial function in its body isn't observable. So it's a shame that IsPartial leaks out. I guess here you'd have me say foo _ = partialityIsOk $ head [True] ? Ollie
Yeah, I think a typeclass to express partiality is a sloppy technique. I'm not even sure everyone agrees on what 'partial' means: if my function throws an IO error on relative FilePaths, is it partial? Is all IO partial? Haskell is definitely not a total language and I doubt it will be. I also don't think that it's an interesting goal. It requires a considerable shift in language design. HasCallstack sounds like a pragmatic solution, but you could as well create an alternative prelude that adds it everywhere you want and then avoid implicit prelude. That won't help you with unsound dependencies, that don't use it, but it's opt-in, which seems more reasonable given that it's obviously a somewhat controversial change. I'd expect the nay-sayers here, however, to be a driving force in a better GHC based solution. Otherwise, the next time this comes up people will say "you had time enough". On June 8, 2021 6:10:52 PM UTC, Oliver Charles <ollie@ocharles.org.uk> wrote:
On Tue, 8 Jun 2021, at 6:36 PM, Richard Eisenberg wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial.
I don't think this is true.
Take:
foo :: Int -> Bool foo _ = head [True]
Clearly foo is total - it is defined for all of its inputs. That it uses a partial function in its body isn't observable. So it's a shame that IsPartial leaks out.
I guess here you'd have me say
foo _ = partialityIsOk $ head [True]
?
Ollie
Let's not diverge too much on the nature of IO functions, in the context of this conversation, here are the functions that are partial: - head, tail, init, last, ... - foldr1, foldl1, maximum, minimum, ... - (!!) They all have in common the usage of `error(WithoutStackTrace)`, so we can safely say that 'partial ~ using error(WithoutStackTrace)' in the context of this RFC. Le 09/06/2021 à 09:31, Julian Ospald a écrit :
Yeah, I think a typeclass to express partiality is a sloppy technique. I'm not even sure everyone agrees on what 'partial' means: if my function throws an IO error on relative FilePaths, is it partial? Is all IO partial?
Haskell is definitely not a total language and I doubt it will be. I also don't think that it's an interesting goal. It requires a considerable shift in language design.
HasCallstack sounds like a pragmatic solution, but you could as well create an alternative prelude that adds it everywhere you want and then avoid implicit prelude. That won't help you with unsound dependencies, that don't use it, but it's opt-in, which seems more reasonable given that it's obviously a somewhat controversial change.
I'd expect the nay-sayers here, however, to be a driving force in a better GHC based solution. Otherwise, the next time this comes up people will say "you had time enough".
On June 8, 2021 6:10:52 PM UTC, Oliver Charles <ollie@ocharles.org.uk> wrote:
On Tue, 8 Jun 2021, at 6:36 PM, Richard Eisenberg wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
> head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial.
I don't think this is true.
Take:
foo :: Int -> Bool foo _ = head [True]
Clearly foo is total - it is defined for all of its inputs. That it uses a partial function in its body isn't observable. So it's a shame that IsPartial leaks out.
I guess here you'd have me say
foo _ = partialityIsOk $ head [True]
?
Ollie
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW: https://glitchbra.in RUN: BSD
I'm aware what was meant, but this was in response to the proposed 'IsPartial' typeclass, which will have this confusion pop up more often. On June 9, 2021 7:48:58 AM UTC, "Hécate" <hecate@glitchbra.in> wrote:
Let's not diverge too much on the nature of IO functions, in the context of this conversation, here are the functions that are partial:
- head, tail, init, last, ... - foldr1, foldl1, maximum, minimum, ... - (!!)
They all have in common the usage of `error(WithoutStackTrace)`, so we can safely say that 'partial ~ using error(WithoutStackTrace)' in the context of this RFC.
Le 09/06/2021 à 09:31, Julian Ospald a écrit :
Yeah, I think a typeclass to express partiality is a sloppy technique. I'm not even sure everyone agrees on what 'partial' means: if my function throws an IO error on relative FilePaths, is it partial? Is all IO partial?
Haskell is definitely not a total language and I doubt it will be. I also don't think that it's an interesting goal. It requires a considerable shift in language design.
HasCallstack sounds like a pragmatic solution, but you could as well create an alternative prelude that adds it everywhere you want and then avoid implicit prelude. That won't help you with unsound dependencies, that don't use it, but it's opt-in, which seems more reasonable given that it's obviously a somewhat controversial change.
I'd expect the nay-sayers here, however, to be a driving force in a better GHC based solution. Otherwise, the next time this comes up people will say "you had time enough".
On June 8, 2021 6:10:52 PM UTC, Oliver Charles <ollie@ocharles.org.uk> wrote:
On Tue, 8 Jun 2021, at 6:36 PM, Richard Eisenberg wrote:
I've been very much of two minds in this debate: On the one
hand,
having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that
we're
letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
> head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial.
I don't think this is true.
Take:
foo :: Int -> Bool foo _ = head [True]
Clearly foo is total - it is defined for all of its inputs. That it uses a partial function in its body isn't observable. So it's a shame that IsPartial leaks out.
I guess here you'd have me say
foo _ = partialityIsOk $ head [True]
?
Ollie
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW: https://glitchbra.in RUN: BSD
But nothing prevents us from agreeing on restricting the semantics of `IsPartial` ! We can write down in the Haddocks “`IsPartial` should exclusively be used for functions that use error/errorWithoutStackTrace, and not for imprecise exceptions or asynchronous exceptions.” We have documentation, guides, tutorials, comments, style guides, etc. I just don't understand why it is a problem. And again, this is not a discussion that is unique to us. The PureScript community have had their own Partial typeclass for ages and this hasn't triggered the end of the world. We don't have to delve into year-long arguments on The Nature of Partiality. --- rant --- As a general comment, it is honestly appalling how RFCs like that trigger such circlejerks that are so utterly disconnected from reality. This does not make us better as a community. The last time I suggested a change in the base library (up-streaming strictness optimisations that were enabled at the first level of optimisation), I've was told that this went against the spirit of the language, even though a simple look at the most minor optimisation level would reveal that we haven't been "true" to this "spirit" for a long, long time. And this is extremely bizarre since we try to take the highest moral stances on some topics whilst making dirty compromises on other topics (for which I am not seeing anyone actively try to change the status quo).
It's been well known for close to three decades(!) that it is perfectly possible to add sophisticated debugging support to lazy languages like Haskell without impacting on the language semantics or formulation of its libraries. The existing tracing and profiling mechanisms of GHC are examples of this.
Henrik, Debug.Trace functions requires the use of "unsafePerformIO". Is this really the sort of thing we want to promote when we talk about "sophisticated debugging support to lazy languages without impacting the semantics"? Looks like the semantics of pure functional programming are flushed down the toilets with that one. Regarding profiling, we are *unable* to teach how it works. The Haskell Wiki article¹ is a stub, there are issues² on the Cabal bug tracker to ask how to enable it, and for most people it's still a mystery. So before we say things like "It's been well known for close to three decades(!)(sic)", I suggest we get our shit together because right now we look like a bunch of clowns. And if by any chance the University of Nottingham has a secret vault of forbidden techniques regarding profiling Haskell applications, I'd love that the rest of the community could benefit from this 30yo knowledge, since apparently nothing has filtered and we are still like monkey playing with sticks in the outside world. So let's meditate on this a bit, shall we? As much as I am not the biggest fan of ad-hoc typeclasses to signal operational behaviour, the inability of the community to promote the "better" ways to handle such failure modes makes me think that we have no right to spit on this RFC. --- ¹ https://wiki.haskell.org/How_to_profile_a_Haskell_program ² https://github.com/haskell/cabal/issues/5930 Le 09/06/2021 à 09:57, Julian Ospald a écrit :
I'm aware what was meant, but this was in response to the proposed 'IsPartial' typeclass, which will have this confusion pop up more often.
On June 9, 2021 7:48:58 AM UTC, "Hécate" <hecate@glitchbra.in> wrote:
Let's not diverge too much on the nature of IO functions, in the context of this conversation, here are the functions that are partial:
- head, tail, init, last, ... - foldr1, foldl1, maximum, minimum, ... - (!!)
They all have in common the usage of `error(WithoutStackTrace)`, so we can safely say that 'partial ~ using error(WithoutStackTrace)' in the context of this RFC.
Le 09/06/2021 à 09:31, Julian Ospald a écrit :
Yeah, I think a typeclass to express partiality is a sloppy technique. I'm not even sure everyone agrees on what 'partial' means: if my function throws an IO error on relative FilePaths, is it partial? Is all IO partial?
Haskell is definitely not a total language and I doubt it will be. I also don't think that it's an interesting goal. It requires a considerable shift in language design.
HasCallstack sounds like a pragmatic solution, but you could as well create an alternative prelude that adds it everywhere you want and then avoid implicit prelude. That won't help you with unsound dependencies, that don't use it, but it's opt-in, which seems more reasonable given that it's obviously a somewhat controversial change.
I'd expect the nay-sayers here, however, to be a driving force in a better GHC based solution. Otherwise, the next time this comes up people will say "you had time enough".
On June 8, 2021 6:10:52 PM UTC, Oliver Charles <ollie@ocharles.org.uk> wrote:
On Tue, 8 Jun 2021, at 6:36 PM, Richard Eisenberg wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
> head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial.
I don't think this is true.
Take:
foo :: Int -> Bool foo _ = head [True]
Clearly foo is total - it is defined for all of its inputs. That it uses a partial function in its body isn't observable. So it's a shame that IsPartial leaks out.
I guess here you'd have me say
foo _ = partialityIsOk $ head [True]
?
Ollie
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW:https://glitchbra.in RUN: BSD
-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW: https://glitchbra.in RUN: BSD
hi Hécate, On 06/09/2021 09:44 AM, Hécate wrote:
Henrik, Debug.Trace functions requires the use of "unsafePerformIO". Is this really the sort of thing we want to promote when we talk about "sophisticated debugging support to lazy languages without impacting the semantics"? Looks like the semantics of pure functional programming are flushed down the toilets with that one.
Not at all what I was saying. See http://www.cs.nott.ac.uk/~psznhn/Publications/thesis-henni.ps.gz for but one example. No unsafePerformIO needed, as it happens Tool support is obviously needed, though, but of pretty much exactly the kind that is already present for profiling. (Not that unsafePerformIO would be a problem as an internal implementation technique, for that matter.)
As a general comment, it is honestly appalling how RFCs like that trigger such circlejerks that are so utterly disconnected from reality.
With respect (and I always do try to maintain a respectful tone), I think that is a deeply unfair comment. I do not see what the purported reality disconnect is with observing that HasCallStack is an operational annotation that has no place in declarative type signatures (as others also have observed), with observing that there are implications for education that ought to be considered, that whenever types of basic functions that have been around since Haskell was created changes, that has implications for no end of books and other literature, and reminding people that there are non-intrusive techniques, for which the required infrastructure pretty much is in place, that would provide a comprehensive solution to proper stack traces. On the contrary, this broader perspective is what is needed to properly account for "reality", and soliciting that perspective is the very point of an RFC, I would have thought. And given the above comment that seems to suggest that Debug.Trace and unsafePerformIO are the only ways to go about debugging in pure languages, maybe the last point about reminding the community about alternatives is particularly apt. Respectfully, /Henrik This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.
| HasCallStack is an operational annotation that has no place in declarative | type signatures I'm not sure I really agree with that. There is a rich literature on effect systems, which decorate types with information about what effects the function has: exceptions, divergence, IO, and the like. So type like head :: Partial => [a] -> a where 'Partial =>' expresses the fact that calling this function might lead to a call of 'error' doesn't seem inherently something that doesn't belong in a type system. Indeed if `error :: Partial => String -> a`, then we can guarantee that any function that calls error will need a Partial constraint... it propagates upward as it should. TL;DR none of this seems (to me) inappropriate for a declarative type system. Simon
I'm not sure I really agree with that. There is a rich literature on effect systems, which decorate types with information about what effects the function has: exceptions, divergence, IO, and the like. So type like head :: Partial => [a] -> a where 'Partial =>' expresses the fact that calling this function might lead to a call of 'error' doesn't seem inherently something that doesn't belong in a type system.
I, of course, agree that partiality is an effect. And I have no issues with effects being reflected in the type system. We do that all the time with e.g. monads. If we indeed had something like head :: Partial => [a] -> a that would be both informative and fairly straightforward to explain to students, for example. (Even if it is not clear to me that a type class really is the right way to express partiality of functions: I always thought information about partiality ought to be tied to the function arrow.) My point is that "HasCallStack" strongly suggest a specific approach to monitor the behaviour of a function in case it goes wrong. To me, at least, that is very operational. And I would struggle to explain head :: HasCallStack => [a] -> a beyond saying "it's just something that sometimes will help you with debugging", and deeply hoping no clever student would ask about the lack of similar annotations for other partial functions. Best, /Henrik This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.
FWIW, partiality annotations seem a bit silly to me when we don't have termination checking. On Wed, Jun 9, 2021, 9:45 AM Henrik Nilsson <Henrik.Nilsson@nottingham.ac.uk> wrote:
I'm not sure I really agree with that. There is a rich literature on effect systems, which decorate types with information about what effects the function has: exceptions, divergence, IO, and the like. So type like head :: Partial => [a] -> a where 'Partial =>' expresses the fact that calling this function might lead to a call of 'error' doesn't seem inherently something that doesn't belong in a type system.
I, of course, agree that partiality is an effect. And I have no issues with effects being reflected in the type system. We do that all the time with e.g. monads.
If we indeed had something like
head :: Partial => [a] -> a
that would be both informative and fairly straightforward to explain to students, for example. (Even if it is not clear to me that a type class really is the right way to express partiality of functions: I always thought information about partiality ought to be tied to the function arrow.)
My point is that "HasCallStack" strongly suggest a specific approach to monitor the behaviour of a function in case it goes wrong.
To me, at least, that is very operational.
And I would struggle to explain
head :: HasCallStack => [a] -> a
beyond saying "it's just something that sometimes will help you with debugging", and deeply hoping no clever student would ask about the lack of similar annotations for other partial functions.
Best,
/Henrik
This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.
Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
I want to quickly chime in that I agree with Hécate's rant. The lack of stack traces for things like `head` are a well known problem in Haskell. We have a reasonable solution on hand, namely `HasCallStack`. It seems clear to me that we should use it. As already mentioned, PureScript has a `Partial` type class. I have used PureScript a little, and I found the `Partial` type class to be reasonable. I would be curious to hear from professional PureScript developers about their experience with the `Partial` type class. (Also note that it has *excellent* documentation already: <https://pursuit.purescript.org/packages/purescript-partial/3.0.0 <https://pursuit.purescript.org/packages/purescript-partial/3.0.0>>.) Discussing if `IsPartial` is a better name seems like a good way to turn this into a drawn out bike shedding argument.
On Jun 9, 2021, at 9:48 AM, David Feuer <david.feuer@gmail.com> wrote:
FWIW, partiality annotations seem a bit silly to me when we don't have termination checking.
On Wed, Jun 9, 2021, 9:45 AM Henrik Nilsson <Henrik.Nilsson@nottingham.ac.uk <mailto:Henrik.Nilsson@nottingham.ac.uk>> wrote:
I'm not sure I really agree with that. There is a rich literature on effect systems, which decorate types with information about what effects the function has: exceptions, divergence, IO, and the like. So type like head :: Partial => [a] -> a where 'Partial =>' expresses the fact that calling this function might lead to a call of 'error' doesn't seem inherently something that doesn't belong in a type system.
I, of course, agree that partiality is an effect. And I have no issues with effects being reflected in the type system. We do that all the time with e.g. monads.
If we indeed had something like
head :: Partial => [a] -> a
that would be both informative and fairly straightforward to explain to students, for example. (Even if it is not clear to me that a type class really is the right way to express partiality of functions: I always thought information about partiality ought to be tied to the function arrow.)
My point is that "HasCallStack" strongly suggest a specific approach to monitor the behaviour of a function in case it goes wrong.
To me, at least, that is very operational.
And I would struggle to explain
head :: HasCallStack => [a] -> a
beyond saying "it's just something that sometimes will help you with debugging", and deeply hoping no clever student would ask about the lack of similar annotations for other partial functions.
Best,
/Henrik
This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.
Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.
_______________________________________________ Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries> _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
| If we indeed had something like | | head :: Partial => [a] -> a | | that would be both informative and fairly straightforward to explain to | students, for example. (Even if it is not clear to me that a type class | really is the right way to express partiality of functions: I always thought | information about partiality ought to be tied to the function arrow.) OK -- that sounds promising. It's what Richard suggested earlier, and sounds pretty good to me. Simon | -----Original Message----- | From: Henrik.Nilsson@nottingham.ac.uk <Henrik.Nilsson@nottingham.ac.uk> | Sent: 09 June 2021 14:45 | To: Simon Peyton Jones <simonpj@microsoft.com>; Henrik Nilsson | <Henrik.Nilsson@nottingham.ac.uk>; libraries@haskell.org | Subject: Re: RFC: Add HasCallStack constraint to partial Data.List | functions. | | > I'm not sure I really agree with that. There is a rich literature on > | effect systems, which decorate types with information about what > effects | the function has: exceptions, divergence, IO, and the like. | > So type like | > head :: Partial => [a] -> a | > where 'Partial =>' expresses the fact that calling this function > might | lead to a call of 'error' doesn't seem inherently something > that doesn't | belong in a type system. | | I, of course, agree that partiality is an effect. And I have no issues with | effects being reflected in the type system. | We do that all the time with e.g. monads. | | If we indeed had something like | | head :: Partial => [a] -> a | | that would be both informative and fairly straightforward to explain to | students, for example. (Even if it is not clear to me that a type class | really is the right way to express partiality of functions: I always thought | information about partiality ought to be tied to the function arrow.) | | My point is that "HasCallStack" strongly suggest a specific approach to | monitor the behaviour of a function in case it goes wrong. | | To me, at least, that is very operational. | | And I would struggle to explain | | head :: HasCallStack => [a] -> a | | beyond saying "it's just something that sometimes will help you with | debugging", and deeply hoping no clever student would ask about the lack of | similar annotations for other partial functions. | | Best, | | /Henrik | | | | This message and any attachment are intended solely for the addressee and | may contain confidential information. If you have received this message in | error, please contact the sender and delete the email and attachment. | | Any views or opinions expressed by the author of this email do not | necessarily reflect the views of the University of Nottingham. Email | communications with the University of Nottingham may be monitored where | permitted by law. | | |
The sad part is seemingly it discards having an informative stack trace? On Wed, Jun 9, 2021 at 10:16 AM Simon Peyton Jones via Libraries < libraries@haskell.org> wrote:
| If we indeed had something like | | head :: Partial => [a] -> a | | that would be both informative and fairly straightforward to explain to | students, for example. (Even if it is not clear to me that a type class | really is the right way to express partiality of functions: I always thought | information about partiality ought to be tied to the function arrow.)
OK -- that sounds promising. It's what Richard suggested earlier, and sounds pretty good to me.
Simon
| -----Original Message----- | From: Henrik.Nilsson@nottingham.ac.uk <Henrik.Nilsson@nottingham.ac.uk> | Sent: 09 June 2021 14:45 | To: Simon Peyton Jones <simonpj@microsoft.com>; Henrik Nilsson | <Henrik.Nilsson@nottingham.ac.uk>; libraries@haskell.org | Subject: Re: RFC: Add HasCallStack constraint to partial Data.List | functions. | | > I'm not sure I really agree with that. There is a rich literature on > | effect systems, which decorate types with information about what > effects | the function has: exceptions, divergence, IO, and the like. | > So type like | > head :: Partial => [a] -> a | > where 'Partial =>' expresses the fact that calling this function > might | lead to a call of 'error' doesn't seem inherently something > that doesn't | belong in a type system. | | I, of course, agree that partiality is an effect. And I have no issues with | effects being reflected in the type system. | We do that all the time with e.g. monads. | | If we indeed had something like | | head :: Partial => [a] -> a | | that would be both informative and fairly straightforward to explain to | students, for example. (Even if it is not clear to me that a type class | really is the right way to express partiality of functions: I always thought | information about partiality ought to be tied to the function arrow.) | | My point is that "HasCallStack" strongly suggest a specific approach to | monitor the behaviour of a function in case it goes wrong. | | To me, at least, that is very operational. | | And I would struggle to explain | | head :: HasCallStack => [a] -> a | | beyond saying "it's just something that sometimes will help you with | debugging", and deeply hoping no clever student would ask about the lack of | similar annotations for other partial functions. | | Best, | | /Henrik | | | | This message and any attachment are intended solely for the addressee and | may contain confidential information. If you have received this message in | error, please contact the sender and delete the email and attachment. | | Any views or opinions expressed by the author of this email do not | necessarily reflect the views of the University of Nottingham. Email | communications with the University of Nottingham may be monitored where | permitted by law. | | |
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
I wonder if we can keep our nice separation of types being declarative and terms being operational by augmenting Richard's proposed partialityIsOK :: String -> (Partial => r) -> r with partialityIsOKWithCallStack :: String -> (Partial => r) -> r Then it would become the call site's choice whether to ask for a call stack rather than just unilaterally providing one whether the caller wants it or not (which I believe is the current situation -- I admit I don't understand HasCallStack). Tom On Wed, Jun 09, 2021 at 11:51:12AM -0400, Carter Schonwald wrote:
The sad part is seemingly it discards having an informative stack trace?
On Wed, Jun 9, 2021 at 10:16 AM Simon Peyton Jones via Libraries < libraries@haskell.org> wrote:
| If we indeed had something like | | head :: Partial => [a] -> a | | that would be both informative and fairly straightforward to | explain to students, for example. (Even if it is not clear to | me that a type class really is the right way to express | partiality of functions: I always thought information about | partiality ought to be tied to the function arrow.)
OK -- that sounds promising. It's what Richard suggested earlier, and sounds pretty good to me.
On Tue, Jun 8, 2021, 1:39 PM Richard Eisenberg <lists@richarde.dev> wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type).
Yes, this is quite awkward. We have here a tension: 1. The *operational* type, indicating the calling convention. This includes HasCallStack. 2. The "denotational" type (for want of a better term), indicating what users (generally) have to know about the function. This does not include HasCallStack. HasCallStack is already partially magical (and the rest is library internals). Maybe we should take that further, and remove HasCallStack from type signatures. Pardon my fake syntax: error :: forall {rep} (a :: TYPE rep). String -> a error @(_ :: class HasCallStack) msg = ... head :: [a] -> a head @(_ :: class HasCallStack) [] = error ... This has two downsides I see: 1. It's no longer so easy to tell whether a function takes a call stack. But that's kind of the point; we usually don't want to think about that. 2. It's no longer so obvious that undefined is a function. But ... we very rarely care that it is.
I feel like this brings up an idea I’ve been kicking around for a while and maybe have suggested In the past in the context of exceptions: We can have more info than just our vanilla type sigs in interface files. Eg you could track approximate “may throw ” sets. And one could conceive of either module pragmas/function pragmas or special built in combinators that surface / help us reason about stuff! One can go further ! You could imagine language modes that Eg surface totality into how expresssions are typed in a module. Or on the wacky end an impure strict language mode that converts all expressions into left to right eval order Anf in the io monad and makes all expressions essentially do notation for the io monad! The point I’m trying to illustrate and articulate by example is that while every flavor of reasoning can have a type theoretic embedding, that doesn’t mean everyone else has to see or work with those cosntraints! A slightly real example of this in ghc today is how we supresss levity polymorphism in types by default for users. So how can we cook up some tools that allow these sorts of information to be visible to those who want it and invisible to those who don’t? I sometimes wonder if, were we designing the ghc abi/calling convention today, would we have a register reserved for the analogue of the has call stack info? (I suppose the dwarf info and stack walking tools on ELF platforms is that to some extent. Just sadly not on all platforms in tier 1 :(. ) On Tue, Jun 8, 2021 at 2:29 PM David Feuer <david.feuer@gmail.com> wrote:
On Tue, Jun 8, 2021, 1:39 PM Richard Eisenberg <lists@richarde.dev> wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type).
Yes, this is quite awkward. We have here a tension:
1. The *operational* type, indicating the calling convention. This includes HasCallStack.
2. The "denotational" type (for want of a better term), indicating what users (generally) have to know about the function. This does not include HasCallStack.
HasCallStack is already partially magical (and the rest is library internals). Maybe we should take that further, and remove HasCallStack from type signatures. Pardon my fake syntax:
error :: forall {rep} (a :: TYPE rep). String -> a error @(_ :: class HasCallStack) msg = ...
head :: [a] -> a head @(_ :: class HasCallStack) [] = error ...
This has two downsides I see:
1. It's no longer so easy to tell whether a function takes a call stack. But that's kind of the point; we usually don't want to think about that. 2. It's no longer so obvious that undefined is a function. But ... we very rarely care that it is.
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
At this point I think it is interesting to see what our cousins have done to address the problem of invisible partiality. PureScript has the `Partial` typeclass¹. I suggest we ask their community how they feel about it, what has been their experience and if they could do it differently, what it would be. --- ¹ https://pursuit.purescript.org/packages/purescript-partial/3.0.0 Le 08/06/2021 à 19:36, Richard Eisenberg a écrit :
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial. * We have some room in how we relate IsPartial to HasCallStack. We could say that IsPartial is just a synonym for HasCallStack (e.g. with type IsPartial = HasCallStack). But perhaps better would be to somehow give users control over whether they want the HasCallStack mechanism to be able to solve IsPartial constraints. Maybe some users would prefer not to be able to satisfy IsPartial constraints immediately, but instead to require an acknowledgement in their code that they're doing something partial. For example:
partialityIsOK :: String -> (IsPartial => r) -> r elements xs = map (partialityIsOK "lists returned by `group` are always non-empty" head) (group xs)
The partialityIsOK function has a more involved type than I would like, but it's very usable in practice. Of course, such a thing only makes sense if IsPartial cannot automatically be satisfied. Getting this to work properly probably needs an extra language feature (maybe make IsPartial magically built-in?), but it might provide a declarative, yet operationally practical way forward here.
Richard
On Jun 6, 2021, at 12:49 PM, Dominic Steinitz <dominic@steinitz.org <mailto:dominic@steinitz.org>> wrote:
-1 for the reasons Henrik has listed
Dominic Steinitz dominic@steinitz.org <mailto:dominic@steinitz.org> http://idontgetoutmuch.org <http://idontgetoutmuch.org> Twitter: @idontgetoutmuch
On 5 Jun 2021, at 11:10, libraries-request@haskell.org <mailto:libraries-request@haskell.org> wrote:
Re: RFC: Add HasCallStack constraint to partial Data.List functions.
_______________________________________________ Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW: https://glitchbra.in RUN: BSD
+1, and I apologize for not reading the full discussion before suggesting the same solution. Ignore my other message please. On 2021-06-08 1:36 p.m., Richard Eisenberg wrote:
I've been very much of two minds in this debate: On the one hand, having these constraints is very practically useful. On the other, what we're doing here is very un-Haskellish, in that we're letting operational concerns leak into a declarative property (a function's type). The reason we're doing this is another un-Haskellish thing -- partiality -- but that ship has sailed.
So, may I propose a slightly different way forward?
Instead of adding a HasCallStack constraint on these functions, add an IsPartial constraint. For example:
head :: IsPartial => [a] -> a
This is slightly awkward, still, because IsPartial is a class-constraint-like-thing, but it has no parameter. But it has a few very nice properties: * IsPartial is declarative: it describes a property of the function without worrying about its operation. * If we think about the way constraints propagate, IsPartial has the right semantics: the caller of a partial function would itself become partial. * We have some room in how we relate IsPartial to HasCallStack. We could say that IsPartial is just a synonym for HasCallStack (e.g. with type IsPartial = HasCallStack). But perhaps better would be to somehow give users control over whether they want the HasCallStack mechanism to be able to solve IsPartial constraints. Maybe some users would prefer not to be able to satisfy IsPartial constraints immediately, but instead to require an acknowledgement in their code that they're doing something partial. For example:
partialityIsOK :: String -> (IsPartial => r) -> r elements xs = map (partialityIsOK "lists returned by `group` are always non-empty" head) (group xs)
The partialityIsOK function has a more involved type than I would like, but it's very usable in practice. Of course, such a thing only makes sense if IsPartial cannot automatically be satisfied. Getting this to work properly probably needs an extra language feature (maybe make IsPartial magically built-in?), but it might provide a declarative, yet operationally practical way forward here.
Richard
On Jun 6, 2021, at 12:49 PM, Dominic Steinitz <dominic@steinitz.org <mailto:dominic@steinitz.org>> wrote:
-1 for the reasons Henrik has listed
Dominic Steinitz dominic@steinitz.org <mailto:dominic@steinitz.org> http://idontgetoutmuch.org <http://idontgetoutmuch.org> Twitter: @idontgetoutmuch
On 5 Jun 2021, at 11:10, libraries-request@haskell.org <mailto:libraries-request@haskell.org> wrote:
Re: RFC: Add HasCallStack constraint to partial Data.List functions.
_______________________________________________ Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
participants (12)
-
Carter Schonwald -
David Feuer -
Dominic Steinitz -
Henrik Nilsson -
Hécate -
Julian Ospald -
Mario Blažević -
Oliver Charles -
Richard Eisenberg -
Simon Peyton Jones -
Taylor Fausak -
Tom Ellis