type-inference - 编译器如何知道返回正确的类型？

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

我将尝试一下(没有专门接受 ML 语言或 Lambda 演算方面的训练，并且使用 '{}' 承载语言的时间太长了，所以我的一些词汇可能会丢失):

(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 [] []解析为一些微不足道的值。然而 poodle's core数学断言:
p : List (Attribute msg) -> List (Html msg) -> Html msg
是 p是接受包含 msg 类型值的东西的东西并返回包含 msg 类型值的内容，如果 p 可能是微不足道的总是返回一个完全不涉及任何类型的常量 msg .它将保留任何 msg照原样(因为它没有被赋予任何转换 msg 的函数)，只需以某种方式移动它们。

另见: "Theorems for Free!"作者:Philp Wadler，1989 年深入研究。瓦德勒从这个开始: