Difference between revisions of "GHC/Typed holes"
< GHC
Jump to navigation
Jump to search
(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...) |
(No difference)
|
Revision as of 15:45, 12 October 2012
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