Is there a legitimate reason for `never`

[ChristophP]

The docs of the Basics module https://package.elm-lang.org/packages/elm/core/latest/Basics#never say that never can be useful together to use Html that shouldn’t produce any message together with one that does using

Html.map never someStaticHtml

But I found that instead of Html Never one can just use Html msg as a type for the static Html which is perfectly fine when no Event handlers are used.

Then the following simplification is possible

someStaticHtml : Html Never
someStaticHtml = ...

someOtherStaticHtml : Html msg
someOtherStaticHtml = ...

Html.map never someStaticHtml
-- equivalent to
Html.map identity someOtherStaticHtml
-- equivalent to
someOtherStaticHtml

So my question is, is there any benefit to using never anywhere ever?

[pdamoc]

@ChristophP

But I found that instead of Html Never one can just use Html msg as a type for the static

msg includes Never. The idea of using Never is to enforce static html.

This might be easier to understand if you think about a complex view:

complexView someParameter =

If you want to enforce that this complexView does not allow generation of messages, you need to type it as

complexView : Html Never ->  Html Never

If you use Html msg for this function, anything goes because the argument given to the function will control the ability of the function to emit messages.

[MartinS]

Another use case for Never is with phantom types.

type Point coordinateSystem = Point Float Float

type WorldCoordinate = WorldCoordinate Never

type ScreenCoordinate = ScreenCoordinate Never

playerStartPos : Point WorldCoordinate
playerStartPos = Point 2 3

healthBarPos : Point ScreenCoordinate
healthBarPos = Point 200 10

Here I’ve defined Point that uses a type parameter to make sure I don’t mix up different coordinate systems. I don’t actually want to create an instance of these coordinate systems though, they are just being used as phantom types. So to prevent accidentally creating them I add Never to their constructor.

[Latty]

The standard library has a good example of where this is useful, in Task.perform.

Normally, you would use Task.attempt, as tasks can fail, but if we have a Task Never a, we know the task can’t possibly fail, so we can do perform instead of attempt and not have to worry about handling errors.

[pd-andy]

Adding the Never to prevent accidentally creating instances of those types is a neat trick I haven’t seen before, I like that!

[brian]

Another use I found neat: the div function in tesk9/accessible-html requires that the attributes be Attribute Never. This is fine in the normal case since style, id, etc are all Attribute msg so they will pass the type check, but you can’t add any interactive stuff since it would require constructing a value of Never! This means that you can’t put a click handler on a div, for example, which someone using a screen reader would have no way of detecting.

[jfmengels]

I feel like there is worth expliciting that where in the signature you find the type variable or Never is important, and gives you different results.

You are right that html : String -> Html msg and html : String -> Html Never give you the same guarantee that the function will return any message. Specifically, this guarantee happens every time the Html is used with (lowercase) type variable that is only present once in the signature, and that the Html is the return value. If you find msg once more in the signature, like in html : msg -> Html msg you lose that guarantee.

Never comes in handy when you want the arguments of a function to be static (in the case of Html), so for instance html : Html Never -> Html msg. If you had done html : Html msg -> Html msg, you would not have that guarantee at all. I second the case @brian mentioned where the signature of tesk9/accessible-html's div function is List (Attribute Never) -> List (Html msg) -> Html msg. If it was List (Attribute msg) -> List (Html msg) -> Html msg, the guarantee that the div itself doesn’t trigger a message would be lost.

[Philipp_Krueger]

There are great replies in this thread already.

Two more data points:

1. reduing the amount of type parameters in type definitions

I guess we all understand that something : Html msg represents something that doesn’t generate messages at all. If you want to have a datatype that stores such a value, you’d have to add a type variable, e.g.:

type alias HtmlWithContent msg =
    { content : String
    , html : Html msg
    }

Then something : HtmlWithContent msg is something that doesn’t produce messages.

Sometimes lots of type variables are tedious, though. So you can do the following:

