[Haskell-cafe] \Statically checked binomail heaps?

[Wouter Swierstra]

Hi Maciej,

> insTree t [] = [t]
> insTree t ts@(t':ts')
>  | rank t < rank t' = t : ts
>  | otherwise = insTree (link t t') ts'

In a way, it's unsurprising that this is where your code breaks. What  
you're doing here is using a boolean guard to determine where to  
insert. The problem is that ghc's type checker doesn't learn anything  
from these boolean guards. In contrast to pattern matching on a GADT,  
you can always exchange the two branches of an if-than-else without  
breaking type correctness. To get the code to work the type checker  
needs learn something about the ranks of t and t' after comparing them.

> Have anyone an idea how make this code working?

Use a different language. In particular, you might want to have a look  
at Agda - a programming language and proof assistand based on  
dependent types that has a very similar look-and-feel to Haskell. If  
you're interested, you may want to have a look at similar developments  
by some of our students at Chalmers:

   http://web.student.chalmers.se/groups/datx02-dtp/

They've given verified implementations in Agda of some fairly advanced  
data structures.

Hope this helps,

   Wouter

PS - There may be a way around this by writing even more type-level  
programs in Haskell, basically reflecting (<) on the type-level and  
doing some really hard work to relate the type level numbers to the  
value level numbers. Brace yourself for a world of pain.