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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
