具体描述
An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. A program's type describes its behavior. Dependent types are a first-class part of a language, and are much more powerful than other kinds of types; using just one language for types and programs allows program descriptions to be as powerful as the programs they describe. The Little Typer explains dependent types, beginning with a very small language that looks very much like Scheme and extending it to cover both programming with dependent types and using dependent types for mathematical reasoning. Readers should be familiar with the basics of a Lisp-like programming language, as presented in the first four chapters of The Little Schemer. The first five chapters of The Little Typer provide the needed tools to understand dependent types; the remaining chapters use these tools to build a bridge between mathematics and programming. Readers will learn that tools they know from programming-pairs, lists, functions, and recursions-can also capture patterns of reasoning. The Little Typer does not attempt to teach either practical programming skills or a fully rigorous approach to type. Instead, it demonstrates the most beautiful aspects as simply as possible, one step at a time.
用户评价
##在看前面几章，犹如在看哲学书，尽是一些毫无意义的定义，满是一些脱裤子放屁的做法。 说是不能用recursion写function，那还玩个屁，于是强行定义了个iter-nat来用，可iter-nat他妈不recursive吗，最后出个rec-nat...再强加解释说这样做有什么什么好处好自圆其说，跟哲学家一个德行。Friedman的书很多都很喜欢，不过这本书讲述的理论，似乎不太行。放弃。
评分##行文步步推进，节奏略慢，同时过多的专注于自然数，略为trivial。没有引入inductive type，导致自然数，列表等都是作为语言的原语生硬引入，这是最大的硬伤。万丈高楼本可平地起，奈何基础设施不够。
评分##打个五星吧。。。不过我只看了最后几章。。。
评分##打个五星吧。。。不过我只看了最后几章。。。
评分##一直感觉Fieldman的书是“高山滚石”式的布局的典范，前期节奏平缓注重体系的自洽和对读者的引导，后半则信息量很大却又水到渠成
评分##语言略微繁琐，但全书从基本type开始，通过一个个小故事的叙述，引出dependent type是如何与theorem proving相辅相成，并在最后指出如何拓展Pie到一个成熟的theorem prover。喜欢！
评分##语言略微繁琐，但全书从基本type开始，通过一个个小故事的叙述，引出dependent type是如何与theorem proving相辅相成，并在最后指出如何拓展Pie到一个成熟的theorem prover。喜欢！
评分##在看前面几章，犹如在看哲学书，尽是一些毫无意义的定义，满是一些脱裤子放屁的做法。 说是不能用recursion写function，那还玩个屁，于是强行定义了个iter-nat来用，可iter-nat他妈不recursive吗，最后出个rec-nat...再强加解释说这样做有什么什么好处好自圆其说，跟哲学家一个德行。Friedman的书很多都很喜欢，不过这本书讲述的理论，似乎不太行。放弃。
评分##行文步步推进，节奏略慢，同时过多的专注于自然数，略为trivial。没有引入inductive type，导致自然数，列表等都是作为语言的原语生硬引入，这是最大的硬伤。万丈高楼本可平地起，奈何基础设施不够。
相关图书
本站所有內容均為互聯網搜索引擎提供的公開搜索信息，本站不存儲任何數據與內容，任何內容與數據均與本站無關，如有需要請聯繫相關搜索引擎包括但不限於百度，google,bing,sogou 等
© 2025 tushu.tinynews.org All Rights Reserved. 求知書站 版权所有