Haskell和Idris之间的差异:类型Universe中运行时/编译时的反映 [英] Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes

问题描述

因此在Idris中编写以下代码是完全有效的.

So in Idris it's perfectly valid to write the following.

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的具体类型只能在运行时确定.

Without the type signature, this looks like a dynamically typed language. But, indeed, Idris is dependently-typed. The concrete type of item b can only be determined during run-time.

这当然是一个Haskell程序员在谈论的问题:在编译时会给出Idris意义上的item b类型，它是if b then Nat ....

This is, of course, a Haskell-programmer talking: The type of item b in the Idris sense is given during compile-time, it is if b then Nat ....

现在我的问题是:我是否可以得出结论，在Haskell中，运行时和编译时之间的边界恰好在值的世界(False，"foo"，3)和类型的世界(Bool，String，整数)，而在Idris中，运行时和编译时之间的边界跨越了整个宇宙?

Now my question: Am I right to conclude that in Haskell, the border between the runtime and the compiletime runs exactly between the world of values (False, "foo", 3) and the world of types (Bool, String, Integer) whereas in Idris, the border between the runtime and the compiletime goes across universes?

此外，我是否可以假设即使在Haskell中使用依赖类型(使用DataKinds和TypeFamilies，请参见

Also, am I right to assume that even with dependent types in Haskell (using DataKinds and TypeFamilies, cf. this article) the above example is impossible in Haskell, because Haskell contrary to Idris does not allow values to leak to the type-level?

推荐答案

是的，您正确地注意到Idris中的类型与值区别与仅编译时与运行时与编译时的区别不符.这是好事.具有仅在编译时存在的值很有用，就像在程序逻辑中我们仅在规范中使用重影变量"一样.在运行时具有类型表示形式也很有用，从而允许对数据类型进行通用编程.

Yes, you're right to observe that the types versus values distinction in Idris does not align with the compiletime-only versus runtime-and-compiletime distinction. That's a good thing. It is useful to have values which exist only at compiletime, just as in program logics we have "ghost variables" used only in specifications. It is useful also to have type representations at runtime, allowing datatype generic programming.

在Haskell中，DataKinds(和PolyKinds)让我们写

In Haskell, DataKinds (and PolyKinds) let us write

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

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

and in the not too distant future, we shall be able to write

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

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

but until that technology is implemented, we have to make do with singleton forgeries of dependent function types, like this:

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]

您可以通过这种伪造走得很远，但是如果我们拥有真实的东西，一切都会变得容易得多.

You can get quite far with such fakery, but it would all get a lot easier if we just had the real thing.

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

Crucially, the plan for Haskell is to maintain and separate forall and pi, supporting parametric and ad hoc polymorphism, respectively. The lambdas and applications that go with forall can still be erased in runtime code generation, just as now, but those for pi are retained. It would also make sense to have runtime type abstractions pi x :: * -> ... and throw the rats' nest of complexity that is Data.Typeable into the dustbin.

这篇关于Haskell和Idris之间的差异:类型Universe中运行时/编译时的反映的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！