什么是依赖类型? [英] What is dependent typing?

问题描述

有人可以向我解释依赖打字吗?我对 Haskell、Cayenne、Epigram 或其他函数式语言的经验很少，因此您使用的术语越简单，我就越感激！

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

这里，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>()

这里，empty 接受一个类型 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.

普通语言提供的内容就这么多.如果一种语言还提供第 4 种可能性，即定义从值到类型的函数，则该语言被称为依赖类型.或者换句话说，通过一个值参数化一个类型定义:

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}

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

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

这里，函数的结果类型取决于实际参数值j，因此是术语.

Here, the function's result type depends on the actual argument value j, thus the terminology.

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