为什么不独立输入？ [英] Why not be dependently typed?
问题描述
基本上有两件事我会喜欢知道。首先，很简单地说，作为一种依赖型语言实际上是指是什么？ （希望不要太过于技术性。）
第二个问题是......缺点是什么？我的意思是，人们知道我们正在走这条路，所以必须有一些优势。然而，我们还没有到来，所以肯定会有一些不利因素阻止人们一路走下去。我觉得问题是复杂性急剧增加。但是，并不真正了解依赖类型是什么，我不知道。
我知道的是每次我开始时阅读一种依赖型编程语言，文本是完全不可理解的......可能是这个问题。 （？）
依赖类型实际上就是值和类型级别的统一，因此您可以参数化类型已经可以在Haskell中使用类型类和参数多态性了），并且可以在值上参数化类型（尽管 DataKinds 非常接近，但严格来说，尽管在Haskell中可能是这样。
编辑：显然，从这一点来看，我错了（请参阅@ pigworker的评论）。我将保留其余部分作为我已经喂养的神话的记录。 ：P
从我听说的转向完全依赖型输入的问题是，它会打破在类型和值级别之间的相位限制允许Haskell被编译为具有擦除类型的高效机器代码。使用我们当前的技术水平，依赖类型的语言必须在某个时刻通过解释器（立即或在编译为依赖类型字节码或类似语言之后）。
这并不一定是一个基本的限制，但我没有亲自意识到目前在这方面看起来很有希望的研究，但尚未将其纳入GHC。如果其他人知道更多，我会很乐意改正。
I have seen several sources echo the opinion that "Haskell is gradually becoming a dependently-typed language". The implication seems to be that with more and more language extensions, Haskell is drifting in that general direction, but isn't there yet.
There are basically two things I would like to know. The first is, quite simply, what does "being a dependently-typed language" actually mean? (Hopefully without being too technical about it.)
The second question is... what's the drawback? I mean, people know we're heading that way, so there must be some advantage to it. And yet, we're not there yet, so there must be some downside stopping people going all the way. I get the impression that the problem is a steep increase in complexity. But, not really understanding what dependent typing is, I don't know for sure.
What I do know is that every time I start reading about a dependently-typed programming language, the text is utterly incomprehensible... Presumably that's the problem. (?)
Dependent typing is really just the unification of the value and type levels, so you can parametrize values on types (already possible with type classes and parametric polymorphism in Haskell) and you can parametrize types on values (not, strictly speaking, possible yet in Haskell, although DataKinds gets very close).
Edit: Apparently, from this point forward, I was wrong (see @pigworker's comment). I'll preserve the rest of this as a record of the myths I've been fed. :P
The issue with moving to full dependent typing, from what I've heard, is that it would break the phase restriction between the type and value levels that allows Haskell to be compiled to efficient machine code with erased types. With our current level of technology, a dependently typed language must go through an interpreter at some point (either immediately, or after being compiled to dependently-typed bytecode or similar).
This is not necessarily a fundamental restriction, but I'm not personally aware of any current research that looks promising in this regard but that has not already made it into GHC. If anyone else knows more, I would be happy to be corrected.
这篇关于为什么不独立输入？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
