Haskell 和 Idris 之间的区别：类型宇宙中运行时/编译时的反映

Question

因此，在 Idris 中，编写以下内容是完全有效的。

item : (b : Bool) -> if b then Nat else List Nat
item True  = 42
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A

没有类型签名，这看起来像是一种动态类型的语言。但是，事实上，Idris 是依赖类型的。 item b 的具体类型只能在运行时确定。

这当然是 Haskell 程序员的谈话：Idris 意义上的item b 类型是在编译时给出的，它是if b then Nat ...。

现在我的问题是：我是否正确得出结论，在 Haskell 中，运行时和编译时之间的边界恰好在值世界（False、“foo”、3）和类型世界（Bool、String、 Integer) 而在 Idris 中，运行时和编译时之间的边界跨越了宇宙？

另外，我是否正确假设即使在 Haskell 中使用依赖类型（使用 DataKinds 和 TypeFamilies，参见 this article），上述示例在 Haskell 中也是不可能的，因为与 Idris 相反的 Haskell 不允许值泄漏到类型级别？

Answer 1

现在我的问题是：我是否可以在 Haskell 中得出这样的结论，边界 在运行时和编译时之间恰好在世界之间运行 值（False，“foo”，3）和类型世界（Bool，String， Integer) 而在 Idris 中，运行时和 编译时间跨越宇宙？

Idris 编译为 Epic（更新：不，它不再像 Spearman 在下面的评论中所说的那样编译为 Epis）：

没有语义检查，除了查看名称是否在范围内 --- 它 假设更高级别的语言将执行 类型检查，在任何情况下，Epic 都不应该对 更高级别的类型系统或您应用的任何转换。 类型注释是必需的，但它们只提供提示 编译器（我可能会改变它）。

所以类型在指称上并不重要，即一个术语的含义不取决于它的类型。此外，一些价值级别的东西可以被删除，例如在Vect n A（其中Vect是静态已知长度的列表类型）n（长度）可以被擦除，because

Brady、McBride 和 McKinna 在BMM04 中描述了一些方法 从数据结构中删除索引，利用以下事实 对它们进行操作的函数要么已经拥有 适当的索引，或者如果需要可以快速重建索引。

这里的问题是，Idris 中的 pi 对类型的作用与 Haskell 中的 forall 几乎相同：在这种情况下，它们都是参数化的（尽管这些参数是不同的）。编译器可以使用类型来优化代码，但在这两种语言中，控制流都不依赖于类型，即你不能说if A == Int then ... else ...（尽管，如果A 是规范形式，那么你就可以静态地知道它是否是@ 987654334@ 与否，因此can 写入A == Int，但这仍然不会影响控制流，因为所有决策都是在运行时之前做出的）。 item b 的具体类型在运行时并不重要。

但是正如pigworker 所说，它不一定是类型的参数。以及它不一定是非参数的值。类型级——值级和参数——非参数是完全正交的二分法。详情见this回复。

因此，Haskell 和 Idris 在处理运行时/编译内容的值级事物的方式上有所不同（因为在 Idris 中，您可以使用 . 标记参数以使其可擦除），但它们以大致相同的方式处理类型。

Answer 2

是的，您正确地观察到 Idris 中类型与值的区别与仅编译时与运行时和编译时的区别不一致。这是好事。具有仅在编译时存在的值很有用，就像在程序逻辑中我们只有在规范中使用的“幽灵变量”一样。在运行时有类型表示也很有用，允许数据类型泛型编程。

在 Haskell 中，DataKinds（和 PolyKinds）让我们写

type family Cond (b :: Bool)(t :: k)(e :: k) :: k where
  Cond 'True  t e = t
  Cond 'False t e = e

在不久的将来，我们将能够写作

item :: pi (b :: Bool) -> Cond b Int [Int]
item True  = 42
item False = [1,2,3]

但在实现该技术之前，我们必须处理依赖函数类型的单例伪造，如下所示：

data Booly :: Bool -> * where
  Truey  :: Booly 'True
  Falsey :: Booly 'False

item :: forall b. Booly b -> Cond b Int [Int]
item Truey  = 42
item Falsey = [1,2,3]

你可以用这样的假货走得很远，但如果我们有真货，一切都会变得容易得多。

至关重要的是，Haskell 的计划是维护和分离 forall 和 pi，分别支持参数和临时多态性。 forall 附带的 lambda 和应用程序仍然可以像现在一样在运行时代码生成中删除，但 pi 的那些仍然保留。拥有运行时类型抽象 pi x :: * -> ... 并将老鼠的复杂巢穴 Data.Typeable 扔进垃圾箱也是有意义的。