Type-Holes
https://ruicc.hatenablog.jp/entry/20130302/1362237249
Haskell
で以前はundefinedを実装を書かずに型チェックを通すために用いていたりしたが、それをコンパイラが強化してサポートしたもの。というか
Agda
でまず実装されたものらしい。
型が分からない箇所にholeと呼ばれるプレイスホルダ'_'を書いておくと、そこに書くべき値の型をコンパイラが教えてくれるとい
う機能
https://wiki.haskell.org/GHC/Typed_holes
https://haskell.jp/blog/posts/2017/07-TypedHoles.html
/LugendrePublic/型付き穴
https://downloads.haskell.org/~ghc/8.6.1/docs/html/users_guide/glasgow_exts.html#typed-hole-valid-hole-fits
https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/typed_holes.html#typed-holes
#型システム