Sorry to raise this old chestnut again, but my work dragged me away
before I had time to properly digest and respond to other peoples
messages on this subject. But now I'm back and I've spent some more
time cogitating type systems generally and the Haskell type system in
particular, and I'm more confused than ever. This is, of course, due
entirely to my naivete :-)
I've taken some time to jot down a few features about the Haskell type
system that seem odd/problematic to me. I don't expect any real answers
(I'm not that naive), I just wonder if anybody else has anything
interesting to say on this subject.
I have found that as long as I use common sense and intuition when
thinking about types I generally don't get 'bitten' by these problems.
But sometimes I do, and I then have to try to work out the least horrible
modifications I need to make to my programs to them to compile. In a
language that has such a complex and idiosyncratic type system as Haskell's
seems to be, this isn't always so straight forward. I'm sorry to say that,
I'm sure there are good reasons for things being the way they are, but
they're not at all obvious to me.
Part of the problem I have in understanding these issues is reliance on the
Haskell 1.4 report which often uses jargon that may be part of the everyday
vocabulary of Computer Scientists, but is probably meaningless to most
potential Haskell users. I believe that there are some textbooks being
written about Haskell at present (but lack of definition of Standard Haskell
is delaying publication). I promise to buy one of these as soon as one becomes
available. In the mean time, perhaps the authors could take some time to
explain all these issues in more detail, if they haven't already.
Functional programming is, on the whole, pretty simple. Unfortunately the
same can't be said of the type system. (Well, it doesn't seem simple to
me, and I suspect that I'm not alone in this.)
-------------
SLPJ's advise
-------------
> On Mon 11 May, Simon L Peyton Jones wrote:
> > My advice would be: write clear code, and let the compiler do the
> > CSE.
>
> I take it you mean avoid using 'as patterns'.
>
> > If it doesn't, complain to the compiler writers. You have
> > good reason to believe that it should.
Humble apologies, I feel a bit guilty about attributing a meaning to SLPJ's
words which he obviously didn't intend. I believe the correct interpretation
of this advise is that given a good compiler, then use/non-use of 'as patterns'
is merely a question of style, it shouldn't influence run-time behaviour.
-------------------------
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.
I already felt slightly uneasy about 'Ad Hoc' polymorphism, now I'm
even more worried. 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.
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."
The report then starts talking about constraints & 'superclass contexts'..
I'm afraid I don't understand any of this. 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.
> 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'? 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? Isn't that the whole point of the
blah->blah notation?
> Not true! Performing the substitution can result in type errors
> (unbound type variables) in cases where the 'as pattern' is valid.
But why is an unbound type variable generally an error? I can see
the problems it has caused the class system in the above example, but
is this the real cause of the problem? No, IMHO (see I'm learning).
Btw, is an 'uninstantiated' type variable the same thing as an 'unbound'
type variable? Probably not, but I'd like to know the difference.
------------------------------
The evil unbound type variable
------------------------------
Hugs 1.4 (and I presume other Haskell implementations) accepts the
following code..
silly = let e=[] in (1:e,'a':e,e:e)
and reports its type to be..
silly :: ([Int],[Char],[[a]])
It appears that, as far as expressions are concerned, there is
no need create separate []'s to cope with all the 'different types' of
empty list there might be. This is just as it should be, IMHO. But
treating patterns or arguments of function definitions differently still
seems like an anomaly to me. I won't call it a 'bug', as the work around
is pretty trivial and should result is zero run-time penalty, provided
the compiler performs 'type illegal' CSE optimisation.
-----------------
Polymorphic Data?
-----------------
Most textbooks about functional programming that I've read discuss
polymorphic functions and the Hindley-Milner type system (which I
believe is the basis of the Haskell type system). I don't recall them
ever discussing polymorphic data, and I'm not sure whether or not the
Hindley-Milner system allows this possibility or not. If I look at the
way Haskell treats expressions I'm inclined to say yes, but if I look
at the way patterns are treated it appears that the answer is no.
It seems to me that assigning values such as [] the type [a], is just
'natures way' of expressing the fact that [] is a genuinely polymorphic
value.
-----------------------
Koen Claessen's example
-----------------------
> It is not only Either instances who suffer from this. Consider the
> following definition of "map", which could be made by a naive user:
>
> map :: (a -> b) -> [a] -> [b]
> map f (x:xs) = f x : map f xs
> map f xs = xs
>
> Same problem here.
An interesting point. A couple thoughts that spring to mind when I look at
this example are..
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.
This example also makes me think that pattern match compilation should
be done before type checking. This probably isn't the case with most
(if not all) compilers. I suppose one problem with doing this is that
it might be more difficult to generate error messages which relate to
the actual source program, rather than some transformed version of it.
-------------------------------------
What do type variables actually mean?
-------------------------------------
Not using explicit universal quantifiers simplifies type expressions,
but also causes a few problems IMHO.
For example..
Why is the following type synonym illegal?
type ListOp = [a]->[a]
Hugs seems to insist that in type synonyms (and algebraic data type
declarations also) all type variables are parameters of the type.
What I really want is to be able to say..
type ListOp = forall a. [a]->[a]
which isn't the same as..
type ListOp a = [a]->[a]
If (polymorphic) functions are supposed to be 'first class' then shouldn't
this be every bit as legal as..
type IntOp = Int->Int
Wouldn't a reasonable convention be to treat any type variables that
were not arguments as being universally quantified? Obviously if one
were to allow this then precautions to avoid name capture problems
(when the synonym is expanded) are necessary, but that shouldn't cause
any difficulty.
or..
Allow explicit universal quantification sometimes, and adopt the
convention that unquantified variables should be taken from some kind
of type 'environment' (such as type arguments in a type/data declaration
or top level type variables in local type signatures).
---------------------
Polymorphic Recursion
---------------------
Is this an example of Polymorphic recursion..?
data Alts a b = Last | Alt a (Alts b a)
mapAlts fa fb Last = Last
mapAlts fa fb (Alt a alts) = Alt (fa a) (mapAlts fb fa alts)
the principal type of this function is..
mapAlts :: (a -> c) -> (b -> d) -> Alts a b -> Alts c d
but left to itself Hugs 1.4 infers a type of..
mapAlts :: (a -> b) -> (a -> b) -> Alts a a -> Alts b b
But at least you can correct this sort of situation in top level
declarations with a type signature.
Is correctly inferring principal types really so hard? This would be a
pretty trivial problem were it not for two issues that I can think of..
1- It seems that local type signatures are occasionally necessary but
often not possible. An unfortunate contradiction IMHO.
2- I thought one of the design goals of Haskell was to produce a language
that was suitable as a target for code synthesis tools, and that type
signatures were supposed to be an 'optional extra' for human programmers.
(Maybe I'm mistaken, its one of those things I seem to remember reading
somewhere but, of course, I've forgotten where.) Since it would appear
that type inference alone cannot be relied upon, it is necessary to
have some means of completely disabling type checking if Haskell is
to be used this way. (I suppose this would necessarily imply ditching
Ad Hoc polymorphism also ... heresy!)
---------------------------------------------
Are parameterised modules no longer en vogue?
---------------------------------------------
I get the impression that the source of a lot of debate & difficulty
in the Haskell world is the use of Ad Hoc polymorphism. Of course
its far to late to change this now. Any language devoid of this feature
just wouldn't be Haskell.
Its nice not to have to explicitly pass 'class methods' as arguments to
functions, and its nice not to have to re-write ones library of matrix ops
to cope with every different number representation. But its not clear to
me what advantages Ad Hoc polymorphism has over parameterised modules, or
ML style signatures and functors.
The restriction that a particular type cannot be declared an instance of
a particular class more than once seems necessary and sensible. (The whole
system would be un workable otherwise). But it's also a bit of a nuisance.
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.
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. 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).
But I shouldn't knock Ad Hoc polymorphism too hard. Even I can see the
advantages of formalising the implicit overloading of common arithmetic
operators that just about all languages support. But you can have too
much of a good thing.
---------------------------------------------------------------
The monomorpism restriction (Para. 4.5.5 of the Haskell report)
---------------------------------------------------------------
Well this one has got me completely baffled. Para. 10.3 of the
tutorial doesn't enlighten me much either.
Rule 1..
I think I can see why the expression len (in the example given)
might unnecessarily be computed twice, given a not very smart compiler,
or an environment with insufficient information to determine that
the same genericLength function should be used. I don't understand
why supplying a type signature for len will inevitably result in the
len being evaluated twice, unless this is some kind of subtle instruction
to the compiler to do this. If this is the case then I don't find the
idea very appealing. Having type signatures affect the behaviour of
the type checker is one thing, but I don't think many users (certainly
this user) would expect the presence or absence of type signatures
to have any effect on run time behaviour.
Rule 2..
"The type of a variable exported from a module must be completely
polymorphic; that is, it must not have any free type variables..."
So much for my theory that the presence of unbound (I.E. free) type
variables is 'natures way' of telling us that a value is polymorphic.
I'm not sure if my grasp of the fundamental concepts behind type checking
is really so weak, or is just the words that I don't understand.
Given that 'unbound' means the same thing as 'free', or so I believe, then
does 'free' in this context imply no quantification, or universal
quantification?
------------------------------
I think this message has got long enough. It seems that Haskells type system
and Ad Hoc polymorphism is my Waterloo. I'm beginning to think that I would
willingly sacrifice this in exchange for a type system I could understand.
My one crumb of comfort is that I'm not alone in my confusion. If one
takes the trouble to browse the 'Questions on the Table' page of the
Standard Haskell website it is apparent that debates about the Haskell
type system dominate all other issues. If such eminent Haskellians have
so many problems understanding and reaching agreement on how the type
system should work, then what hope is there for the rest of us naive users?
(It's also quite interesting to see how often the 'N' word occurs in these
discussions.)
Regards
--
Mr. Grumpy (a.k.a. Adrian Hey)
