@partial metadata for partial/non-total function with a pure type signature

[Kleidukos]

Hello maintainers and contributors,

Following this merge request in base's documentation, and an interesting comment from Ben Gamari, I lay before you the possibility of having an additional metadata annotation:

@partial <optional message>

to indicate the fact that a function with a seemingly innocent type signature (such as maximum :: (Foldable t, Ord a) => t a -> a) might in fact raise a runtime exception.

There are of course some other things to sort out, notably at the UI/UX level.
Does haskell.org or any of the corporate sponsors have any people with this skillset that could be of any help?

I hope this will lead to some interesting advances in how we document our Haskell code. :)

cc @bgamari @cartazio

[bgamari]

The only thing that makes me nervous here is that it's somewhat of a lie. A function lacking @partial may very well diverge, even if its RHS appears to be total. Afterall, the function may use a function that is itself non-total.

[Kleidukos]

@bgamari This is indeed a valid concern. My opinion would be to be honest regarding the limitations of this metadata, with maybe some kind of tooltip on the metadata, that would explain that this does not equate a formal proof of totality and is user-defined (or something like that).

[cartazio]

I think it might be better to flip it around : rather than just saying it’s partial, it should be a “has failure modes”. Eg length and most other recursive / finite length assuming algorithms will fail in the sense of an infinite loop on a cyclic list ! May throw exception is one annotation May nonterminate on certain lazy / infinite structures is another. Maybe step zero is we start a document that tracks all the safety properties different functions in base require (what conditions for infinite loop, throwing an exception based on inputs/state etc). Then figure out what we may want from a documentation and or tooling support. I worry that unless we first write down all these and look at it holistically, we may miss an opportunity to do something cool with the whole big picture.

…

On Sun, Mar 22, 2020 at 5:24 AM Hécate ***@***.***> wrote: @bgamari <https://github.com/bgamari> This is indeed a valid concern. My opinion would be to be honest regarding the limitations of this metadata, with maybe some kind of tooltip on the metadata, that would explain that this does not equate a formal proof of totality and is user-defined (or something like that). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1139 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQTVRFQU54VMKMJ5J2DRIXKLXANCNFSM4LQ4AKFA> .

[Kleidukos]

Thank you Carter for the insight!

On my side, I suggest we first go with marking functions for which a (direct) code path to undefined/error/errorWithoutStacktrace/throw is possible.
This excludes functions calling such functions because we wouldn't see the end of it, but it can be a good start if we want to lead to way to a glorious future where we have a proper termination checker in GHC.
And better docs. That's why we're here. ;)

[TixieSalander]

Hello, @Kleidukos asked me to work on the annotation's UI integration. I'll take look on how I can help.

[Kleidukos]

Tixie is a wonderful designer and I have had the chance of working with her in the past.
I am sure she will be able to fill some gap in our skill set. :)

[Kleidukos]

For reference, here is an example of a function that is partial (with its current warning), and has an example section:

[cartazio]

i'd really like it to be collapsable :)

[cartazio]

so

Warning Sigil Partiality: then the collapsed info which explain , or something along those lines, we can compare several flavors and figure it out

[cartazio]

restating part of a discussion on irc, i was suggesting "@partiality", or something like that, be the grammatical analogue of

[TixieSalander]

Here the result of a first iteration designing warning message in the documentation:

• I emphasized the message with a light colored box + an icon
• I've choose a standard color for a warning message but in pastel shades to harmonize nicely
• High contrast between text and background (WCAG AAA compliant)

[chessai]

note that there is a typo in that image, should be 'Exception', not 'Excepetion'.

Additionally, I think 'has failure modes' is a step in the right direction.

[cartazio]

i do think the WARNING SIGIL Partiality piece should then have the text under it
a la examples toggle

[Kleidukos]

@cartazio So something like

⚠️ Partiality

This function is partial and may raise a runtime exception…

[cartazio]

Yes!
With the body being the documentation about side conditions for failure / correctness and or examples thereof

[hasufell]

I feel partial is too specific. What we want to express is failure. There are 3 types of failure (at least):

• failure that is part of the result type (Either String ())
• failure that is part of the exception system (IOException hidden behind IO, but also MonadThrow/MonadCatch, etc. potentially)
• failure that raises error/bottom, so is forced depending on evaluation (partiality is part of this)

Now, with this proposal, we have a specialized syntax for a tiny subcase of the entire problem. With things like MonadThrow, the line between runtime exception and result type exception get blurry, because it depends on the caller what it will be. As such, I feel it would be too much effort trying to give specialized syntax for all these different cases.

Instead there should be a sufficiently simple way to mark failures:

