Как компилятор знает, как вернуть правильный тип?

Question

У меня есть следующий код, который я не понимаю:

type Msg
    = Left | Right


content : Html Msg
content =
    p [] []

Подпись типа p:

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

Вопрос в том, почему p можетвернуть тип Msg в функции content.Я знаю, что Html msg и msg могут использовать любую переменную, но она не возвращает ни Left, ни Right.

Answer 1

Теперь тип Html является настолько низкоуровневым типом, что на самом деле он не определен в языке Elm.Но для целей этого вопроса давайте представим, что Html определяется как

type Html msg
  = HtmlWithMessage HtmlNodes msg
  | HtmlWithoutMessage HtmlNodes

, где HtmlNodes будет некоторым типом, представляющим реальный возвращаемый html.

Теперь, когда вы определитеMsg как type Msg = Left | Right, тогда тип Html Msg может иметь три возможных значения:

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

И поскольку в p нет сообщения, оно вернет HtmlWithoutMessage HtmlNodes.

Вопрос в том, почему p может возвращать тип Msg в функции content.Я знаю, что Html msg и msg могут использовать любую переменную, но она не возвращает ни Left, ни Right.

p не возвращает тип Msg, но типHtml с параметром типа msg.Типу не обязательно использовать параметр типа во всех его возможных значениях, поэтому он может включать значения, которые вообще не используют параметр типа, например HtmlWithoutMessage HtmlNodes.

Answer 2

Я сделаю снимок (не особенно обучался языкам ML или лямбда-исчислению и слишком долго работал с языками '{}', поэтому некоторые из моего словарного запаса могут быть отключены):

(1) Msg - это тип, который специализируется на Left или Right

(2) content - это значение типа Html(Msg)

(3)content имеет значение p [] []

Давайте оценим content ...

(4) p - это функция типа p : List (Attribute msg) -> List (Html msg) -> Html msg

ВВыражение выше msg является переменной типа, мы могли бы также написать, не так запутанно:

(4a) p - это функция типа p : List (Attribute xtype) -> List (Html xtype) -> Html xtype

В синтаксисе Java это было бычто-то вроде

(4x) p является функцией типа p<XType> : List (Attribute<XType>) -> List (Html<XType>) -> Html<XType>

Итак, у нас есть следующее ограничение на p [] []:

• Этотипа p : List (Attribute xtype) -> List (Html xtype) -> Html xtype
• Он разрешает тип Html Msg

, что немедленно говорит нам о том, что неизвестный тип xtype действительно должен иметь тип Msg:

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

Первый аргументот p до [].В соответствии с приведенной выше ограниченной подписью тип этого выражения должен быть List (Attribute Msg).Никаких проблем с этим, механизм проверки теорем проверки типа вяза пропускает это.

Второй аргумент p - [].В соответствии с приведенной выше ограниченной подписью тип этого выражения должен быть List (Html Msg).С этим тоже проблем нет.

• Таким образом, вы можете вызывать p с помощью [] [].
• Все, что разрешается, будет иметь тип Html Msg.

Как это возможно, если p не знает много о Msg?

Вызвать математическое мышление на основе ограничений и заключить, что p [] [] должно разрешить значение типа Html x для каждого типа x.Это возможно только в том случае, если оно разрешается до значения, которое не изменяется в x - константа, полностью независимая от x.Поэтому p [] [] разрешается до некоторого тривиального значения.Однако ядро ​​ пуделя математического утверждения:

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

состоит в том, что p - это то, что принимает вещи, содержащие значения типа msg, и возвращает вещисодержит значения типа msg, может быть тривиально, так что если p всегда возвращает константу, полностью не включающую ничего типа msg.Он будет сохранять все msg как было (потому что ему не было дано никакой функции, преобразующей msg), просто как-то сдвинул их.

См. Также: "Теоремы бесплатно!" от Philp Wadler, 1989, для углубления в это.Вадлер начинает с этого: