[Haskell-cafe] Re: Typeclass vs. Prolog programming

[oleg at pobox.com]

I previously wrote:
> The typechecker commits to the instance
> and adds to the current constraints
>         TypeCast x Int, Ord Bool, Eq Bool
> The latter two are obviously satisfied and so discharged. The former
> leads to the substitution {x->Int}.

I should have been more precise and said: 
	The former _eventually_ leads to the substitution {x->Int}.

Your analysis is right on the mark. That's exactly how I think of
TypeCast.


> This is all very beautiful, but it's a little annoying that the
> cornerstone "silver bullet" TypeCast has to be defined in a way that
> fools the typechecker into doing the right thing in spite of itself.

One of the drafts of the HList paper, when describing TypeCast,
literally had a phrase about `fooling the typechecker'...

Well, it seems things like TypeCast were not envisioned by the
Founding Fathers. In this respect, the story of C++ templates come to
mind. My feeling is that we're still discovering the capabilities of
the Haskell typechecker and the right abstractions. We should view
TypeCast as an ungainly _encoding_ of a simple abstraction, or just as
a tool for implementing type-level typecase and local improvement
rules. When the right abstraction emerges (and perhaps it already has:
CHR), GHC might implement it directly. Until then, we can use the
encoding...