Haskell - 多态性和值取决于类型
Haskell - polymorphism and values depending on types
从阅读 lambda cube and this thread 的维基百科条目，当应用于 Haskell 时，我的理解是
- 由术语索引的术语族 - 从值到值的典型函数
- 按类型索引的术语系列 - ??
- 按类型索引的类型族 - 类型构造函数中的参数多态性，类型族
- 按术语索引的类型系列 - pi 类型（您在 Haskell 中伪造单例类型）、sigma 类型等...
如果我把上面列出的例子弄错了，请纠正我。引用维基百科文章：
- Terms depending on types, or polymorphism. System F, aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.
我不知道 Haskell 如何适合上面的 (2)。 Haskell 术语和类型之间有很强的区别，并且类型擦除，所以你在 OOP 中没有反射的东西，例如 typeof(a) 或 b.GetType()，然后继续 return 运行 时基于类型信息的一些值。
所以我在 Haskell 中唯一能想到的关于 (2) 的可能是
- Return type polymorphism in say
mempty in Data.Monoid, where value depends on the instance type
- 您在 LHS 上接受类型并在 RHS 上具有值构造函数的数据族
这样对吗？虽然我觉得我没有建立所有的联系......
说临时多态性满足 (2) 而参数多态性满足 (3) 是否正确？但是，ad-hoc 与参数化如何与类型与数据系列的 RHS 差异相关？
最后一件事，如何求和类型值，例如
Nothing :: forall a. Maybe aRight 3 :: forall a. Num b => Either a b
当他们缺乏适合这张图片的类型上下文时？我的猜测是这是 (2)?
的一个例子
按类型索引的术语
在 lambda 立方体中，这是参数多态性。
在系统 F 中，多态项看起来像将类型作为参数和 return 个项的函数。
id : ∀ a. a -> a
id = Λa . λx : a . x -- Λ binds type args, λ binds term args
它们可以通过显式应用到类型来实例化：
boolId : Bool -> Bool
boolId = id Bool
在Haskell中，面向用户的语言没有明确的类型应用和抽象，因为类型推断可以在大多数（但不是全部）情况下填充细节。相比之下，GHC Haskell 的中间语言 GHC Core 与 System F 非常相似，并且确实具有类型应用程序。
类型擦除与我们是否可以按类型索引术语是正交的。它的发生使得在 Haskell 中类型可以从运行时中删除，但我们可以想象其他语言没有统一大小的运行时对象，因此它们需要保留类型（或大小信息）。
按类型索引的类型
在 lambda 立方体意义上，这意味着具有从类型和类型构造函数到类型和类型构造函数的函数。
Haskell 没有类似的功能。类型族最接近，但它们都是 weaker and stronger.
键入 类 和 lambda 立方体
类型 类 是未在 lambda 立方体中建模的奇怪野兽。在 Haskell 中，它们脱糖为函数和字典传递，因此它们甚至不会出现在 GHC Core 中。它们可以被看作是对程序的某种预处理，依赖于实例的自我强加的唯一性来确定性地填充细节。
从阅读 lambda cube and this thread 的维基百科条目，当应用于 Haskell 时，我的理解是
- 由术语索引的术语族 - 从值到值的典型函数
- 按类型索引的术语系列 - ??
- 按类型索引的类型族 - 类型构造函数中的参数多态性，类型族
- 按术语索引的类型系列 - pi 类型（您在 Haskell 中伪造单例类型）、sigma 类型等...
如果我把上面列出的例子弄错了，请纠正我。引用维基百科文章：
- Terms depending on types, or polymorphism. System F, aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.
我不知道 Haskell 如何适合上面的 (2)。 Haskell 术语和类型之间有很强的区别，并且类型擦除，所以你在 OOP 中没有反射的东西，例如 typeof(a) 或 b.GetType()，然后继续 return 运行 时基于类型信息的一些值。
所以我在 Haskell 中唯一能想到的关于 (2) 的可能是
- Return type polymorphism in say
memptyinData.Monoid, where value depends on the instance type - 您在 LHS 上接受类型并在 RHS 上具有值构造函数的数据族
这样对吗？虽然我觉得我没有建立所有的联系......
说临时多态性满足 (2) 而参数多态性满足 (3) 是否正确？但是，ad-hoc 与参数化如何与类型与数据系列的 RHS 差异相关？
最后一件事，如何求和类型值，例如
Nothing :: forall a. Maybe aRight 3 :: forall a. Num b => Either a b
当他们缺乏适合这张图片的类型上下文时？我的猜测是这是 (2)?
的一个例子按类型索引的术语
在 lambda 立方体中，这是参数多态性。
在系统 F 中，多态项看起来像将类型作为参数和 return 个项的函数。
id : ∀ a. a -> a
id = Λa . λx : a . x -- Λ binds type args, λ binds term args
它们可以通过显式应用到类型来实例化：
boolId : Bool -> Bool
boolId = id Bool
在Haskell中，面向用户的语言没有明确的类型应用和抽象，因为类型推断可以在大多数（但不是全部）情况下填充细节。相比之下，GHC Haskell 的中间语言 GHC Core 与 System F 非常相似，并且确实具有类型应用程序。
类型擦除与我们是否可以按类型索引术语是正交的。它的发生使得在 Haskell 中类型可以从运行时中删除，但我们可以想象其他语言没有统一大小的运行时对象，因此它们需要保留类型（或大小信息）。
按类型索引的类型
在 lambda 立方体意义上，这意味着具有从类型和类型构造函数到类型和类型构造函数的函数。
Haskell 没有类似的功能。类型族最接近，但它们都是 weaker and stronger.
键入 类 和 lambda 立方体
类型 类 是未在 lambda 立方体中建模的奇怪野兽。在 Haskell 中，它们脱糖为函数和字典传递，因此它们甚至不会出现在 GHC Core 中。它们可以被看作是对程序的某种预处理，依赖于实例的自我强加的唯一性来确定性地填充细节。