什么是依赖型打字？ [英] What is dependent typing?

问题描述

有人可以解释依赖打字给我吗？我在Haskell，Cayenne，Epigram或其他函数式语言方面几乎没有经验，所以您可以使用的术语越简单，我越会感激它！

解决方案考虑到这一点：在所有体面的编程语言中，你可以编写函数，例如

  def f（arg） =结果
  

这里 f 取值 arg 并计算值 result 。它是一个从值到值的函数。

现在，有些语言允许你定义多态（又名通用）值：

  def空< T> = new List< T>（）
  

这里，空接受一个类型 T 并计算一个值。它是一个从类型到值的函数。

通常，你也可以有泛型类型定义：

 键入Matrix< T> = List< List< T>> 
  

这个定义需要一个类型并返回一个类型。它可以被看作是一个从类型到类型的函数。

对于普通语言提供的东西太多了。如果一种语言也提供了第四种可能性，那么它就被称为从属类型，即从数值到类型定义函数。换句话说，通过一个值参数化一个类型定义：

  type BoundedInt（n）= {i：Int | i< = n} 
  

有些主流语言有一些假的形式，不要混淆。例如。在C ++中，模板可以将值作为参数，但在应用时它们必须是编译时常量。一种真正的依赖型语言并非如此。例如，我可以使用上面的类型：

  def min（i：Int，j：Int）：BoundedInt j）= 
 if i<编辑：在这里，函数的结果类型取决于。  关于实际参数值 j ，因此是术语。
 
Can someone explain dependent typing to me?  I have little experience in Haskell, Cayenne, Epigram, or other functional languages, so the simpler of terms you can use, the more I will appreciate it!
解决方案
Consider this: in all decent programming languages you can write functions, e.g.
def f(arg) = result
Here, f takes a value arg and computes a value result. It is a function from values to values.

Now, some languages allow you to define polymorphic (aka generic) values:
def empty<T> = new List<T>()
Here, empty takes a type T and computes a value. It is a function from types to values.

Usually, you can also have generic type definitions:
type Matrix<T> = List<List<T>>
This definition takes a type and it returns a type. It can be viewed as a function from types to types.

So much for what ordinary languages offer. A language is called dependently typed if it also offers the 4th possibility, namely defining functions from values to types. Or in other words, parameterizing a type definition over a value:
type BoundedInt(n) = {i:Int | i<=n}
Some mainstream languages have some fake form of this that is not to be confused. E.g. in C++, templates can take values as parameters, but they have to be compile-time constants when applied. Not so in a truly dependently-typed language. For example, I could use the type above like this:
def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j
Edit: Here, the function's result type depends on the actual argument value j, thus the terminology.

                        
这篇关于什么是依赖型打字？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！