[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
C T McBride
c.t.mcbride at durham.ac.uk
Mon Aug 9 11:30:11 EDT 2004
On Mon, 9 Aug 2004, Simon Peyton-Jones wrote:
> Closed classes are certainly interesting, but a better way to go in this
> case is to allow the programmer to declear new kinds, as well as new
> types. This is what Tim Sheard's language Omega lets you do, and I'm
> considering adding it to GHC.
> kind HNat = HZero | HSucc HNat
> class HNatC (a::HNat)
> instance HNatC HZero
> instance HNatC n => HNatC (HSucc n)
> At the moment I'm only thinking of parameter-less kind declarations but
> one could easily imagine kind parameters, and soon we'll have kind
> polymorphism.... but one step at a time.
> Any thoughts?
Yes. "Yes please."
This is still in the realm of using type-level proxies for values,
but it's a much more practical fake of dependent types than you can
manage with type classes. It lets you do quite a lot of the handy
indexing that's found in basic dependently typed programs, without
quite crossing the line to full-on value dependency. Of course, I
recommend crossing this line in the long run, but I accept that doing
so might well mess things up for GHC. This is a sensible, plausible
step in the right direction. And I'm sure you'll be able to jack it
up to datakinds parametrized by datakinds, provided all the indices
are in constructor form: the unification apparatus you've already got
for datatype families (or GADTs as you've dubbed them) should do
everything you need, as long as you unify the indices before you
unify the indexed `values'.
What you still don't get is the ability to use datatype families to
reflect on values in order to extend pattern matching, the way James
McKinna and I do in `The view from the left'. But one step at a time.
You also don't get for free the ability to write type-level programs
over these things. If you do add type-level programs over datakinds,
you may find that the unification-in-the-typing-rules style comes
under strain. I'm told that's why the ALF crew retreated from full-on
datatype families, which is why they're not in Cayenne. The Epigram
approach is different: the unification problems are solved internally
to the theory, so you still get the solutions when they're easy, but
the wheels don't come off when they're not.
Even so, you do get quite a long way towards the `static' uses of
dependent types which support n-ary vectors and the like, but where
n isn't supposed to be a run-time value. You'll get `projection
from a vector is exception-free'; you won't get `projection from a
vector returns the thing in that position in the vector'.
So let's have this, and we'll see how many of the programs I've
written in the last 5+ years with these data structures become
Haskell programs. More than a few, I expect.
More information about the Haskell-Cafe