Add the empty function never : Never -> a

[andersk]

There seems to be no way to pattern-match on the empty type Never; this adds a canonical way to do so. An example where this is needed is Task.perform never : (a -> msg) -> Task Never a -> Cmd msg.

(I suppose that given a polymorphic Task never a, one could use something like Task.perform identity : (a -> msg) -> Task a a -> Cmd msg instead. But that’s confusing.)

This is a more general solution to #578, which would now be solved by Cmd.map never : Cmd Never -> Cmd msg. It’s safer than making the user write a Debug.crash call because the type system prevents it from being accidentally put in a place where it might ever receive a value.

(I previously called this function absurd, after Haskell’s Data.Void.absurd.)

[jvoigtlaender]

Another possible use case occurred in this thread.

[jvoigtlaender]

Elaborating on the use case from the mentioned thread:

One may model the case that one has some html that is static (in the sense it never gives rise to an event) by using type Html Never. Then, when including that piece of html in a view, one will typically have to transform it into something of type Html Msg for an application specific Msg type. The way to do so is to use Html.map with a function of type Never -> Msg. There may not always (depending on the application specific Msg type) be a very good choice for such a function. But the function from this pull request would always fit the bill. Instead of absurd, I'd probably call it never.

[andersk]

never was also a name I considered, so, sure. Changed.

[jvoigtlaender]

You would also have to add the function name to a @docs comment, or Elm will complain at some point (compiler or package uploader).

[andersk]

Added to @docs; thanks.

[rtfeldman]

Historically when Evan has asked for a motivating example, he's meant something of the form "I was building something useful, and hit this roadblock." He's also generally asked questions about existing solutions and attempted workarounds; adding a new capability has been largely treated as a last resort, only after all other options have been exhausted.

Does that clarify what he's looking for?

[jvoigtlaender]

@andersk, in line with the directions under https://github.com/elm-lang/core/blob/master/CONTRIBUTING.md#adding-new-functions, I propose you move this pull request to https://github.com/elm-community/basics-extra (which I just created, to welcome this contribution as the first one in the package).

[andersk]

@rtfeldman I’m happy to expand on my particular use case, but I don’t think there are additional interesting details here; this is a generic problem with Never that has a generic solution.

I am writing a full screen application that needs to know the window size. So I add Window.resizes to my subscriptions, and I get that information as soon as the user manually resizes the window. But I also need to know it on startup, so I spawn a Window.size task on startup.

import Html
import Html.App as Html
import Task
import Window

type Msg = Resize Window.Size

type alias Model = { size : Window.Size }

main : Program Never
main =
  Html.program
  { init =
      ( { size = Window.Size 0 0 }, Task.perform ??? Resize Window.size )
  , update =
      \msg model ->
      case msg of
        Resize size -> ( { size = size }, Cmd.none )
  , view =
      \model -> Html.text (toString model.size)
  , subscriptions =
      \model -> Window.resizes Resize
  }

Window.size is a task that cannot return an error, so what do I put in for ???? Elm expects a function that takes a nonexistent error and returns a Msg. Because of the way the types are set up (Window.size : Task x size), it happens that I can put the identity function identity here, but I would not expect a user who isn’t already familiar with type theory to understand that. It would be much more natural and self-documenting to use a function that explicitly presupposes at the type level that an error can never happen.

If you strip away all the details, this problem is equivalent to that of writing a function Either Never a -> a. Surely it’s obvious that one should be able to write such a function.

The fact that a destructor is not provided for the standard empty type Never and cannot be written without Debug.crash is a shortcoming of Never. It would be like providing a pair type with no fst and snd functions and no way to pattern match the values out. The only reason Elm has been able to get away without it so far is that Never is only ever “destructed” in native code.

[andersk]

@jvoigtlaender Thanks, but this pull request cannot be moved as written, because only the Never type is exported from Basics, not the Never constructor. It could be reimplemented using Debug.crash, and I suppose that would still be better than making each user write a Debug.crash call, but it’s still part of what I’m trying to avoid.

