GHC/Typed holes
< GHC
Jump to navigation
Jump to search
Revision as of 15:45, 12 October 2012 by Thoughtpolice (talk | contribs) (New page: Type system <span style='font-size: x-large; font-weight: bold'>Type holes in GHC.</span> Type holes are a powerful feature in GHC that is inspired by [http://wiki.portal...)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
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.)
Introduction
Lorem ipsum...
Motivating example
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)'
TODO FIXME
Notes on parametricity and Agda
TODO FIXME