Konstantin Laufer <[EMAIL PROTECTED]> writes:
| Consider the following recursive function binding:
|
| > f [] = 0::Int
| > f (x:xs) = 1 + f([]::[Int]) + f([]::[Bool]) + f xs
|
| This binding is ill-typed since f is used in two different instances
| of its polymorphic-to-be type. Indeed, the above declaration is
| rejected by hbc, ghc, and gofer.
That's correct. However, I think that you'll find hbc will accept it
if you provide an explicit type signature:
f :: [a] -> Int
(As far as I know, the Miranda type system will do the same thing.)
This is an extension of the current definition of Haskell and, I
imagine, something that might one day be considered for inclusion
in a future version of the language. But we should probably think
carefully about the interaction with type classes. For example,
the following innocent looking program:
g :: Eq a => a -> Bool
g x = x==x || g [x]
could be compiled under this extension, but evaluating the expression
g True in an implementation based on dictionaries would require
the construction of an infinite sequence of dictionaries for
instances:
Eq Bool, Eq [Bool], Eq [[Bool]], ...
So this expression cannot be evaluated in constant space. (Actually,
that is true anyway for this example since the argument to g is
also increasing without bounds. I wonder if there are examples
where an apparent constant-space computation actually requires
unbounded storage because of dictionaries?)
I have done some work to experiment with an implementation of type
classes that does not use dictionary values at run-time. Definitions
like the above are simple of example that cannot be dealt with using
these methods.
| However, the restriction can be overcome by declaring a class
| containing the function. The following program compiles and runs
| without complaints under all three:
|
| > class F a where
| > f :: a -> Int
| >
| > instance F [a] where
| > f [] = 0::Int
| > f (x:xs) = 1 + f([]::[Int]) + f([]::[Bool]) + f xs
|
| This is fine from a type inference point of view since f is declared
| and given a polymorphic type at the point where the class is defined.
Yes, the thing that makes this work is the combination of explicit
type information and the indirect recursion through the type class
mechanism.
For this example, type classes don't provide as good a solution as
simple explicit typing. For example, it gives:
(\x y -> if x==y then f x else f y) :: (Eq a, F a) => a -> a -> Bool
Not a major problem, but the type is a little misleading since the
term on the left can only be applied to lists. If you could ensure
that no user would ever define an instance of F for another type
then you could reduce the type to Eq a => [a] -> [a] -> Bool. That
isn't possible if you want to be able to extend standard Haskell
classes with definitions as new modules are added to a program.
| There are some useful applications for this, particularly in
| connection with existential types. Any thoughts or comments? Is this
| a well-known technique?
Here's another example that might be of interest (I'm afraid it uses
constructor classes rather than standard type classes though ...)
Consider the following two datatype definitions:
data X a = XTag [X a]
data Y a = YTag (Y [a])
We can define `map' functions for each of these datatypes, analogous
to the map function on lists:
instance Functor X where map f (XTag xs) = XTag (map (map f) xs)
instance Functor Y where map f (YTag xs) = YTag (map (map f) xs)
The first map function can be expressed in the standard Hindley-Milner
type system, but the second cannot. The constructor classes make
it possible to use the definition for essentially the same reasons
as the example above.
Hope these comments are the kind of thing you were looking for!
All the best,
Mark
