型付け導出の表記

型はコロンで表す

$ t:T

$ \frac{t_1:\mathrm{Bool}\quad t2:T \quad t3:T}{\mathrm{if}\quad t_1\quad\mathrm{then}\quad t_2\quad\mathrm{else} \quad t_3:T}

Tは型引数であり、同一の任意の型が入る

$ t_1はBool型かつ、$ t_2がT型かつ、$ t_3がT型ならば、「if $ t_1 then $ t_2 else $ t_3」という式はT型になる、という意味

「水平線の下の式」が「この型」になる、ということを導出する

あくまでも型のみに言及している

公理っぽくなるのは以下のようなとき

$ \mathrm{true}: \mathrm{Bool}とか

$ 0:\mathrm{Nat}とか

だから逆に$ \mathrm{true}:Rみたいなものがあると、$ R=\mathrm{Bool}だな、ってことがわかる