On 18/02/07, David Tolpin
The following code compiles: is it a bad thing that it does?
class (Eq a) => Eql a where (=:=) :: a -> a -> Bool x =:= y = x == y
eql :: Eql a => a -> a -> Bool eql x y = x == y
The reason this typechecks: 1) The compiler infers that x and y must have a type which instantiates Eq. 2) Therefore, it infers the type eql :: Eq a => a -> a -> Bool 3) This doesn't match up with the type you specified for eql, though, so we need to check that your specified type is a specialisation of the inferred type (see below for a more thorough explanation). 4) It is; if we know that x has a type which instantiates Eql, then we can prove that this type also instantiates Eq, by the constraint on the class head of Eql. 5) The program is accepted. Step 3 may need more explanation. We can use type signatures to specify a polymorphic type down to a less polymorphic one. For example, if you wrote: id x = x Then the compiler infers id :: a -> a. However, if you only wanted id to work on Ints, then you could write: id :: Int -> Int id x = x This program would still be accepted, because Int -> Int is less polymorphic than a -> a, i.e., you can get from a -> a to Int -> Int by chosing the substitution a = Int. You could also decide that you only wanted id to work on instances of Show: id :: Show s => s -> s id x = x This'd work, again, because you can get from a -> a to Show s => s -> s by chosing the substitution a = Show s => s (note that (Show s => s) -> (Show s => s) is the same as Show s => s -> s). Show s => s -> s is still a polymorphic type, but it's less polymorphic than a -> a (the latter is defined over all types, the former only over types that are instances of Show). HTH. -- -David House, dmhouse@gmail.com