Type holes in GHC.
Type holes are a powerful feature in GHC that is inspired by Agda. But what are type holes, and how do they help us write code?
(This page was taken from a 'tutorial' I wrote of this feature on Reddit.)
Let us consider the definition of a Free monad:
data Free f a = Pure a | Free (f (Free f a))
A free monad coupled with an
Writing 'instance Monad (Free f)'
Notes on parametricity and Agda