依赖类型介绍

2022年10月16日

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

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
idris2好像把定义啥的写在一个文件里,然后在console调用

目前为止还没什么特别的。我可以用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].