haskell - Haskell 和 Idris : Reflection of Runtime/Compiletime in the type universes 之间的区别

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 程序员的谈话:item b 的类型在 Idris 意义上是在编译时给出的，它是 if b then Nat ... .

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

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

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进垃圾箱。