Jake McArthur wrote:
On 06/03/2010 10:14 AM, Gabriel Riba wrote:
No need for runtime errors or exception control
hd :: List!Cons a -> a
hd (Cons x _) = x
This is already doable using GADTs:
data Z
data S n
data List a n where
Nil :: List a Z
Cons :: a -> List a n -> List a (S n)
hd :: List a (S n) -> a
hd (Cons x _) = x
tl :: List a (S n) -> List a n
tl (Cons _ xs) = xs
Sure, it is the whipping boy of dependent types afterall. However,
* Haskell's standard lists (and Maybe, Either,...) aren't GADTs,
* last I heard GADTs are still a ways off from being accepted into haskell',
* and, given that this is the whipping boy of dependent types, you may
be surprised to learn that pushing the proofs of correctness through for
the standard library of list functions is much harder than it may at
first appear. Which is why, apparently, there is no standard library for
length-indexed lists in Coq.[1]
But more to the point, this proposal is different. Gabriel is advocating
for a form of refinement types (aka weak-sigma types), not for type
families. This is something I've advocated for in the past (under the
name of "difference types")[2] and am still an avid supporter of-- i.e.,
I'm willing to contribute to the research and implementation for it,
given a collaborator familiar with the GHC code base and given
sufficient community interest.
The reason why length-indexed lists (and other type families) are
surprisingly difficult to work with is because of the need to manipulate
the indices in every library function. With refinement types predicated
on the head constructor of a value, however, there is no need to
maintain this information throughout all functions. You can always get
the proof you need exactly when you need it by performing case analysis.
The benefit of adding this to the type system is that (a) callees can
guarantee that the necessary checks have already been done, thereby
improving both correctness and efficiency, and (b) it opens the door for
the possibility of moving the witnessing case analysis further away from
the use site of the proof.
While #b in full generality will ultimately lead to things like type
families, there are still a number of important differences. Perhaps
foremost is that you needn't define the proof index at the same point
where you define the datatype. This is particularly important for adding
post-hoc annotations to standard types like lists, Maybe, Either, etc.
And a corollary to this is that you needn't settle on a single index for
an entire programming community, nor do you impose the cost of multiple
indices on users who don't care about them.
In short, there's no reason why the equality proofs generated by case
analysis should be limited to type equivalences of GADT indices. Value
equivalences for ADTs are important too.
[1] Though I'm working on one:
http://community.haskell.org/~wren/coq/vecs/docs/toc.html
[2] http://winterkoninkje.livejournal.com/56979.html
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
