the関数 - mrsekut-p

the関数

Idrisのthe関数

code:idris

Idris> :t the

the: (a: Type) -> a -> a

1つの型をとって、その型専用のid関数になる

例えば、intId = the Natとすれば、intIdはNat専用の恒等関数になる

code:idr

intId = the Nat

intId 3 -- 3

intId "hoge" -- error

これを使って、the 型値と書いて「その型は、その値を許容するか」を確認できる

例えば、有限集合型Finは一つの自然数型をとって、それ未満の自然数を許容する型になるが、それを確認してみる

code:idr

the (Fin 3) 3 -- error

the (Fin 3) 2 -- FS (FS FZ)