型はコロンで表す

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}だな、ってことがわかる

関連

参考

TaPL p. 71, p.76