[Haskell-cafe] \Statically checked binomail heaps?

Wouter Swierstra wss at cs.nott.ac.uk
Mon Oct 19 11:07:26 EDT 2009

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:


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

Hope this helps,


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.

More information about the Haskell-Cafe mailing list