haskell – 为什么不依赖类型?

我已经看到几个来源回应的观点是“Haskell正在逐渐成为一种依赖类型语言”。这意味着,随着越来越多的语言扩展,Haskell正在沿着这个大方向漂移,但还不存在。

基本上有两件事我想知道。第一个是,很简单,“作为一种依赖类型语言”是什么意思? (希望没有太技术。)

第二个问题是…有什么缺点?我的意思是,人们知道我们的方向,所以必须有一些优势。但是,我们还没有,所以必须有一些下行阻止人们一路走来。我得到的印象是,问题是复杂性的急剧增加。但是,不是真正理解什么依赖打字是,我不知道肯定。

我所知道的是,每次我开始阅读一个依赖类型的编程语言,文本是完全不可理解的…可能是这就是问题。 (α)

依赖类型实际上只是值和类型级别的统一,所以你可以参数化类型上的值(已经可能与类型类和参数多态性在Haskell),你可以参数化值类型(不严格说来,可能在Haskell ,虽然DataKinds非常接近)。

编辑:显然,从这一点开始,我错了(见@ pigworker的评论)。我将保留其余的作为我被喂养的神话的记录。 :P

从我所听到的移动到完全依赖打字的问题是,它将打破类型和值级别之间的相位限制,允许Haskell编译为具有已擦除类型的高效机器代码。使用我们当前的技术水平,一种依赖类型的语言必须在某一点(或者立即,或者在被编译为依赖类型的字节码或类似的之后)通过解释器。

这不一定是一个根本的限制,但我个人不知道任何当前的研究在这方面看起来有希望,但还没有进入GHC。如果任何人知道更多,我会很乐意纠正。

相关文章

迭代器模式(Iterator)迭代器模式(Iterator)[Cursor]意图...
高性能IO模型浅析服务器端编程经常需要构造高性能的IO模型,...
策略模式(Strategy)策略模式(Strategy)[Policy]意图:定...
访问者模式(Visitor)访问者模式(Visitor)意图:表示一个...
命令模式(Command)命令模式(Command)[Action/Transactio...
生成器模式(Builder)生成器模式(Builder)意图:将一个对...