[Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)

[wren ng thornton]

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