I do not propose exporting the Never constructor, both because it’s more confusing than the never function, and because if Elm were to add support for types with zero constructors (like Haskell added in Haskell 2010), it would be natural to reimplement Never as such a type:

type Never  -- no constructors

never : Never -> a
never n = case n of
  -- no cases

Among the available options:

• add never to Basics;
• export the Never constructor from basics, preventing its implementation from being improved in the future;
• add a Debug.crash-based implementation of never to basics-extra;
• add a second, incompatible Never type to basics-extras, whose constructor can be used in an implementation of never;
• add zero constructor data types to the language;

I still think the first is cleanest. What do you think?

[jvoigtlaender]

My proposal (see also a recent exchange on the mailing list) is to add the function to basics-extra with this definition:

never n = never n

[andersk]

Submitted as elm-community/basics-extra#1. Keeping this issue open to track the request to move never to core.

[rtfeldman]

Window.size is a task that cannot return an error, so what do I put in for ???? Elm expects a function that takes a nonexistent error and returns a Msg.

We'd discussed having a Task.performAndIgnore : Task x a -> (a -> msg) -> Cmd msg in the past, and @evancz was looking for motivating use cases. This seems to be another one to add to the list!

That said, without Task.performAndIgnore existing, I think telling people "use identity for this" seems like a better fallback than adding something that relies on Debug.crash (or a known compiler bug that could be fixed anytime and make it no longer compile) to basics-extra and encouraging people to use that.

I agree that people would not intuitively realize identity works here, but why not just tell them that it works instead of pointing them to a new thing?

[andersk]

@rtfeldman performAndIgnore is not the right answer. I don’t want to ignore errors—I want to assert that errors are impossible, and have the compiler check this for me. If the upstream API were to change so that the task is now allowed to return errors, I would want to hear about that so I can handle the errors appropriately. That’s the entire point of having a statically typed language, right?

Besides, why should a hypothetical solution that only works with Task.perform be preferred over a clean, generic, orthogonal function that should obviously exist and that would allow Never to be dealt with in a uniform way across all APIs?

[rtfeldman]

I don’t want to ignore errors—I want to assert that errors are impossible, and have the compiler check this for me.

Ah, good point!

Let me try to summarize the discussion. Here are three options, and their drawbacks:

Option 1: performAndIgnore

Task.performAndIgnore Resize Window.size

Drawback:

If the upstream API were to change so that the task is now allowed to return errors, I would want to hear about that so I can handle the errors appropriately.

Option 2: Status Quo, use identity

Task.perform identity Resize Window.size

Drawback:

I would not expect a user who isn’t already familiar with type theory to understand that. It would be much more natural and self-documenting to use a function that explicitly presupposes at the type level that an error can never happen.

Option 3: never

Task.perform never Resize Window.size

Drawback:
Now instead of teaching people how/why identity works in Option 2, we're expanding the API to include a new feature, and teaching people this instead.

Does this seem like a fair summary of things, or am I missing something?

[andersk]

@rtfeldman Sure.

I would add that if Task.perform identity became idiomatic, someone might mistakenly use it on a Task where the error and result types are nonempty but happen to be the same—say Task String String, which either returns a String error message or a String result—leading to errors being misinterpreted as results. Task.perform never prevents this mistake. This is perhaps a minor point because Elm error types tend to be custom ADTs, but still it points to an opportunity to make the types more expressive while improving readability.

[jvoigtlaender]

Hopefully not distracting from the discussion here, but Richard, when you say

or a known compiler bug that could be fixed anytime and make it no longer compile

you mean the elm/compiler#873 discussed over there, or something else? The elm/compiler#873 doesn't apply, I think.

[rtfeldman]

@jvoigtlaender That was what I meant, but 👍 if you think it doesn't apply. 😄

@andersk Fair point about the potential for misusing identity in the Task String String case.

It occurs to me that there's a fourth option:

Option 4: Task.performCertainly

performCertainly : (a -> msg) -> Task Never a -> Cmd msg
performCertainly =
    Task.perform mustBeNever


mustBeNever : Never -> x
mustBeNever _ =
    Debug.crash "The type-checker should have prevented this from being run!"

