『Programming with Types: Examples in TypeScript』を読む

書籍

以下の『Programming with Types: Examples in TypeScript』をところどころ気になった箇所について読みながら、メモを作成する(作業用)。

概要

Programming with Types teaches type-based techniques for writing software that’s safe, correct, easy to maintain, and practically self-documenting. Designed for working developers, this clearly written tutorial sticks with the practical benefits of type systems for everyday programming tasks. Following real-world examples coded in TypeScript, you’ll build your skills from primitive types up to more-advanced concepts like functors and monads.
(from: https://www.oreilly.com/library/view/programming-with-types/9781617296413/

日常的なプログラミングタスクにおいて実践的に型システムの恩恵を得るためのチュートリアルとのこと。なお最終的にはファンクターやモナドといった概念まで突っ込むらしい本。

著者

Vlad Riscutia: MicrosoftでLoopを開発中
https://vladris.com

PADAone🐕

Preface

著者(Vlad Riscutia)は以下の理論/数学側によった書籍などを読み込んで型システムについて学び、型システムのデザインについての理論的な領域と日常的なソフトウェア開発との直接的なつながりがあることを発見した。

Elements of Programming (Alexander Stepanov)
From Mathmatics to Generic Programming (Alexander Stepanov)
Category Theory for Programmers (Bartosz Milewski) → プログラマーのための圏論
Types and Programming Language (Benjamin Pierce) → 型システム入門

著者いわく、型システムを学ぶにつれて書くコードがよくなっていったと語っている。

もちろん、すべてのプログラマーが上記のような数学的証明がある分厚い本を読み込む時間や余裕がないことをわかっているが、型システムについてカバーし、現実的なアプリケーション開発にフォーカスしてその恩恵を気軽に得られるような本が存在しえる余地があると考えてこのような本をつくるにいたったらしい。

この本では、関数型、部分型、OOP、ジェネリックプログラミング、ファンクターやモナドといった高階型の機能について、理論的なバックグラウンドについてフォーカスするのでなく、各機能を現実のアプリケーション開発の側面から見た説明でウォークスルーを提供するとのこと。

なお、最初はC++で解説しようと考えていたが、C++は複雑な言語なので、読者を言語の難易度で限定しないように十分に強力な型システムを備えている一方でシンタックスも簡単なTypeScriptを選択したとのこと。

PADAone🐕

実際、数学的証明が本の中にあるせいで、言語に組み込まれた型システムの機能について知っておくべき内容がかなり高尚なものとして扱われているような気がするのでこのような本が必要になった経緯は妥当だなと思った。

というか、圏論と関数型から来る機能の内容も含まれてるのはありがたい。

数学的証明をすっ飛ばして知識や要点だけ得るだけでもかなりの恩恵があるんじゃないかなー。ざっと知って背景理論の詳細(数学的証明やら細かい話)が気になったらあとからじっくり調べれればいい。

PADAone🐕

Chapter 1. Introduction to typing

カバー内容は以下。

なぜ型システムが存在するのか
強く型付けされたコードの恩恵
型システムの型
さまざまな型システムが提供する共通機能

PADAone🐕

なぜ型は存在するのか

ハードウェアと機械語といった低レベルにおいては、プログラムロジック(コード)とそれが操作するデータは両方ともビットで表現される。このレベルではコードとデータに違いが存在しないため、いずれかにミスがあればエラーが簡単に発生してしまう。

コードとデータの違いを識別するためには、まずデータ片の解釈方法について知る必要がある。例えば、11000101010011 という16ビット列は符号付き整数なら 49827 だが、符号なし整数なら -15709 だし、UTF-8 エンコードなら文字 '£' になってしまう。つまり、このビット列だけではそのデータがどのような意味なのかを決定できない。
プログラムが走るハードウェアはすべてのビット列を保存しているが、このビット列のデータをどのように解釈するかという方法を知るため、つまりデータに意味を与えるための追加のレイヤーが必要であることがわかる。

型はデータに対して意味を与え、所与の文脈においてビット列がなにを表現しているかソフトウェアに解釈させることができる。

型はさらに変数の値についてそれがとることのできる有効な値の集合に制限する。値の範囲を制限できるということは、実行時に出現する可能性のある無効な値を許可しないことでそれに基づくエラーを排除できるということでもある。

PADAone🐕

型と型システム

(1) 型とは
型とは、データに対して可能な操作、データの意味、および許可される値の集合を定義するものであり、型チェックは、データの整合性を確保し、アクセスの制限を強制し、データを開発者の意図通りに解釈させるために行われる。

(2) 型システムとは
型システムとは、プログラミング言語の要素 (変数、関数、他の高階コンストラクトなど) に対して割り当てて強制するような一連のルールのことである。プログラマが注釈を通じてコード上で明示的に行うか、コンテキストに基づいて特定の要素の型を暗黙的に推論することで型システムは型を割り当てる。そして、型システムは型同士でのさまざまな変換についてのルールを定める。

(3) 型チェックとは
型チェックのプロセスは、プログラムが型システムのルールを守っているかどうかを保証する。型チェックはコンパイラがコードを変換するときかコードを実行するランタイム時に行われる。型付け規則の強制をハンドリングするコンパイラのコンポーネントが型チェッカーと呼ばれる。

PADAone🐕

型システムの恩恵

型付けの主な恩恵は以下の5つであり、この5つのすべてはよいソフトウェアデザインと振る舞いについての土台となる特徴にもなっている。

Correctness
Immutability
Encapsulation
Composability
Readability