Personal tools

GHC/Typed holes

From HaskellWiki

< GHC
Revision as of 15:45, 12 October 2012 by Thoughtpolice (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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.)

Contents

1 Introduction

Lorem ipsum...

2 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

3 Writing 'instance Monad (Free f)'

TODO FIXME

4 Notes on parametricity and Agda

TODO FIXME