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，参见 这篇文章），上面的例子在 Haskell 中也是不可能的，因为与 Idris 不同，Haskell 不允许值泄漏到类型层次？

- ruben.moor

---

好的问题！我会引导你关注@pigworker的这个演讲，以补充他的答案。 - Benjamin Hodgson

你能否创建一个idris-Universe的主题/标签，并使用它来代替MultiValue数据库中的universe吗？ - Mike

@Mike：“创建一个新标签需要至少1500的声望值...” 我猜，一个合适的标签应该是“类型宇宙”。 - ruben.moor

Answer 1

是的，你观察到了在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非常复杂。

- pigworker

---

GHC 8: https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#overview-of-type-in-type完全依赖类型的语言也消除了表达式和类型之间的区别，但在GHC中实现这一点是另一回事。 - ruben.moor

是的，这确实是一个故事，也许并不遥远的另一天再讲吧。 - pigworker

Answer 2

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

Idris编译成Epic（更新：不，正如Spearman在下面的评论中所说，它不再编译成Epic）：

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

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

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

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

然而，正如pigworker所说，它不一定是类型参数化的。同样，值不一定是非参数化的。类型级别 - 值级别和参数化 - 非参数化完全是正交的二分法。有关详细信息，请参见this答案。

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

- effectfully

---

"Idris编译成Epic"这是否仍然适用？Idris实现论文（2013）提到Epic作为编译器后端，但是Idris更改日志表明，与Epic的依赖关系在Idris 0.9.3（2012-09-15）中被删除，几乎比论文发表早一年。当前的Idris源代码（1.0）似乎不包含任何关于“Epic”的引用。 - Spearman