书籍介绍
这是一本会让读者在读完后怅然若失的书——不是因为它艰深，恰恰因为它太温柔。Friedman 延续
作者简介
Daniel P. Friedman is Professor of Computer Science in the School of Informatics, Computing, and Engineering at Indiana University and is the author of many books published by the MIT Press, including The Little Schemer and The Seasoned Schemer (with Matthias Felleisen); The Little Prover (with Carl Eastlund); and The Reasoned Schemer (with William E. Byrd, Oleg Kiselyov, and Jason Hemann).
用户评论
以前看完一部喜欢的长篇小说或者电视剧的时候都会多少有些失落。读完了这本关于编程的书之后竟然也有了类似的感觉。Friedman 的书都是有温度的。写了一篇算是读后感的东西，http://mxm.ink/post/2019-06-09-dependent-type/
打个五星吧。。。不过我只看了最后几章。。。
语言略微繁琐，但全书从基本type开始，通过一个个小故事的叙述，引出dependent type是如何与theorem proving相辅相成，并在最后指出如何拓展Pie到一个成熟的theorem prover。喜欢！
最终还是迷失在iter-Cap, rec-Cap, ind-Cap中了。
在看前面几章，犹如在看哲学书，尽是一些毫无意义的定义，满是一些脱裤子放屁的做法。 说是不能用recursion写function，那还玩个屁，于是强行定义了个iter-nat来用，可iter-nat他妈不recursive吗，最后出个rec-nat...再强加解释说这样做有什么什么好处好自圆其说，跟哲学家一个德行。Friedman的书很多都很喜欢，不过这本书讲述的理论，似乎不太行。放弃。
行文步步推进，节奏略慢，同时过多的专注于自然数，略为trivial。没有引入inductive type，导致自然数，列表等都是作为语言的原语生硬引入，这是最大的硬伤。万丈高楼本可平地起，奈何基础设施不够。
一直感觉Fieldman的书是“高山滚石”式的布局的典范，前期节奏平缓注重体系的自洽和对读者的引导，后半则信息量很大却又水到渠成
Friedman神奇的风格，当小说来看了- -'''
MIT Press的其他书籍查看全部
The Politics of Dating Apps
Hacking Life
Designing with the Body
The Ordinary Man of Cinema
Streaming, Sharing, Stealing
White City, Black City
下载
收藏