The Little Typer (The MIT Press)

Daniel P. Friedman, David Thrane Christiansen

  • 出版商: MIT
  • 出版日期: 2018-09-18
  • 售價: $1,490
  • 貴賓價: 9.5$1,416
  • 語言: 英文
  • 頁數: 424
  • 裝訂: Paperback
  • ISBN: 0262536439
  • ISBN-13: 9780262536431
  • 相關分類: 程式語言
  • 無法訂購

買這商品的人也買了...

商品描述

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 recursion―can also capture patterns of reasoning. The Little Typer does not attempt to teach either practical programming skills or a fully rigorous approach to types. Instead, it demonstrates the most beautiful aspects as simply as possible, one step at a time.

商品描述(中文翻譯)

《The Little Typer》是一本介紹依賴型別(dependent types)的書籍,以逐步演示最美麗的方面為特色。

程式的型別描述了其行為。依賴型別是語言的一個一等公民,比其他類型更強大;僅使用一種語言來描述型別和程式,使得程式描述可以和所描述的程式一樣強大。《The Little Typer》從一個非常類似Scheme的小型語言開始,逐步擴展到涵蓋使用依賴型別進行編程和數學推理的範疇。讀者應該熟悉類似Lisp的編程語言的基礎知識,這些知識在《The Little Schemer》的前四章中有介紹。

《The Little Typer》的前五章提供了理解依賴型別所需的工具;其餘章節則使用這些工具在數學和編程之間建立了一座橋樑。讀者將學習到,他們從編程中熟悉的工具,如對、列表、函數和遞迴,也可以捕捉推理的模式。《The Little Typer》並不試圖教授實用的編程技能或完全嚴謹的型別方法。相反,它以盡可能簡單的方式逐步演示最美麗的方面。