依赖类型介绍

在函数式语言中，不存在没有参数的方法，不存在没有返回值的方法。如果方法签名用箭头（->）表示，箭头两边都必须有类型。

string getStr()
{
  return "hello";
}

C#方法getStr()在函数式语言中不存在，它会被表示成一个值，无法调用。

泛型

Java 4，我们只能写List l，不能指定l能保存什么类型的元素。Java 5开始支持泛型，List<Integer> l要求l只能保存Integer。

我们可以规定List里面能存什么了，那我们还能声明list的其他性质吗？比如长度，或者索引0的元素的类型？

Simple type -> Generic type -> Dependent type

Dependent types依赖类型，到底是什么依赖什么呢？跟类型相对的就是值，大部分编程语言里都是值依赖类型。比如类型说好了是int，值就不能是3.14或”hello”，因为它们的类型分别是float和string。相对地，依赖类型就是说类型依赖值。比如说值是3.14，那么类型是bool；值是true，那么类型是String。你会问凭什么呀？不凭什么，这是程序逻辑指定的。

下面用idris2定义方法isSingleton。第一行为方法声明，其参数类型为Bool，返回值类型是Type。第二行起为方法的值或方法的事先，用pattern matching的方式定义如果参数的值为True，则返回值为Nat；如果参数的值为False，则返回值为List of Nat。（Nat is natural number）

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

目前为止还没什么特别的。我可以用C#写一个同样的方法。

static Type isSingleton(bool b)
{
	if (b)
		return typeof(double);
	else
		return typeof(double[]);
}

下面是见证奇迹的时刻。idris2方法mkSingle的参数的类型是Bool，但返回值却由isSingleton计算给出。

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

在C#，我们只能设置返回值为object，要具体去看方法体才能知道mkSingle要么返回double类型的值0，要么返回double[]。

static object mkSingle(bool x)
{
	if (x)
		return 0d;
	else
		return new double[0];
}

但是在idris2难道就不用去看方法体了吗？要，但我们看的是isSingleton的方法体。

f : (x : Bool) -> isSingleton x -> Nat
f True n = 0
f False ls = 1

当我们运行f True []，idris先type check。在type checking时期，idris可以调用isSingleton，发现第二个参数必须是Nat，于是报错。

当我们运行f False []，idris先type check。在type checking时期，idris可以调用isSingleton。type check通过后，再执行f的方法体。

由此可见，在type dependent languages，一份方法存在两处，type check time and runtime。^[1]

参考资料

. Types and Functions. Idris2 . [2022-10-17].

参考资料

1. Gqqnbig. How many times does a type function run, can you prove?. . 2022-10-22 [2022-10-23].↑