>Haskellで以前はundefinedを実装を書かずに型チェックを通すために用いていたりしたが、それをコンパイラが強化してサポートしたもの。というかAgdaでまず実装されたものらしい。
> 型が分からない箇所にholeと呼ばれるプレイスホルダ'_'を書いておくと、そこに書くべき値の型をコンパイラが教えてくれるとい
> う機能