@fails `Either.Left` if file is empty
@fails `IOException` if file does not exist
@fails due to partial pattern matching if filepath is empty
@fails `throwM InternalError` if file is a directory

This allows to express failures in a sufficiently powerful way. The downside is that there's no special syntax for the different cases. But I'm not sure if that's necessary (and with effects systems it might become even more of a problem).

When there's a block of @fails, haddock could group them and convert it to an item list.

[Kleidukos]

Hi @hasufell, thanks for chiming in. :)

I feel partial is too specific. What we want to express is failure. There are 3 types of failure (at least):

In our specific case, we wish to express untyped runtime errors, in the same vein as GHC's !2930.

So by that definition, I don't think we should go as far as to mark Either types to be "partial". After all, these function do map every member of their domains to the codomain specified by the type signatures, so there's nothing to worry about, no hidden traps that would be only discovered by an unhappy usage of these functions.

---

failure that is part of the exception system (IOException hidden behind IO, but also MonadThrow/MonadCatch, etc. potentially)

Now that is an interesting middle line that raises some questions, which are quite legitimate.
Maybe this warrants some more discussions, maybe it's self-evident, I don't have enough experience with those to have a fixed point of view on the matter, hence my calls to discussion.

---

However, I would like it to be known that I do not wish to operate in a mode similar to GHC proposals where something needs to be debated for 30 days and 30 nights before being set in stone forever, and be passed as tradition to our children.
If MonadThrow & co. are not included in the guidelines for @fail/@partiality following this discussion, it's alright, and they can be added later, when we have some more experience using this metadata marker!

[hasufell]

In our specific case, we wish to express untyped runtime errors, in the same vein as GHC's !2930.

Well, as I said. untyped runtime errors can be expressed with @fails as well, without pinning the use case too much.

So by that definition, I don't think we should go as far as to mark Either types to be "partial".

No, this is an assumption. A function that returns Either/Maybe can still be perfectly partial.

---

Most haskell code I've worked with is a wild combination of those 3 cases. E.g.

foo :: MonadIO m => [String] -> ExceptT String m Int
foo xs = do
 let bar = head xs                 -- partial
 contents <- liftIO $ readFile bar -- IO exception
 parsedContents <- parse contents  -- may short-circuit ExceptT
 ...

[Kleidukos]

Okay I think I've misunderstood you, I thought you meant that because an function returned an Either it should be marked with @fails. My bad.

[hasufell]

Okay I think I've misunderstood you, I thought you meant that because an function returned an Either it should be marked with @fails. My bad.

It can. It's up to the discretion of the maintainer. If the type is unexpressive (e.g. String) and there are multiple different failure cases, this might be a good idea.

[cartazio]

fails is the wrong grammar i think. or maybe i need to reread julians remarks :)

[cartazio]

failures are partiality. nontermination, nonlocal control, deadlocks, they are all "stuck" states per se.

I guess its useful to distinguish things that are explicit failures this code throws an exception on bad inputs vs this will trigger sigbus or this will deadlock if you write bad code. but at least in some perspectives, those are all the same.

[cartazio]

Hrmm. I guess it’s def true that we should think of this all as what it really is: a markup tool for software authors.

…

On Sun, Mar 29, 2020 at 12:02 PM Julian Ospald ***@***.***> wrote: Okay I think I've misunderstood you, I thought you meant that because an function returned an Either it should be marked with @fails <https://github.com/fails>. My bad. It can. It's up to the discretion of the maintainer. If the type is unexpressive (e.g. String) and there are multiple different failure cases, this might be a good idea. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1139 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABBQUQCYFEMMDUKVOW4U3RJ5WINANCNFSM4LQ4AKFA> .

[kindaro]

Hello! What is the situation with @partial and other metadata right now? I want to use @partial and a few other fields to make vector better — see haskell/vector#479. Is there someone in the hoogle team I can work on this together with?

[Kleidukos]

@kindaro Hi, we're going to migrate this ticket to GitLab in the following week, and I'll make public announcements regarding the roadmap; as well as public consultations. Thank you for your interest, I am still thinking about it. Perhaps the recent warnings on List.head/tail can be a source of inspiration.

[kindaro]

So what is the right way for me to go on? What actions should I take?

I have just finished reading haskell/core-libraries-committee#87 — this seems to be what you refer to as «recent warnings on List.head/tail». Is there something else you would offer me to look at?

I did not grasp what you mean by «public announcements regarding the roadmap» and «public consultations». Would you have a moment to clarify this?

[Kleidukos]

@kindaro Nothing special, just advertise on Discourse that the development of Haddock will be more active, bring transparency regarding its roadmap, be more receptive to ideas and contributions.