Upside: more direct; instead of learning never and then that never is to be used with Task.perform, you just use Task.performCertainly.

Downside: less composable—although we don't have a motivating use case for composing never, do we?

[jvoigtlaender]

@rtfeldman, that's exactly the thing from this proposal on the mailing list, right?

Yes, this could be put into Task or Task.Extra, and users of it would not need to be aware of never. But as has already been pointed out, there are other places where one would want to use never for similar reasons as in the Task.perform case. In particular, one sometimes might want to use it as argument to Html.map (if one has typed a thing as Html Never to express that it definitely is not carrying any event handlers, put then wants to put it into some other view), and similarly as argument to Cmd.map.

Of course, one can make special versions of Html.map and Cmd.map, just as one can make special version Task.performCertainly of Task.perform.

[andersk]

Even if for some reason you think we should duplicate all functions like Task.perform, Html.map, Cmd.map to work with Never, consider that someone else might want to write a new API we haven’t thought of yet that should also work with Never—and even if you think they should duplicate their functions as well, the implementation of those duplicated functions will necessarily involve Debug.crash, an intentional infinite loop, or a call to never.

[rtfeldman]

if one has typed a thing as Html Never to express that it definitely is not carrying any event handlers, put then wants to put it into some other view

Why is this better than Html a? That also guarantees that it definitely is not carrying any event handlers, but you don't need to Html.map it.

consider that someone else might want to write a new API we haven’t thought of yet that should also work with Never

The first two points on Elm's official API design guidelines are:

1. Design for a concrete use case
2. Avoid gratuitous abstraction

If it seems like I'm pushing back so hard on abstracting this without a specific use case, it's because that is explicitly and unequivocally the Elm way to approach API design. :)

[jvoigtlaender]

@rtfeldman:

Why is this better than Html a?

In my very first comment above, I linked to a thread on the mailing list. There, someone wanted to express that their model type carries static-only html. How to do that? With Html Never:

type alias Model =
  { staticHtml : Html Never
  , someOtherFields : ... }

With your suggestion:

type alias Model a =
  { staticHtml : Html a
  , someOtherFields : ... }

Spot the difference? It's suddenly necessary to parametrize the Model type by a, for no other purpose than to be able to express elsewhere that the contained Html stuff is effect-free. That will potentially affect a lot of type signatures.

Moreover, your solution is no solution at all if I want to express that some function in my component accepts only effect-free Html stuff. Say I'm writing a component that expects to have subcomponents and it really wants to ensure that when it assembles its own view from the views of the subcomponents whatever it gets from the subcomponents is effects-free Html. How do you type a function that you want to be guaranteed to always get only effects-free Html as input?

Hint: The following is not the solution.

function : Html a -> Whatever

To that function, the caller can pass arbitrarily effectful Html.

But the following is a solution.

function : Html Never -> Whatever

Nobody can pass an Html ConcreteMessageType to this.

[andersk]

@rtfeldman I am not asking for a new abstraction. I’m simply asking that the existing Never abstraction be completed with its destructor function, so that it can be used for its originally intended purpose. At least three concrete use cases have been provided. Even if you take the position that there should be three special-case APIs for them and that no possible future APIs (standard or custom) should be taken into consideration, a destructor of Never remains a crucial part of the implementation of those three special-case APIs. (And I doubt such a position is what the author of the design guidelines had in mind.)

