Improvements to generic return types to reduce confusion

[harrysarson]

I recently saw a discussion on slack about the type annotations for functions that can return any type. For example: myList : List a or myMaybe : Maybe a

Of course myList must be an empty list because how else could it be a list containing any type of value.

Of course myMaybe must be Nothing because if it was Just 7, Just "hello" or Just anything it would not be able to have the type Maybe a.

Now it has taken me ~6 months of using with elm to realise the truth of the above two statements despite how obvious they seem to me now I have clocked them. For a long time, I thought that ports are defined with a generic return type because they were in some way “magic”. Instead, commands related to a port will never give a message back to the update function.

The realisation came when I was trying out rust and found https://doc.rust-lang.org/nightly/book/second-edition/ch19-04-advanced-types.html#the-never-type-that-never-returns. In rust there is a special symbol for this “never type” which is !.

If elm used ! for these never types and I had found a port definition like port myPort : String -> Cmd ! I may have been very confused. However, I then would have googled “exclamation mark elm” and been taken to the elm docs (or stack overflow) where I would have understood that ! means that no messages can be produced. My confusion would have lasted ~5 minutes instead of ~6 months.

Note: the “never type” in rust is very different from the elm Never type. The special symbol I am proposing would work exactly like generic return types do currently. For example empty : List a -> empty : List ! and the value could be used in exactly the same way as it is now.

I am not necessarily advocating using ! here, other symbols such as _ would also be viable. Something completely different may also be good.

To summarise

list1 : a -> List a and list2 : a -> List b look very similar but are infact have completely different implications. It would be good if they also looked very different.

---

Edit: added note about elm’s Never.

[Warry]

There is a Never type in Elm too (https://package.elm-lang.org/packages/elm/core/latest/Basics#Never). The main difference from a given type variable is that it can never be setted/mapped/mixed or anything. Never is final, and can’t be composed with. That’s why it’s almost only used in Task, and not let’s say Html.

[Warry]

Hm! by linking to the docs, I read what the never (lower case) function actually does, and it’s very cool! It actually allows to map Never to anything, which defeats some of my statement above.

[joelq]

@harrysarson it’s a really exciting moment once you make that connection! All of a sudden you start seeing that pattern everywhere. For example Html a for HTML with no event handlers or Task x String for a task that can never fail.

As @Warry mentioned, there is a Never type in Elm.

While it might be more correct to say:

empty : List Never
empty =
  []

it does make it harder pass into other functions. For example, I should be able to sum an empty list (because it can be considered a list of numbers) but I can’t pass a List Never into List.sum : List number -> number.

The solution as mentioned by @Warry is to use the never helper. We could say List.map never empty to convert our List Never into a List a. If we’re going to need to do that every time we want to use our empty list, we may as well define it as a List a to start with.

That’s why folks usually prefer empty : List a instead of empty : List Never

I could see an argument for giving up a little bit of convenience in exchange for more obvious code using Never

[harrysarson]

There is one detail I left out about the rust never type: it can be coerced into any type. Therefore, the rust never type works in the same way as generic return types in elm (not like elm’s never type).

I am not proposing using Never in elm, but instead something new to represent a type that can be converted into any of type.

I will edit my post to clarify.

[bChiquet]

A generic type (a) won’t necessarily mean Never. If you look at types like a puzzle system, a is an universal plug. But then, generic types can also be constrained. For instance:
flipTuple : (a, b) -> (b, a)
can not be freely replaced by:
ambiguous : (a, a) -> (a, a)
nonsense : (Never, Never) -> (Never, Never)

What I’m trying to point out is that generics in the type system are inherently related to constraint logics. Much of their power is that you can constrain them to mean special things (e.g. there is only one implementation for (a, b) -> a). Special-casing generic types with no constraints as Never or Anything may help understanding the special case where generics aren’t constrained, but it ill make harder to understand how you can constrain generics to make beautiful APIs.

[gigobyte]

How about coming up with a semantic name for the generic type? Something like List never sounds good to me.

[rupert]

@harrysarson

commands related to a port will never give a message back to the update function.

If elm used ! for these never types and I had found a port definition like port myPort : String -> Cmd ! I may have been very confused.

Glad to hear you are getting to grip with this. I wanted to point out a few small glitches in your reasoning:

A port type might look like

port myPort : String -> Cmd msg

but not like

port myPort : String -> Cmd Never

The reason is, that the msg above is a type variable which is not yet bound to any type at all. This type is open so that it can be bound to your Msg type when you use it:

type Msg 
  = MyMsg
  | MoreMsgs 
  ...

So if I call the port in my update function, msg which is a variable is free to bind to Msg:

update : Msg -> Model -> (Model, Cmd Msg)
update msg model = 
  ...
     myPort "hello" -- This takes the type Cmd Msg

So even though the Cmd never ‘gives back a message to the update function’ its type cannot be Never, otherwise it could not match the type of the update function.

What actually happens when Elm is figuring out the the type, is something called ‘unification’. Unification is an algorithm over structures that may contain variables, and where free variables in the two structures can be bound to the corresponding value on the other side. Its a bit hard to explain briefly, but google ‘unification in logic programming’ or something. Or check out the language Prolog. Here are some examples:

Cmd msg 'unifies with' Cmd Msg 
with
msg == Msg

Cmd Never 'does not unify with' Cmd Msg
since
Never != Msg

(a -> b) -> List a -> List b 'unifies with' (String -> Int) -> List String -> List Int
with
a == String
b == Int

There is a bit more to type checking than just unification, but once you have grasped the concept of it, it should all make a lot more sense.

@harrysarson

I am not proposing using Never in elm, but instead something new to represent a type that can be converted into any of type.

Any lower case type variable is already a type that can be converted into any type. It is a free variable, that can be bound to another type. This happens whenever you use a function or a type with a variable in it - by unification.

[harrysarson]

I think I have confused folk here by talking about “never” (sorry!). What I am proposing is replacing type definitions: empty : List a would become empty : List !.

The ! above would represent the type variable that is not yet bound to a type. ! can be coerced/bound to any type.

Examples:

• A (pointless) function that takes any list and returns an empty list: makeEmpty : List a -> List !
• Some HTML that never produces messages: view : Model -> Html !
• Task.succeed from elm/core: succeed : a -> Task ! a.

(! could be replaced by _ or something else in the above)

[rupert]

@harrysarson

empty : List a would become empty : List !

The a is needed, because there can be more than one variable. If ! was used that would limit type expressions to having at most one variable. For example, the type of List.map is:

map : (a -> b) -> List a -> List b

and I think you can see that this type definition would not be the same:

map : (! -> !) -> List ! -> List !

When a is bound to say Int, the input list that also has an a in its type must be List Int; similar for the output type b.

[harrysarson]

In my plan, ! could not be used unless it could be converted to any type.

map : (a -> b) -> List a -> List b

a and b cannot be any type, they are determined by the function you give the map function.

[dmy]

For those that use slack, I think that this is what @rtfeldman proposed here a few weeks ago (with _ instead of !).

You may find the discussion relevant.

[rupert]

I see. I think _ has more precedent as a wildcard than !; I guess that originally comes from Prolog.

[rupert]

@harrysarson

Some HTML that never produces messages: view : Model -> Html !

When I write view functions that never produce messages, I use the Never type:

mySubView : Model -> Html Never
mySubView model = ...

view : Model -> Html Msg
view model = 
   mySubView model |> Html.map never

never is a special function in Basic (that can never be called!):

never : Never -> a

I prefer to make it quite explicit that a view function can Never produce any messages, rather than leaving a free variable to allow that piece of the view to be bound into any view type.