On 27-May-1998, Mr. Grumpy <[EMAIL PROTECTED]> wrote:
> -------------------------
> Fergus Hendersons Example
> -------------------------
> > Note that the different types can lead to different semantics.
> > Consider the following code, which is similar to the code above:
> >
> > foo :: (Int -> Float) -> Either Int Char -> Either Float Char
> > foo f (Left a) = Left (f a)
> > foo _ r@(Right c) = classmethod r
> >
> > class Demo t where
> > classmethod :: t -> Either Float Char
> >
> > instance Demo Either Int Char where
> > classmethod = m1
> >
> > instance Demo Either Float Char where
> > classmethod = m2
> >
> > Here `r' has type `Either Int Char', not `Either a Char',
> > and this determines which class method is called.
> > Note that writing
> >
> > foo _ r@(Right c) = classmethod (Right c)
> >
> > would result in compile error (or worse) due to an uninstantiated
> > type variable.
>
> I see what you mean. Sorry I was so thick earlier. I don't know if
> this is a real problem (I haven't actually tried writing any Haskell
> code like this), but if it is it seems to me that the typing of
> as patterns (or of variables known to be bound to a particular pattern)
> isn't really the cause of this ambiguity. The problem would occur in
> any expression of form 'classmethod (Right c)', as you point out.
Yes. My point is that Haskell makes types part of the semantics.
That means you can't diddle with the types without affecting the semantics.
The proposed change would generalize some types. Making things
more polymorphic increases the likelyhood of ambiguities.
> Can we rely on compilers to spot this kind of error
> at compile time? I hope so, but maybe the 'or worse' option will be
> invoked instead.
It is easy for a compiler to spot unbound type variables at compile time.
I just wasn't sure off-hand what current Haskell implementations do
or what the Haskell report says they are supposed to do.
It's a little bit more difficult for a compiler to figure out
when unbound type variables will actually cause trouble.
More on this below...
> I see that paragraph 4.3.2 of the Haskell 1.4 report states that..
> "A type may not be declared as an instance of a particular class more
> than once in a program."
> ... Does the above constraint
> apply to algebraic types with or without their arguments 'instantiated'
> (or should I say 'bound'?). If the latter is assumed, then the example
> above is illegal, but I've probably got this wrong.
I don't know off-hand which interpretation is correct.
But you can construct a similar example demonstrating the same
thing which doesn't rely on the former interpretation.
> > The type of a polymorphic expression such as `(Right c)' is, as is
> > always the case in Haskell, determined by the context in which it occurs.
>
> But what happens if the context doesn't provide sufficient information
> to instantiate the 'uninstantiated type variable'?
Then, if the type is needed, you're going to be in trouble.
Sometimes the type isn't needed, in that case you'll be OK.
It can be difficult for a compiler to distinguish
these two cases at compile time, however.
Sometimes a function may have a type such as
f :: Foo a => [a] -> Bar
If the class `Foo t' has a method that can construct a
`t' from things other than other `t's, then a call to
`f' with the type variable `a' unbound could lead
to a run-time error. But if the class `Foo t'
is a class like `Ord' which has no such method,
then such calls are safe. I'm not sure how difficult
it is for a compiler to distinguish these two cases.
> It seems to me that
> the more sensible approach is to say that if the type of a constructor C
> is known (as it always will be) and the type of a variable x is also
> known, then this is sufficient information to determine the type of (C x)
> whether it appears in an expression or a pattern. If that leaves a type
> variable unbound, then so what?
Then if the type is needed, for example for dispatching to the right
class method, then you have what in the field of logic programming
we call a "mode error".
> ... why is an unbound type variable generally an error?
Unbound type variables can lead to runtime errors.
A strong type system is supposed to prevent runtime errors.
Thus it makes sense to disallow anything that might
result in an attempt to access an unbound type.
> Btw, is an 'uninstantiated' type variable the same thing as an 'unbound'
> type variable?
Yes.
> What is the ultimate purpose of type checking a program? The answer has
> to be, to avoid run-time errors. Beyond this, the type system seems to
> serve no purpose and so should not reject definitions such as that
> above, in an ideal world.
The Haskell type system is used for much more than just avoiding run-time
errors. In particular, the Haskell system of type classes means that
types are part of the semantics.
Some people have argued against this, arguing for a system where
types do not affect the operational semantics, only the legality.
But this leads to a less expressive language (for example,
you can't have a polymorphic `read').
> ---------------------------------------------
> Are parameterised modules no longer en vogue?
> ---------------------------------------------
...
> For example, the 'Ord' class has 'compare' as a method. I find I often
> wish to order (and therefore compare) data according to different
> criteria at different times. So all my sorting/searching/set-manipulation
> functions are written to take the compare function as an argument, and not
> rely on Ad Hoc polymorphism to select the appropriate function. This has the
> added advantage that a compare function can be given the more general
> type :: a -> b -> Ordering (when it appears as an argument). In other words,
> as a general rule, I completely disregard Haskell's class system when ever
> possible. If this makes me a naive user, then I must plead guilty.
You shouldn't disregard it "when ever possible";
you should only disregard it in cases where you will
often want to apply different methods to the same data type.
In many situations, the methods you want are usually fixed for each type,
and in those sort of situations, it makes sense to use type classes.
> I suppose I could probably get around this problem by by making different
> types using newtype, but I this would no doubt cause other complications
> elsewhere.
Yes, perhaps. See Alistair Reid's proposal for newtype typecasts
to avoid some of these complications.
> A case of the cure being worse than the disease I think. A
> system of parameterised modules would be of considerable assistance (to
> Ad Hoc sceptics like me at least).
I believe there have been some proposals for "first class modules"
or something along those lines.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