If Elm had rank n types (elm/compiler#1039), one could replace Html Never with the isomorphic type (∀ a. Html a) and Html Never -> Whatever with (∀ a. Html a) -> Whatever. Or in fact, one could replace Never with (∀ a. a). I’m sure you will agree, though, that adding rank n types to the language just to compensate for the absence of a bog standard empty type destructor function in the library would be the pinnacle of gratuitous abstraction.

(Additionally, my previous point about using identity still applies to that plan, unless a never : (∀ a. a) -> a is provided.)

[rtfeldman]

Great points all around! I'm sold on a never function being the right approach. Thank you for being patient with me. 😸

One final note:

I’m simply asking that the existing Never abstraction be completed with its destructor function, so that it can be used for its originally intended purpose.

Another recurring theme of Evan's is "don't block on me." Since the never a = never a implementation works fine for now, and even if a future compiler change broke it, changing to the destructure version would be trivial...all of which means this PR will most likely be extremely low on the priority list.

Personally I would recommend using never a = never a in https://github.com/elm-lang/core/pull/593/files, since that does not require any core changes!

Here's a revised summary:

Motivation

There are two problematic use cases that currently have no good solution:

Html.program
  { init =
      ( { size = Window.Size 0 0 }, Task.perform _____ Resize Window.size )

What goes in the blank? Window.size can never fail, but there is no way to tell Task.perform that.

The other problematic use case is this:

type alias Model =
  { staticHtml : Html Never
  , someOtherFields : ... }

You can write this, but you can never use staticHtml with Html.map because you have nothing to pass to Html.map.

This comes up in reusable components. For a concrete example of this, see elm-html-widgets.

Solution

Introduce a function never : Never -> a, which type-checks but which can never be called.

Html.program
  { init =
      ( { size = Window.Size 0 0 }, Task.perform _____ Resize Window.size )

Complete working example:

import Html exposing (..)
import Html.App
import Html.Events exposing (..)

main =
    view model

type alias Model =
    { staticHtml : Html Never }

type Msg = NoOp

model : Model
model =
    { staticHtml = i [] [ text "Hello, World!" ] }


view : Model -> Html Msg
view model =
    button [ onClick NoOp ]
        [ Html.App.map never model.staticHtml ]

never : Never -> a
never a = never a

Unsatisfactory Alternatives

You can use Html a instead of Html Never in many cases, but it is worse than Html Never in two ways. First, it does not let you write a reusable view function that accepts only "non-interactive" Html - in other words, Html Never. Second, it means your type alias now needs a type variable:

type alias Model a =
  { staticHtml : Html a
  , someOtherFields : ... }

This in turn means that every alias using this one will also need a type variable, which is annoying and can potentially impact a ton of code. Html Never does not have this problem.

There are several options that would address the "Window.dimensions on init" case, but they all have drawbacks that never does not.

performAndIgnore

Task.performAndIgnore Resize Window.size

Drawback:

If the upstream API were to change so that the task is now allowed to return errors, I would want to hear about that so I can handle the errors appropriately.

identity

Task.perform identity Resize Window.size

Drawback:

I would not expect a user who isn’t already familiar with type theory to understand that. It would be much more natural and self-documenting to use a function that explicitly presupposes at the type level that an error can never happen.

identity also doesn't suffice for the Html Never case.

Task.performCertainly

performCertainly : (a -> msg) -> Task Never a -> Cmd msg
performCertainly =
    Task.perform mustBeNever


mustBeNever : Never -> x
mustBeNever _ =
    Debug.crash "The type-checker should have prevented this from being run!"

Downside: now you have to learn performCertainly, Html.mapCertainly, etc, instead of learning never once and using it in several places.

[andersk]

Personally I would recommend using never a = never a in https://github.com/elm-lang/core/pull/593/files, since that does not require any core changes!

I’m not sure what you mean. This pull request is a core change, and it works as written; it does not require any changes other than itself.

[rtfeldman]

Gah, wrong link! I meant https://github.com/elm-community/basics-extra/pull/1/files

...which I now see uses it, and has the other one as a comment. Never mind. 😄

[andersk]

That one already uses never n = never n, because it seems like the least bad option available outside of core. However, it has the disadvantage that if someone who wants to avoid the dependency on the extra library just for one function decides to copy the definition without copying the corresponding type signature, they end up with the incredibly unsafe inferred type never : a -> b.

[jvoigtlaender]

This exists now: http://package.elm-lang.org/packages/elm-community/basics-extra/latest/Basics-Extra#never.

Next, should performCertainly : (a -> msg) -> Task Never a -> Cmd msg be added to http://package.elm-lang.org/packages/NoRedInk/elm-task-extra?

[jvoigtlaender]

For the Html.map never case, I've made a pull request here: elm-community/html-extra#6.

[jvoigtlaender]

@rtfeldman, is the NoRedInk/elm-task-extra repository welcoming of an addition like the Task.performCertainly discussed above?

(That repository doesn't have GitHub issues enabled, hence I'm asking here. I could of course simply make a PR against that repository, but don't know whether it's open for additions. Also, it's not yet updated to 0.16, so maybe it's actually on road to deprecation. Should a new task-extra repository be created at elm-community?)

[rtfeldman]

@jvoigtlaender happy to accept a PR for that! Please @ me so I see it. 😄

[jvoigtlaender]

So there are now three "hidden" uses of never in specialized APIs:

• http://package.elm-lang.org/packages/elm-community/html-extra/2.0.0/Html-Extra#static
• http://package.elm-lang.org/packages/elm-community/svg-extra/1.0.0/Svg-Extra#static
• http://package.elm-lang.org/packages/NoRedInk/elm-task-extra/2.0.0/Task-Extra#performFailproof

each with an example application in their documentation.

@andersk, you originally mentioned that one might want to use the function in Cmd.map never. Do you have a concrete example for that in mind? What function name for this specialized function of type Cmd Never -> Cmd msg would make sense, and in which package could it usefully live?

[andersk]

I imagine its use case would be similar to Html.map never. You have a subcomponent that happens to have an empty message type, with functions like

init : Flags -> (Model, Cmd Never)
update : Never -> Model -> (Model, Cmd Never)
subscriptions : Model -> Sub Never
view : Model -> Html Never

and you want to compose it into a larger component with a nonempty message type. Perhaps you could just throw away its Cmd Never and Sub Never values—but if you want to have the compiler check that the subcomponent message type is really uninhabited before throwing them away, you’d want to do it with Cmd.map never and Sub.map never.

There may also be legitimate Cmds that have side effects but never return. The ones in the (not-yet-published?) Navigation module are good examples.

However, I remain skeptical of the premise that any uses of never we can imagine should be wrapped into specialized APIs and hidden away. The advantage of creating specialized functions for Cmd.map never and Sub.map never seems especially unclear in this case over just writing Cmd.map never and Sub.map never inline.

[andersk]

Hmm. I just noticed that the Never type is not actually as uninhabited as it purports to be: the compiler magically provides a flags value of type Never to a program of type Program Never (elm/compiler#1398). Everything currently marked Program Never really ought to be marked Program () instead.

[jvoigtlaender]

You have a subcomponent that happens to have an empty message type

I don't think that makes sense. It would be impossible to ever call the function update : Never -> ..., so there would never by any change to the model, so the "subcomponent" would essentially be a static piece of html, artificially expressed as a pair of a fixed Model value and a function Model -> Html Never.

There may also be legitimate Cmds that have side effects but never return.

That reminds me of https://github.com/evancz/elm-effects/issues/28. In the 0.17 world, that would be a function performSilently : Task x () -> Cmd x. But whether obtained from such a performSilently or from one of the navigation API functions, I wonder whether one would indeed ever want an explicit Cmd Never. Wouldn't one here indeed leave those Cmds be and remain fully polymorphic in the message type?

So I am now actually skeptical one would ever have a use for the Cmd Never type. I am pretty convinced that Sub Never is nonsensical.

None of that means I would not also be happy to have never rather than "just" the specialized APIs hiding it away. But nevertheless I consider it a good idea to have those specializations expressed and available explicitly somewhere (like now in the three *-extra packages).

About your last comment, regarding Program Never, I fully share your concerns. But that discussion is probably best left to the other issue you opened.

[andersk]

Sure, such a static subcomponent scenario seems somewhat strained in solitude.

(One could imagine writing a combinator that takes a component as an argument and is polymorphic in the message type, and then wanting to instantiate it with a static subcomponent. But I agree that this particular train of thought involves a lot of speculation and isn’t likely to justify a specialized API for Cmd Never on its own. The general never function is sufficient.)

[evancz]

Tracking in #322. Very easy to add, so makes sense to make the decision before writing the code.