圖書標籤: 類型係統 計算機科學 計算機 編程 Types Programming CS programming
发表于2024-12-23
The Little Typer pdf epub mobi txt 電子書 下載 2024
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.
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).
打個五星吧。。。不過我隻看瞭最後幾章。。。
評分Very approachable introduction to dependent type.
評分在看前麵幾章,猶如在看哲學書,盡是一些毫無意義的定義,滿是一些脫褲子放屁的做法。 說是不能用recursion寫function,那還玩個屁,於是強行定義瞭個iter-nat來用,可iter-nat他媽不recursive嗎,最後齣個rec-nat...再強加解釋說這樣做有什麼什麼好處好自圓其說,跟哲學傢一個德行。Friedman的書很多都很喜歡,不過這本書講述的理論,似乎不太行。放棄。
評分在看前麵幾章,猶如在看哲學書,盡是一些毫無意義的定義,滿是一些脫褲子放屁的做法。 說是不能用recursion寫function,那還玩個屁,於是強行定義瞭個iter-nat來用,可iter-nat他媽不recursive嗎,最後齣個rec-nat...再強加解釋說這樣做有什麼什麼好處好自圓其說,跟哲學傢一個德行。Friedman的書很多都很喜歡,不過這本書講述的理論,似乎不太行。放棄。
評分在看前麵幾章,猶如在看哲學書,盡是一些毫無意義的定義,滿是一些脫褲子放屁的做法。 說是不能用recursion寫function,那還玩個屁,於是強行定義瞭個iter-nat來用,可iter-nat他媽不recursive嗎,最後齣個rec-nat...再強加解釋說這樣做有什麼什麼好處好自圓其說,跟哲學傢一個德行。Friedman的書很多都很喜歡,不過這本書講述的理論,似乎不太行。放棄。
首先 这书我前面几乎全跳过了。。。大概只看了附录 如果你觉得速度ok 不是很着急的话 那就慢慢看 零基础都能懂,自洽 不会scheme都能看。千万别觉得前面都读过了最后几章+附录不看也行,开头的那些都是开胃菜重要的都在最后。 如果想稍微速成一点dependent type的话 建议直接做...
評分首先 这书我前面几乎全跳过了。。。大概只看了附录 如果你觉得速度ok 不是很着急的话 那就慢慢看 零基础都能懂,自洽 不会scheme都能看。千万别觉得前面都读过了最后几章+附录不看也行,开头的那些都是开胃菜重要的都在最后。 如果想稍微速成一点dependent type的话 建议直接做...
評分首先 这书我前面几乎全跳过了。。。大概只看了附录 如果你觉得速度ok 不是很着急的话 那就慢慢看 零基础都能懂,自洽 不会scheme都能看。千万别觉得前面都读过了最后几章+附录不看也行,开头的那些都是开胃菜重要的都在最后。 如果想稍微速成一点dependent type的话 建议直接做...
評分首先 这书我前面几乎全跳过了。。。大概只看了附录 如果你觉得速度ok 不是很着急的话 那就慢慢看 零基础都能懂,自洽 不会scheme都能看。千万别觉得前面都读过了最后几章+附录不看也行,开头的那些都是开胃菜重要的都在最后。 如果想稍微速成一点dependent type的话 建议直接做...
評分首先 这书我前面几乎全跳过了。。。大概只看了附录 如果你觉得速度ok 不是很着急的话 那就慢慢看 零基础都能懂,自洽 不会scheme都能看。千万别觉得前面都读过了最后几章+附录不看也行,开头的那些都是开胃菜重要的都在最后。 如果想稍微速成一点dependent type的话 建议直接做...
The Little Typer pdf epub mobi txt 電子書 下載 2024