简评: The Little Typer(可能是最容易理解的关于Dependent Type的书)

分享 未结
1 1 0 2
小编 2019-06-13发布
收藏 点赞
来源: 阿莱克西斯

如果这本书都无法让你理解Dependent Type,那么可能没有人能教会你Dependent Type了。

即使如此,这本书也还是很难。

换了新组有很多新东西要熟悉,特别是Deep Learning对我来说是全新的领域,所以最近一直在看书看论文,没有很多时间写东西。

然而这几天让我想更新专栏的反而是这本关于高级类型系统,"Dependent Type"的书,The Little Typer,毕竟Type Theory和Programming Language Theory是程序员特有的“艺术”,感觉是无法放弃的大爱 ⁄(⁄ ⁄ ⁄ω⁄ ⁄ ⁄)⁄ ⁄(⁄ ⁄ ⁄ω⁄ ⁄ ⁄)⁄

什么是Dependent Type

简单来说,比如java的List<T>这里,你要先给定类型参数:T才能得到最终的类型,比如List<String>. 而一般Dependent Type是指这个参数可以是term,或者说是一个值。比如如果java支持dependent type,那么你可以定义只存3个String的List:List<String, 3>

你可以理解为,支持Dependent Type的语言,支持你定义一个类型计算函数x -> T,从而根据输入term/参数的不同,而“计算”出函数/数据的类型,然后你的函数/数据实现必须满足所以可以计算出的类型。 而语言的Type Checker在做类型推导的时候,会在编译时刻跑你的函数来推导类型。

Dependent Type的用处

Dependent Type可以让程序员更细致精确的用类型系统限制系统的表达力,比如只能存10个元素的List,你想往里放11个那就编译不过。那么当你的函数声明自己只能接受有10个元素的数组的时候,你根本不用检查在你的input数组里,别人是不是放多了。

另外就是根据Curry-Howard correspondence,你可以用Dependent Type来写逻辑推导,Formal Proof,来证明最后的“结论”(Type)是对的(可到达的)。达到:“错的”程序编译不了的效果。

The Little Typer

我看过另外2本和Dependent Type有些关系的书。

  • Type-Driven Development with Idris (TDDI)Advanced Topics in Types and Programming Languages (ATTPL)

ATTPL里只有一章是关于Dependent Type的,书比较难,内容学术一点,大概长这样:

TDDI则目的在推广Idris,所以你可以看到更多应用方面的内容,比如怎么处理IO,怎么做Type Safe Concurrent Programming.

The Little Typer则专注在Dependent Type,和用Dependent Type写formal proof这一点,它是比较“啰嗦”的一本书,而这正是它的优势。下边简单说一下这本书的特点:

  1. 为教学而发明的语言:Pie

首先,它为了讲明白Dependent Type,专门发明了一个叫做Pie的非常非常简单的语言,语法类似Scheme, 如果你看过SICP,或者The Little Scheme,那么书里程序的组织对你来说会非常熟悉。就算你完全不知道Lisp,Scheme,那么也完全没问题,因为Pie实在太简单了。这样的讲解方式就防止了话题向IO,Monad等偏移,或增加理解难度。比如Type-Driven Develipment with Idris这本书,如果你对Haskell完全不了解,那么看这本书会比你懂Haskell要难的多。

2. Pie不支持case match

不支持case match使得程序特别繁琐和啰嗦,然而对于初学者来说,这繁琐的过程却正是理解细节的关键。用书里的原文举例,如果Pie支持case match,那么一个从数组里取第一个元素的front函数则可以简单的定义为:

可以看到就这么几行code,然而这个“match es”,隐藏了简直是无数的逻辑,而作者在书里,用没有case match支持的Pie,来向你展示了如何用一个核语言,来实现dependent type的类型推导(多图预警)。

不支持case match的front定义:

可以看到要调用mot-front, zero-not-add1, step-front

mot-front定义:

step-front定义

zero-not-add1我就不贴了,因为它要调另外好几个函数,长度是和上边几个类似。。。

可以看到用Pie实现的逻辑要长很多,因为你需要把高级语言关于dependent type和inductive data type的case match这个魔法,自己来实现。

Pie可以说是需要支持Dependent Type所需要的最小功能集合,或者说,实现了Dependent Type的语言,一般都需要内置一个Pie。而通过Pie来讲解Dependent Type,而不是一门高级语言比如Idris,那么所有高级语言所隐藏的东西,都需要你用Pie写出来。而这些东西却是初学者理解Dependent Type的很好的内容。

3. Pie不支持Implicit Arguments

不支持Implicit Argument简直是救了初学者的命,你知道我看Idris的时候自己脑补Implicit Argument有多痛苦嘛!!!而且Pie需要你任何时候都把类型参数提供的清清楚楚明明白白,而不能省略,对于一门正式的工业界语言来说,这种重复和啰嗦是无法容忍的,但是在教学来说,要求把所有“显而易见”的东西清楚的写出来,这对于一头扎在程序海洋的读者就非常友好。

4. 细节入微的思维线

书以对话的形式进行,就像A,B两个人闲聊天一样,有问有答,甚至有时候A会答错,然后B告诉A怎么错了,在写一个proof的时候,每一步的因为所以都解释的非常清楚,使得程序就好像自然而然就必须这么写一样,整个大段的程序就这么写出来了。。。

最后贴一个有趣的评论:读完本书可以+20 IQ哟!!!!

程序是人表达思维的工具而已,重要的是思维,而不是工具,工具会由思维的表达需要为指导而变化。如果AI和研究如何精准表达,如何抽象,简化,和应用的高级程序语言理论,类型理论,可以结合起来的话,我们的未来会发生什么呢?

我完全不知道它们是否可以结合,但是我想让自己处于可以“翘首以待”的状态,这也许就是我为什么学这些“对目前的我来说,毫无用处的东西”的原因吧。

回帖
  • 消灭零回复