type alias HtmlWithContent =
     { content : String
     , html : Html Never
}

You save yourself one type variable, AND HtmlWithContent has this guaruntee now by itself!
(Btw, you can create type alias EventlessHtml = Html Never and always use EventlessHtml without any type variables! Neat, I think)

In a similar way, you could create something like this:

type alias Icons =
    { plus : Svg Never
    , expand : Svg Never
    , close : Svg Never
    , ...
    }

(Not that this type would be particularly useful. But notice, that adding one msg type parameter here would tie all of the svg types together. Here we keep the freedom of choosing the msg type later via Svg.map never.)

2. making some constructors in custom types impossible

This is kind of similar to Task Never a. Any custom type that has multiple cases, let’s take Result for a first example:

type Result error ok
    = Ok ok
    | Err error

Result Never a will always be Ok _, you can construct a function Result Never a -> a, but this is left as an exercise to the reader

This will work for any custom type, which can be useful in some cases for ASTs, for example.

[Philipp_Krueger]

Oh and something else: I like to introduce people to the idea of forall binding your type variables.

If you define a function in Elm you should imagine, that all your type variables are actually bound by a forall, so:

something : Html msg
-- is 'actually'
something : forall msg . Html msg

(This syntax is for example valid in haskell with an extension, or valid in purescript.)

Imagine this forall like something that allows you to choose what msg should be at call sites.

In this way, Html msg does not mean, that this Html doesn’t produce messages, for example here:

something : msg -> Html msg
something message = Html.button [ Events.onClick message ] [ Html.text "click me" ]

But forall msg . Html msg captures this idea of ’msg is supposed to be anything’, making this truly static html.

In Elm, Never, from a design perspective, is the same as the type forall a . a (Choose anything, it can be anything).
You can see that this is true by looking at the never function:

never : Never -> a
-- is 'actually'
never : forall a . Never -> a
-- is the same as
never : Never -> forall a . a

Also, forall a . Html a is the same as Html (forall a . a), becuase Html is a functor (has a valid map) function.

Enough type talk by me for today. Hope this was at least in some way enlightening

[ChristophP]

Hi everyone, those where all great answers. Thanks for all the theory and examples. Makes more sense to me know where the difference is between Html msg and Html Never.
Also the trick for preventing instanciation of a type is pretty neat

[openorclose]

I’ve tried to create a function Result Never a -> a, but only managed to do it using the naive Debug.todo method:

f : Result Never a -> a
f result =
  case result of
    Ok ok -> ok
    Err _ -> Debug.todo ""

Any hints on another way to create this?

[Philipp_Krueger]

Some hints:

• Take a look at the never function.
• Look where you could get hold of a Never value.

Hope this helps

[openorclose]

I got it!

Thanks for the hints!

[rupert]

@Philipp_Krueger

Oh and something else: I like to introduce people to the idea of forall binding your type variables.

Enlightening; I enjoyed that.

You’ve got forall, can you think of a way of mapping thereexists into the Elm type system? Or is it simply not possible, or only possible with limitations?

[Philipp_Krueger]

I know of a concept called “Existential types”, but I don’t fully understand it and I think I’ve read that it is only an ergonomic improvement over modeling the same thing with foralls.

[joelq]

I had a real use-case for the never function in an application the other day. This was all a bit complicated so jump to the bottom of the post if you just want to see the code that uses never. Otherwise, here’s some buildup on how I got to the point of using never

Generic pages

I wanted to write some generic layout functions that could render any page in my application. In addition to chrome and navigation, the layout would also handle displaying notifications and modal content.

The state of each page was modeled using dramatically varying types. In addition, pages could define modals that only existed on that page, but I wanted them to be displayed in the layout just like the other modals. To handle this situation, I created a type that looked like this:

type alias Page content modal =
    { notificationQueue : NotificationQueue
    , modal : Modal modal
    , content : content
    , -- more shared fields
    }

