为什么不依赖类型? [英] Why not be dependently typed?

问题描述

我看到一些消息来源回应了Haskell 正在逐渐成为一种依赖类型的语言"的观点.这意味着随着越来越多的语言扩展，Haskell 正在朝着那个大方向漂移，但还没有.

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. (?)

推荐答案

依赖类型实际上只是值和类型级别的统一，因此您可以在类型上参数化值(在 Haskell 中已经可以使用类型类和参数化多态性)并且您可以对值的类型进行参数化(严格来说，在 Haskell 中尚不可行，尽管 DataKinds 非常接近).

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).

显然，从现在开始，我错了(见@pigworker 的评论).我会保留剩下的内容，作为我被灌输的神话的记录.:P

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

转向完全依赖类型的问题，据我所知，它会打破类型和值级别之间的阶段限制，允许将 Haskell 编译为具有擦除类型的高效机器代码.以我们目前的技术水平，依赖类型的语言必须在某个时候(要么立即，要么在编译为依赖类型的字节码或类似的之后)通过解释器.

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).

这不一定是基本限制，但我个人不知道目前有任何在这方面看起来很有希望但尚未纳入 GHC 的研究.如果有其他人知道更多，我很乐意得到纠正.

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屋！