Holes
from
Idris
どんな型を持つ値を書けばよいのかを調べるやつ
型宣言している前提
?hoge
を使う
例
code:idr
hello : IO ()
hello = putStrLn ?greeting
これでコンパイルが通るので、
>:t greeting
とすると、greetingはString型の値を書くよというのがわかる
型を調べる以外にも、Haskellのundefinedのように、実装を書かずに型のみで仕様を書き終えることにも使えそう
http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#holes