How does the compiler know to return the right type?

Question

I have the following code, that I do not understand:

type Msg
    = Left | Right


content : Html Msg
content =
    p [] []

The type signature of p:

p : List (Attribute msg) -> List (Html msg) -> Html msg

The question is, why p can return the type of Msg in the content function. I know that Html msg and msg can any variable but it does not return either Left or Right.

Answer 1

I will take a shot at this (not particularly trained in ML languages or Lambda calculus, and worked with '{}' carrying languages for far too long, so some of my vocabulary may be off):

(1) Msg is a type that specializes to either Left or Right

(2) content is a value of type Html(Msg)

(3) content has value p [] []

Let's evaluate content ...

(4) p is a function of type p : List (Attribute msg) -> List (Html msg) -> Html msg

In the expression above msg is a type variable, we could also write, less confusingly:

(4a) p is a function of type p : List (Attribute xtype) -> List (Html xtype) -> Html xtype

In Java syntax that would be something like

(4x) p is a function of type p<XType> : List (Attribute<XType>) -> List (Html<XType>) -> Html<XType>

So we have the following constraint on p [] []:

• It is of type p : List (Attribute xtype) -> List (Html xtype) -> Html xtype
• It resolves to type Html Msg

this immediately tells us that unknown type xtype must actually be type Msg:

(5) p : List (Attribute Msg) -> List (Html Msg) -> Html Msg

The first argument to p is []. According to the constrained signature above, the type of that expression must be List (Attribute Msg). No problem with that, the elm type checking theorem proving engine lets this through.

The second argument to p is []. According to the constrained signature above, the type of that expression must be List (Html Msg). No problem with that either.

• Thus, you can invoke p with [] [].
• Whatever it resolves to will be of type Html Msg.

How is that possible if p doesn't know much about Msg?

Invoke mathematical constraint-based thinking and conclude that p [] [] must resolve to a value of type Html x for every type x. This is only possible if it resolves to a value that does not vary in x - a constant completely independent of x. Therefore p [] [] resolves to some trivial value. However the poodle's core of the mathematical assertion:

p : List (Attribute msg) -> List (Html msg) -> Html msg

is that p is something that takes stuff containing values of type msg and returns stuff containing values of type msg, maybe trivially so if p always returns a constant completely not involving anything of type msg. It will keep any msg as it was (because it has not been given any function transforming msg), just shift them around somehow.

See also: "Theorems for Free!" by Philp Wadler, 1989 for going deeper into this. Wadler starts off with this:

Answer 2

Now the Html type is such a low level type that it is not actually defined with Elm language. But for the purpose of this question let's imagine that Html is defined as

type Html msg
  = HtmlWithMessage HtmlNodes msg
  | HtmlWithoutMessage HtmlNodes

where HtmlNodes would be some type representing the actual html being returned.

Now when you define Msg as type Msg = Left | Right, then type Html Msg can have three possible values:

1. HtmlWithMessage HtmlNodes Left
2. HtmlWithMessage HtmlNodes Right
3. HtmlWithoutMessage HtmlNodes

And since there is no message in p, it would return HtmlWithoutMessage HtmlNodes.

The question is, why p can return the type of Msg in the content function. I know that Html msg and msg can any variable but it does not return either Left or Right.

p is not returning type of Msg, but type of Html which has type parameter msg. The type is not required to use the type parameter in all of its possible values and so can include values which don't use type parameter at all, like HtmlWithoutMessage HtmlNodes.