[Haskell-cafe] \Statically checked binomail heaps?
wss at cs.nott.ac.uk
Mon Oct 19 11:07:26 EDT 2009
> 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
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