Scrub most partial functions from Prelude

[strake]

View

[cartazio]

I'm not sure how much support there actually is for this, even though folks always talk about it

On Friday, September 16, 2016, M Farkas-Dyck notifications@github.com wrote:

View

https://github.com/strake/rfcs/blob/08c53516d5230c811ac248e68550fd58d4cbabc3/texts/0000-scrub-partial-list-functions-from-prelude.rst

You can view, comment on, or merge this pull request online at:

https://github.com/haskell/rfcs/pull/8 Commit Summary

• Scrub most partial functions from Prelude

File Changes

• A texts/0000-scrub-partial-list-functions-from-prelude.rst https://github.com/haskell/rfcs/pull/8/files#diff-0 (93)

Patch Links:

• https://github.com/haskell/rfcs/pull/8.patch
• https://github.com/haskell/rfcs/pull/8.diff

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/8, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwiTjOlJku0tpCLl4y4pK-tIyIuhmks5qq2KqgaJpZM4J_fzl .

[simonmar]

This doesn't really achieve much, IMO. You can't eliminate all the ways to write bottom: there are pattern matching failures, division by zero, undefined methods, uninitialized record fields, error, undefined, array indexing, and of course non-termination. Removing a few partial functions just tends to push the partiality to the call site, making life harder for the programmer. Let's educate people and improve the documentation instead.

[jwiegley]

I agree with @simonmar; trying to enforce program correctness, when it comes both at a high cost (lots of breakage in existing code) and does not actually enforce correctness (you can still do broken things in lots of other ways), isn't worth the pain.

[hvr]

Alternative approach: Devise an opt-in scheme to annotate total/partial functions similar in spirit to how SafeHaskell provides the ability to annotate and infer "safety" of Haskell functions, but instead for partiality/totality.

[gbaz]

I may be mistaken here, but I thought the prime process was fundamentally about non-libraries changes, and that libraries changes remained in the hands of the library committee, at least for the time being?

(I should add that personally I've worked on code under the discipline of not importing any partial functions from the prelude, and I think it is good practice and that uniformly such functions should not be in by default, and that head should never be used when we have headNote instead, etc. The presence of so many famous head errors indicates that even if this doesn't get us close to 100% correctness, it just rules out a set of typically bad practices. But, again, I still suspect this is not the right venue for this discussion?)

[goldfirere]

I like @hvr's suggestion -- which is in scope. The language could provide a way to note that a function is partial and then warn accordingly. Of course, we'd need to implement this idea in GHC first.

[quchen]

Maybe this should be part of Haddock, not Haskell itself?

[gbaz]

Some interesting prior art now in PureScript with the Exhaustiveness checking (http://blog.functorial.com/posts/2016-01-31-PureScript-0.8.html) and the Partial typeclass (https://github.com/purescript/purescript/wiki/The-Partial-type-class).

[jwiegley]

@gbaz Their use of a Partial class seems quite nice, and a clearish way for people to upgrade code if such a construct were enabled in a legacy project.

[cartazio]

That sort of class constraint doesn't have the right opt in semantics.

Any info at the haddock layer generally is derived from Haskell source / ghc layer.

Zooming out : having some sort of robust lattice for possible exceptions and totality / partiality plus provenance of if it's inferred vs asserted vs proven etc has pretty rich / interesting design space. And can be tricky in the presence of ... stuff like higher order functions and or effects.

I think I have some design notes related to ways to adapt tech that's out there for trying to adapt these to ghc in a principled way. But either way this is one of those yaks that need to be evaluated in the Wild

On Thursday, September 22, 2016, John Wiegley notifications@github.com wrote:

@gbaz https://github.com/gbaz Their use of a Partial class seems quite nice, and a clearish way for people to upgrade code if such a construct were enabled in a legacy project.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/8#issuecomment-248970763, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwswFoRP7yJQnEdP6UDj_-XZWrgVQks5qsrpagaJpZM4J_fzl .

[gbaz]

@cartazio could you expand on "right opt-in semantics"? I think opt-out is fine here. If the compiler detects an incomplete pattern match, it adds the constraint. If you want to opt-out you use the unsafe function they provide (perhaps with a different name to keep "unsafe" meaning type-unsound and not diluting it). I agree this needs to be evaluated in the wild, etc and as per @goldfire "Of course, we'd need to implement this idea in GHC first." But it does seem intriguing, and it would be nice to see fleshed out why you think that this should be "more opt-in" than is. (Of course, an opt-in component could be to hide it behind a flag such as -XConstrainIncompleteMatches).

[cartazio]

I mean that discharging class constraints doesn't line up with any opt anything semantics. Or I'm not seeing how it does. I agree you could have pragmas and some bounds and assertions. I just don't see the semantics you propose lining up with forcing us to consider subtyping on arguments to higher order functions in a complicated way.

That is: termination tracking plus higher order code leads to some pretty intricate type theory. The approach in Agda 2.5 is neat , but not sure if the power weight ratio fits Haskell

On Friday, September 23, 2016, gbaz notifications@github.com wrote:

@cartazio https://github.com/cartazio could you expand on "right opt-in semantics"? I think opt-out is fine here. If the compiler detects an incomplete pattern match, it adds the constraint. If you want to opt-out you use the unsafe function they provide (perhaps with a different name to keep "unsafe" meaning type-unsound and not diluting it). I agree this needs to be evaluated in the wild, etc and as per @goldfire https://github.com/goldfire "Of course, we'd need to implement this idea in GHC first." But it does seem intriguing, and it would be nice to see fleshed out why you think that this should be "more opt-in" than is. (Of course, an opt-in component could be to hide it behind a flag such as -XConstrainIncompleteMatches).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/8#issuecomment-249203707, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwmO7R9ED11syTYPAEQwDyEwrM14eks5qs941gaJpZM4J_fzl .

[jwiegley]

@cartazio What does this have to do with "termination tracking"?

[cartazio]

Is the collatz function terminating? Or is it partial?

Or when we talk about partiality, do we specifically mean definitely terminates in bounded time or throws an exception?

If we mean exception tracking, and we specifically mean incomplete case matching that can't be ruled out because of application / data structure invariants , my point still stands about asking how should we think about it in the face of higher order function compositions.

On Saturday, September 24, 2016, John Wiegley notifications@github.com wrote:

@cartazio https://github.com/cartazio What does this have to do with "termination tracking"?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/8#issuecomment-249346543, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwtflfvJJDgBYKJ_Jo_zQnXPysujPks5qtLV4gaJpZM4J_fzl .

[cartazio]

(I may just be agreeing vigorously :) )

