问题标签 [type-theory]

阅读Angelika Langer 出色的泛型常见问题解答，我终于开始真正了解泛型的一些更微妙的点。

但我仍然对一些行话感兴趣。我的外行对“最左”和“最右”的理解显然与兰格在她的常见问题解答中使用它的方式不同。

"在执行转换期间类型擦除，这意味着类型参数被它们最左边的边界或对象替换，如果没有指定边界.. "

...

" Type Erasure。 最左边的上限用于类型擦除并替换字节码中的类型参数。在我们的类 Box {...} 中，所有出现的 T 都将替换为上限 Number 。例如，如果 class Box 有一个类型为 T 的私有字段和一个用于设置此私有字段的方法 void set(T content)，然后该字段在类型擦除后将是 Number 类型，并且该方法将被转换为方法 void set(Number content)。 …… ”

...

“类型参数的类型擦除是它的最左边界...... ”

给定Box< T extends Number >；我的理解是这T是类型参数并且Number是界限。那么，既然Number是类型参数的右边T，为什么不Number叫“最右边的界限”呢？这只是一个深奥的数学家说话的例子吗？是不是就像在形式类型理论中，六代表九，左代表右？

有人可以教育我为什么在类型理论中将视觉上更靠右打印的东西称为“最左边”吗？

提前致谢。

我最近一直在 Elm 中研究一个 API，其中一种主要类型是逆变的。所以，我用谷歌搜索看看可以用逆变类型做什么，发现Haskell 中的逆变包定义了 Divisible 类型 class。

定义如下：

事实证明，我的特定类型确实适合 Divisible 类型类的定义。虽然 Elm 不支持类型类，但我确实会不时查看 Haskell 以获得一些灵感。

我的问题：这个类型类有什么实际用途吗？Haskell（或其他语言）中是否有已知的 API 可以从这种分而治之的模式中受益？有什么我应该注意的问题吗？

非常感谢您的帮助。

我编写了一个Const3与 非常相似的Const新类型，但包含三个给定类型参数中的第一个：

我可以为这种新类型定义很多有用的实例，但我必须自己完成。

但是，我在类型级别应用的函数类似于函数

这@pl告诉我相当于const . const.

两者(.)和const都有匹配的新类型包装器：Compose和Const. 所以我想我可以写：

并自动继承有用的实例，例如：

但 GHC 不同意：

这似乎与和的种类Compose有关Const：

因此，经过一番搜索，我发现有一个名为 GHC 的扩展PolyKinds程序允许我执行以下操作：

好像魔法一样，这些种类是正确的：

但我仍然无法将它们组合起来写Const3 = Compose Const Const。

是什么赋予了？有没有一些聪明的方法可以做到这一点，所以我可以从和继承Functor等实例中获益？ConstCompose

（作为旁注，导致我的最初想法Const3是写：

捕捉到幺半群是单对象类别的想法。如果有一个解决方案仍然允许我以某种方式编写上述实例，那就太好了。）

考虑以下通过类型检查器的函数定义对：

即类型的表达式forall a. a可以在需要类型之一的地方使用Int。在我看来，这很像子类型，但据称 Haskell 的类型系统缺少子类型。这些形式的可替代性有何不同？

这个问题并不特定于forall a. a. 其他示例包括：

我一直在思考如何将其推广scanl到任意 ADT。Prelude 方法只是将所有内容都视为一个列表（即Foldable）并将其应用于scanl结构的平面视图。相反，我倾向于将其scanl视为将状态从树的每个节点传递给其子节点的操作，同时在从根向下传播到叶子时应用单曲面操作。因此，例如，在 上Data.Tree，我们有：

因此，例如：

结果是：

这与scanl独立应用树的每个路径相同，保留原始结构。

问题很简单：这是一个有意义的概括吗？即，它是否常用，有分类解释，也许有不同的名称？

依赖类型通常被宣传为一种使您能够断言程序在规范中是正确的方法。因此，例如，要求您编写对列表进行排序的代码- 您可以通过将“排序”的概念编码为类型并编写诸如List a -> SortedList a. 但是你如何证明规范SortedList, 是正确的呢？是不是这样，您的规范越复杂，您将该规范作为一种类型的编码就越有可能不正确？

我对 Haskell 禁止作为“不可预测”的类型有相当不错的直觉：即 aforall出现在类型构造函数的参数中而不是->. 但究竟什么是预测性？是什么让它变得重要？它与“谓词”一词有何关系？

如何系统地计算系统 F 中给定类型的居民数量？

假设有以下限制：

• 所有居民都终止，即没有底部。
• 所有居民都没有副作用。

例如（使用 Haskell 语法）：

• Bool有两个居民。
• (Bool, Bool)有四个居民。
• Bool -> (Bool, Bool)有十六个居民。
• forall a. a -> a有一个居民。
• forall a. (a, a) -> (a, a)有四个居民。
• forall a b. a -> b -> a有一个居民。
• forall a. a居民为零。

为前三个实现算法是微不足道的，但我不知道如何为其他算法做。

下面的这个min定义适用于两个教会编号并返回最小的。每个数字都成为一个延续，将其 pred 发送给另一个，zig 和 zag，直到达到零。此外，其中一个数字在每次调用时都会将 f 附加到结果中，因此，最后，您将看到(\ f x -> f (... (f (f x)) ...))右侧的“f”的数量是调用第一个延续的次数。

似乎min无法在 System-F 上输入。例如，为了在 GHC 上运行它，我不得不使用unsafeCoerce两次：

是否可以min在 System-F（或构造函数）上输入？