I don't get this line -- <i>"the Haskell compiler will complain because we still miss the definition of the type of the function."</i><p>That's not true. The compiler will give the function the most general type it can infer, which in this case is<p><pre><code> holds :: Eq a => UnionFindElement a -> a -> Bool
</code></pre>
without you needing to specify it in the file.<p>The <i>point</i> of the article is sound - using the interpreter to ask for types is a great way to work (and often leads to surprising realizations which can lead you to generalize and abstract your code), but the <i>reasoning</i> is spurious. Most of the time, you don't need to supply types in Haskell, as the compiler is perfectly capable of figuring them out for itself.
More on how much GHC (and other compilers) can reason about resources (alternatively:infer/thorem prove from type signatures and knowledge about data structures used:<p><a href="http://stackoverflow.com/questions/11725899/is-there-a-theory-that-combines-category-theory-abstract-algebra-and-computation" rel="nofollow">http://stackoverflow.com/questions/11725899/is-there-a-theor...</a><p><a href="http://homepages.inf.ed.ac.uk/bcampbe2/thesis/thesis-final.pdf" rel="nofollow">http://homepages.inf.ed.ac.uk/bcampbe2/thesis/thesis-final.p...</a><p><a href="http://research-repository.st-andrews.ac.uk/bitstream/10023/564/6/Pedro%20B%20Vasconcelos%20PhD%20thesis.pdf" rel="nofollow">http://research-repository.st-andrews.ac.uk/bitstream/10023/...</a><p><a href="http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf" rel="nofollow">http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf</a><p>Also, there's djinn