[jwiegley]

I thought (perhaps erroneously) that the proposal was simply to add "Partial =>" to the type signature of partial functions in the Prelude, not add heuristics for computing whether any function should magically acquire that constraint. If a user uses a partial function, that doesn't make their function also Partial; it is an error which they can resolve either by deciding to propagate partiality, or by using a function that accepts the danger and provides the constraint.

[cartazio]

The initial proposal was to just remove them. Unless I'm mixing stuff up.

How to surface / handle exposing / composing partiality info is not articulated by that, and is what the thread has shifted to discussing.

Perhaps I (or Someone else) should take the time to write up some ideas / theoughts that help articulate the design space.

My personal concern / worry is that the wrong approach makes writing higher order code that has partiality a bit more subtle.

On Sunday, September 25, 2016, John Wiegley notifications@github.com wrote:

I thought (perhaps erroneously) that the proposal was simply to add "Partial =>" to the type signature of partial functions in the Prelude, not add heuristics for computing whether any function should magically acquire that constraint. If a user uses a partial function, that doesn't make their function also Partial; it is an error which they can resolve either by deciding to propagate partiality, or by using a function that accepts the danger and provides the constraint.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/8#issuecomment-249435992, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwp7kqZkjGTglI4jiZ2t_mrR2qy3Vks5qtrbqgaJpZM4J_fzl .

[jwiegley]

Yes, that was the original proposal, which seemed a bit harsh to me. I prefer this other direction, where partiality is a type-error that can easily be opted out of on a case-by-case basis, in a way that makes use of the type system.

[llelf]

to add "Partial =>" to the type signature of partial functions in the Prelude

Even more: If we have some “standartized” Partial class, that would allow declaring even user-defined functions Partial (if wanted).

[quchen]

I’m not sure this Partial is a good idea yet. Suppose we change head to have type Partial => [a] -> a. How does this affect map head :: ???? Should this be partial as well, since it potentially contains bottoms?

• If we mark everything containing a partial function as partial, how do we un-mark functions like map head . group, which contain partial functions, but combine them in a total way?
• If we do not propagate the Partial, then I don’t see why we should have it in the first place, as it would not be much more than a comment.

[strake]

This is more controversial than i thought. Shall we close it? I would not protest.

[gbaz]

If we mark everything containing a partial function as partial, how do we un-mark functions like map head . group, which contain partial functions, but combine them in a total way?

The approach as given by the PS implementation would be to manually call a function unPartial or the like which discharges the constraint and could even potentially (via reflection [aka implicit configurations]) provide an error message to be given should the partial functions actually be tripped.

I do agree that this is a controversial discussion (but also an interesting one). As someone not on the committee but who has been paying attention to the discussions on running it, my impression is that this just means this ticket/discussion could drag on. As long as it doesn't distract from any other more pressing work, it seems to me interesting and with the potential to lead to some future implementation work, at which point it could get picked up again as a proper proposal. So it seems up to the committee in my mind to judge if they want to leave things in this state open, or only to keep the things open which they think have a chance at more rapid progress, or which exist more fully in existing haskell compilers...

[cartazio]

Let's close it but note that some good ideas have been discussed but any approach needs to be grounded in some experiences using them because of how subtle this stuff can get.

On Tuesday, September 27, 2016, M Farkas-Dyck notifications@github.com wrote:

This is more controversial than i thought. Shall we close it? I would not protest.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/8#issuecomment-249788780, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwspTpZQyReS_bgVqmA2_L-JiBpI5ks5quMdzgaJpZM4J_fzl .

[jwiegley]

I'd prefer not to close just yet, until some more exploration has been done. I haven't been feeling any controversy here, just the normal questions that should arise when attempting to break new ground.

[quchen]

I am also not against the Partial feature per se, but I’m not sure the (design of the) Report is the right place to try things like these out.

[jwiegley]

I see what you mean now; yes, I suppose this is not the place.

[cartazio]

Closing as "needs more experimentation and exploration" before it's mature enough for language standards discussion.