具體描述
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.
用戶評價
##行文步步推進，節奏略慢，同時過多的專注於自然數，略為trivial。沒有引入inductive type，導緻自然數，列錶等都是作為語言的原語生硬引入，這是最大的硬傷。萬丈高樓本可平地起，奈何基礎設施不夠。
評分##在看前麵幾章，猶如在看哲學書，盡是一些毫無意義的定義，滿是一些脫褲子放屁的做法。 說是不能用recursion寫function，那還玩個屁，於是強行定義瞭個iter-nat來用，可iter-nat他媽不recursive嗎，最後齣個rec-nat...再強加解釋說這樣做有什麼什麼好處好自圓其說，跟哲學傢一個德行。Friedman的書很多都很喜歡，不過這本書講述的理論，似乎不太行。放棄。
評分##打個五星吧。。。不過我隻看瞭最後幾章。。。
評分##語言略微繁瑣，但全書從基本type開始，通過一個個小故事的敘述，引齣dependent type是如何與theorem proving相輔相成，並在最後指齣如何拓展Pie到一個成熟的theorem prover。喜歡！
評分##最終還是迷失在iter-Cap, rec-Cap, ind-Cap中瞭。
評分##Very approachable introduction to dependent type.
評分##最終還是迷失在iter-Cap, rec-Cap, ind-Cap中瞭。
評分##一直感覺Fieldman的書是“高山滾石”式的布局的典範，前期節奏平緩注重體係的自洽和對讀者的引導，後半則信息量很大卻又水到渠成
評分##一直感覺Fieldman的書是“高山滾石”式的布局的典範，前期節奏平緩注重體係的自洽和對讀者的引導，後半則信息量很大卻又水到渠成
相關圖書
本站所有内容均为互联网搜索引擎提供的公开搜索信息，本站不存储任何数据与内容，任何内容与数据均与本站无关，如有需要请联系相关搜索引擎包括但不限于百度，google,bing,sogou 等
© 2026 book.tinynews.org All Rights Reserved. 静思书屋 版权所有