Haskell TypeCast type class

Question

I've run into a type class called TypeCast in Haskell in a few different places.

It's rather cryptic, and I can't seem to fully parse it.

class TypeCast   a b   | a -> b, b -> a     where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t -> a -> b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t -> a -> b

instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x

http://okmij.org/ftp/Haskell/typecast.html gives a helpful but perfunctory comment on this code. For more information, that page points me to http://homepages.cwi.nl/~ralf/HList/paper.pdf which is a broken link.

I see that TypeCast is a class that allows you to cast from one type to another, but I don't see why we need TypeCast' and TypeCast''.

It looks like all this code does is allow you to cast a type to itself. In some of the sample code I've seen, I tried replacing it with this:

class TypeCast a b | a -> b, b -> a where typeCast :: a -> b
instance TypeCast a a where typeCast a = a

and the samples still worked. The samples I've been looking at are mostly from that first link.

I was wondering if someone could explain what the six lines are for.

Answer 1

What is TypeCast actually for?

It isn't used for retrieving type information about existential types (that would break the type system, so it is impossible). To understand TypeCast, we first have to understand some particular details about the haskell type system. Consider the following motivating example:

data TTrue
data TFalse

class TypeEq a b c | a b -> c

instance TypeEq x x TTrue
instance TypeEq x y TFalse 

The goal here is to have a boolean flag - on the type level - which tells you if two types are equal. You can use ~ for type equivalence - but this only gives you failure on type in equivalence (ie Int ~ Bool doesn't compile as opposed to TypeEq Int Bool r will give r ~ TFalse as the inferred type). However, this doesn't compile - the functional dependencies conflict. The reason is simple - x x is just an instantiation of x y (ie x ~ y => x y == x x), so according to the rules of fundeps (see the docs for full details of the rules) , the two instances must have the same value for c (or the two values must be insantiations of one another - which they aren't).

The TypeEq class exists in the HList library - lets take a look how it is implemented:

class HBool b => TypeEq x y b | x y -> b
instance TypeEq x x HTrue
instance (HBool b, TypeCast HFalse b) => TypeEq x y b
-- instance TypeEq x y HFalse -- would violate functional dependency

Naturally these instance don't conflict - HTrue is an instantiation of b. But wait! Doesn't TypeCast HFalse b imply that b must be HFalse? Yes, it does, but the compiler does not check the class instance constraint when attempting to resolve fundep conflicts. This is the key 'feature' which allows this class to exist. As a brief note - the two instances still overlap. But with -XUndecidableInstances -XOverlappingInstances, the compiler will choose the first instance preferentially, due to the fact that the first instance is more 'specific' (in this case, that means it has at most 2 unique types - x and HTrue, while the other instance has at most 3). You can find the full set of rules that UndecidableInstances uses in the docs.

Why is TypeCast written the way it is?

If you look in the source for HList, there are multiple implementations of TypeCast. One implementation is:

instance TypeCast x x

The straightforward instance one would assume will work. Nope! From the comments in the file containing the above definition:

   A generic implementation of type cast. For this implementation to
   work, we need to import it at a higher level in the module hierarchy
   than all clients of the class. Otherwise, type simplification will
   inline TypeCast x y, which implies compile-time unification of x and y.

That is, the type simplifier (whose job it is to remove uses of type synonyms and constant class constraints) will see that x ~ y in TypeCast x x since that is the only instance that matches, but only in certain situations. Since code that behaves differently in different cases is 'Very Bad', the authors of HList have a second implementation, the one in your original post. Lets take a look:

class TypeCast     a b |   a -> b,   b -> a   
class TypeCast'  t a b | t a -> b, t b -> a 
class TypeCast'' t a b | t a -> b, t b -> a 

instance TypeCast'  () a b => TypeCast    a b 
instance TypeCast''  t a b => TypeCast' t a b 
instance TypeCast'' () a a 

In this case, TypeCast x y can never be simplified without looking at the class constraint (which the simplifier will not do!); there is no instance head which can imply x ~ y.

However, we still need to assert that x ~ y at some point in time - so we do it with more classes! The only way we can know a ~ b in TypeCast a b is if TypeCast () a b implies a ~ b. This is only the case if TypeCast'' () a b implies a ~ b, which it does.

I can't give you the whole story unfortunatley; I don't know why

instance TypeCast' () a b => TypeCast a b 
instance TypeCast' () a a

doesn't suffice (it works - I don't know why it wouldn't be used). I suspect it has something to do with error messages. I'm sure you could track down Oleg and ask him!

Answer 2

The HList paper was published in the proceedings of the Haskell Workshop 2004, and so is available from the ACM DL and other archives. Alas, the explanation in the published version is abbreviated for the lack of space. For full explanation, please see the expanded version of the paper published as a Technical Report, which is available at http://okmij.org/ftp/Haskell/HList-ext.pdf (The CWI link is indeed no longer valid since Ralf left CWI long time ago.) Please see Appendix D in that TR for the explanation of TypeCast.

In the latest GHC, instead of TypeCast x y constraint you can write x ~ y. There is no corresponding typeCast method: it is no longer necessary. When you write the x ~ y constraint, GHC synthesizes something like typeCast (called coercion) automatically and behind the scenes.

Asking me a question directly in a e-mail message usually results in a much faster reply.