type Modal local
    = Global GlobalModal
    | LocalModal local
    | ModalClosed

Specific pages

These generic types allowed me to vary all the page-specific stuff. For example I might have something like:

initialModel : Page LocalContent LocalModal
initialModel =
  -- build up a `Page` record

type alias LocalContent = { field1 : String, field2 : Int, ... }
type LocalModal = Modal1 | Modal2

Layout

Finally I created a function that could render any Page in a layout. Two important things it needs to know are:

1. How do you render your page-specific content?
2. How do you render your page-specific modal content?

viewPage :
    { viewContent : content -> List (Html a)
    , viewModal : modal -> Html a
    }
    -> Page content modal
    -> Html a

This might look like:

view : Page LocalContent LocalModal -> Html Msg
view page =
  Generic.viewPage
    { viewContent = viewLocalContent
    , viewModal = viewLocalModal
    }
    page

Never

This all worked fine until I created a page that didn’t have any local modals. I figured out that I could have a page type like Page LocalContent Never but what should I pass as the viewModal function?

I could pass a lambda like this but that felt very kludgy:

(\modal -> text "this will never get called")

Eventually I realized that the never function was my solution:

view : Page LocalContent Never -> Html Msg
view page =
  Generic.viewPage
    { viewContent = viewLocalContent
    , viewModal = never
    }
    page

[turboMaCk]

But I found that instead of Html Never one can just use Html msg as a type for the static Html which is perfectly fine when no Event handlers are used.

For most practical purposes this is indeed correct. However one can define this useless Html msg view which attaches event msg event even without passing a way to construct msg:

module NeverIsForever exposing (viewEndOfTheUniverse)

import Html exposing (Html)
import Html.Events as Events

msg : (a -> a) -> a
msg f =
    msg f


viewEndOfTheUniverse : Html msg
viewEndOfTheUniverse =
    Html.div [Events.onClick <| msg identity] []

don’t try this at home

[Janiczek]

At GlobalWebIndex we have a type Error customError:

type Error err
    = -- elm/http errors
      BadUrl String
    | Timeout
    | NetworkError
    | BadStatus Http.Metadata String
    | BadBody Http.Metadata Decode.Error
      -- core-next and gateway errors
    | GenericError UUID GenericError
      -- Extension point for component specific errors (TV, Chart builder etc.)
    | CustomError UUID err
      -- Miscellania
    | OtherError OtherError

Now the various requests decode various customError types.

One might be CBQueryError (so the top-level type would look like Error CBQueryError):

type CBQueryError
    = InvalidQuery
    | EmptyExpression
    | InvalidProjectsCombination InvalidProjectsCombinationData
    | SplitterNotWhitelisted Question

Another might be:

type XBQueryError
    = InvalidQuery
    | EmptyExpression

Now here’s the never kicker: some endpoints don’t have their own customErrors. So the top-level type we use for them is Error Never.

The error type would be useless without some functions that work with it though. Some functions, in the end, have to work with those Error customError values and their CustomError customError variants. You have to provide functions like customError -> String to them, which you have defined for CBQueryError and XBQueryError. But what should you provide for Never?

That’s right, you use never.

[turboMaCk]

That’s correct solution indeed but I think once can still argue that in this case you can get away without Never and use unit type like (), {} or type Unit = Unit in this case.

I sort of feel that only good answer to this question is an answer by another question - Do you think we need number 0 in math? If I add or subtract it from something it does nothing, If I multiply it with something it gives nothing. Never is just type level 0.

0 --> Never
1 --> ()
2 --> Bool
a + b --> Left a | Right b
a * b --> (a, b)

[Janiczek]

By your description it seems like the endpoints that have no custom errors (0) still fall into the 0 --> Never category.

BTW yeah this algebraic way of looking at types is helpful.
Another description: https://guide.elm-lang.org/appendix/types_as_sets.html