Thinking with Types
MEMO:
良い本だが難しいので中断中。もうちょっと Haskell 書きなれたら再度チャレンジしたい
I. Fundamentals
1. The Algebra Behind Types
1.1. 同型と濃度(cardinarity)
1.2. 和(sum)、積(product)、べき乗(exponential)
1.3 Example: Tic-Tac-Toe
1.5. 正準表現 Canonical Representations
2. Terms, Types and Kinds
2.1. The Kind System
Kind -> Types of Types 型の型
TYPE Kind レベルでの型
2.2 Arrow Knd
Maybe :: TYPE -> TYPE
Either :: TYPE -> TYPE -> TYPE
MaybeT :: TYPE -> TYPE -> TYPE -> TYPE
MaybeT はモナドど型を受けて型を返すが、モナドはMonad :: TYPE -> TYPE なので全体として上のようになる
2.1.3 Constraint Kinds
Show a => a -> String
Showは type signature の一部
Showは Kind を持つか？ー＞持つ
この類の kind は constraint kind になる
2.2 Data Kinds
-XDataKinds
TYPE, CONSTRAINT とそれらのアロー表記が使える
code:haskell
data Bool
= True
| False
-XDataKinds ある場合は次の kind 定義が得られる
code:haskell
kind Bool
= 'True
| 'False
2.3 Promotin of Build-In Types
import GHC.TypeLits
2.3.1 Symbols
:set -XDataKinds
:kind "hello"
2.4 Type-Level Functions
3. Variance
covariance
contravariance
invarinace
プラス、マイナスの属性を付けて varinace を判定できる
a -> b
a は マイナス、b は +
bifunctor
profunctor
II. Lifting Restrictions
4. Working with Types
4.1 Type Scoping
Haskell の型変数は普通使い回しはできない
-XScopedTypeVariables を使えば forall などで使いまわしできる
4.2 Type Applications
4.3 Ambiguous Types
5. Constraints and GADTs
Constraints
型の制限？
GADT
data type に型を書けるようになる
6 Rank-N Types
forall
Rank はいわば多相性の深さ(the "depth" of its polymorphism)
7. Existential Types
7.1 Existential Types and Eliminators
存在型を使うと動的言語のようなこともできる。
-XConstraintsKind
8. Roles
Coerce
newtype はゼロコストの抽象
code:haskell
coerce :: Coercible a b => a -> b
coerce でnewtypeへの変換がゼロコストで扱える
coerce は常に安全に使えるわけではな/いのに注意
Map k v と Map (Reverse k) v
coerce 可能だがメモリレイアウトはまったく異なる
Roles
the role system ensures coercions are safe.
タイプパラメタは role を持つ
roles:
nominal
representational
phantom
-XRoleAnnotations 設定後、role のアノテーションを追加できる
code:haskell
type role BST nominal
III Computing at the Type-Level
9. Associated Type Families
printf
code:haskell
class HasPrintf a where
type Printf a :: Type // Associated Type Family
format :: String
-> Proxy a
-> Printf a
型クラスHasPrintfのインスタンスは、format 関数の他にPrintf aを決定する必要がある
Building types from a schema
Generating Associated TErms
10. First Class Families
ファーストクラスとしてのType Family
元々はできないと考えられていた
条件の緩和
Defuncionalizationを使用する
ex) fst
code:haskell
fst :: (a,b) ->
fst (a,b) -> a
defunctionalize!
code:haskell
data Fst a b = Fst (a,b)
class Eval l t | l -> t where
eval :: l -> t
instance Eval (Fst a b) a where
eval (Fst (a,b)) -> a
Type level defuncionalization
11. Extensible Data
python の dictionary のような "Extensible" なレコード型も Haskellでできる。
12. Custom type errors
13. Generics
14 Indexd Monad
15. Dependent Types