Haskell 和 Idris 之间的区别：Runtime/Compiletime 在类型域中的反映
Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes
因此在 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 中，运行 时间和编译时间 运行 之间的边界恰好位于值的世界之间（错误， "foo", 3) 和类型世界（Bool、String、Integer），而在 Idris 中，运行时间和编译时间之间的边界跨越宇宙？
此外，我是否可以假设即使 Haskell 中存在依赖类型（使用 DataKinds 和 TypeFamilies，参见 this article），上述示例在 Haskell 中也是不可能的，因为Haskell 与 Idris 不允许值泄漏到类型级别相反？
是的，您观察到 Idris 中类型与值的区别与仅编译时与运行时和编译时的区别不一致。这是好事。仅在编译时存在的值很有用，就像在程序逻辑中我们仅在规范中使用 "ghost variables" 一样。在运行时具有类型表示也很有用，允许数据类型泛型编程。
在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 扔进垃圾箱也是有意义的。
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?
Idris 编译为 Epic（更新：不，它不再像 Spearman 在评论中所说的那样编译为 Epis下面）：
No semantic checking, other than to see if names are in scope --- it
is assumed that the higher level language will have performed
typechecking, and in any case Epic should make no assumptions about
the higher level type system or any transformations you've applied.
Type annotations are required, but they only give hints to the
compiler (I might change this).
所以类型在指称上并不重要，即术语的含义不取决于它的类型。此外，可以删除一些值级别的东西，例如in Vect n A（其中Vect是静态已知长度的列表类型）n（长度）可以被删除，because
There are methods described by Brady, McBride and McKinna in BMM04
to remove the indices from data structures, exploiting the fact that
functions operating on them either already have a copy of the
appropriate index or the index can be quickly reconstructed if needed.
这里的问题是 Idris 中的 pi 对类型的作用与 Haskell 中的 forall 几乎相同：它们都是参数化的（尽管这些参数化性不同）在这种情况下。编译器可以使用类型来优化代码，但是在这两种语言中，控制流都不依赖于类型，即你不能说 if A == Int then ... else ... （但是，如果 A 是规范形式，那么你知道静态地不管它是否是 Int，因此 can 写成 A == Int，但这仍然不影响控制流，因为所有决定都是在运行时之前做出的）。 item b 的具体类型在运行时并不重要。
然而 pigworker says it's not necessarily to be parametric in types. As well as it's not necessarily to be non-parametric in values. Type-level — value-level and parametric — non-parametric are completely orthogonal dichotomies. See this 回答详情。
所以 Haskell 和 Idris 在处理 runtime/compile 内容的价值级别方面是不同的（因为在 Idris 中你可以用 . 标记一个参数以使其可擦除），但他们对待类型的方式大致相同。
因此在 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 中，运行 时间和编译时间 运行 之间的边界恰好位于值的世界之间（错误， "foo", 3) 和类型世界（Bool、String、Integer），而在 Idris 中，运行时间和编译时间之间的边界跨越宇宙？
此外，我是否可以假设即使 Haskell 中存在依赖类型（使用 DataKinds 和 TypeFamilies，参见 this article），上述示例在 Haskell 中也是不可能的，因为Haskell 与 Idris 不允许值泄漏到类型级别相反？
是的，您观察到 Idris 中类型与值的区别与仅编译时与运行时和编译时的区别不一致。这是好事。仅在编译时存在的值很有用，就像在程序逻辑中我们仅在规范中使用 "ghost variables" 一样。在运行时具有类型表示也很有用，允许数据类型泛型编程。
在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 扔进垃圾箱也是有意义的。
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?
Idris 编译为 Epic（更新：不，它不再像 Spearman 在评论中所说的那样编译为 Epis下面）：
No semantic checking, other than to see if names are in scope --- it is assumed that the higher level language will have performed typechecking, and in any case Epic should make no assumptions about the higher level type system or any transformations you've applied. Type annotations are required, but they only give hints to the compiler (I might change this).
所以类型在指称上并不重要，即术语的含义不取决于它的类型。此外，可以删除一些值级别的东西，例如in Vect n A（其中Vect是静态已知长度的列表类型）n（长度）可以被删除，because
There are methods described by Brady, McBride and McKinna in BMM04 to remove the indices from data structures, exploiting the fact that functions operating on them either already have a copy of the appropriate index or the index can be quickly reconstructed if needed.
这里的问题是 Idris 中的 pi 对类型的作用与 Haskell 中的 forall 几乎相同：它们都是参数化的（尽管这些参数化性不同）在这种情况下。编译器可以使用类型来优化代码，但是在这两种语言中，控制流都不依赖于类型，即你不能说 if A == Int then ... else ... （但是，如果 A 是规范形式，那么你知道静态地不管它是否是 Int，因此 can 写成 A == Int，但这仍然不影响控制流，因为所有决定都是在运行时之前做出的）。 item b 的具体类型在运行时并不重要。
然而 pigworker says it's not necessarily to be parametric in types. As well as it's not necessarily to be non-parametric in values. Type-level — value-level and parametric — non-parametric are completely orthogonal dichotomies. See this 回答详情。
所以 Haskell 和 Idris 在处理 runtime/compile 内容的价值级别方面是不同的（因为在 Idris 中你可以用 . 标记一个参数以使其可擦除），但他们对待类型的方式大致相同。