Hi Mark,
> The example that prompted this discussion, however, a type annotation,
> and not a type signature declaration. Compare:
>
> foo :: Double with foo = 23 :: Double
> foo = 23
>
> Hope this clarifies things!
Thank you. I should have read more carefully.
Miranda doesn't have type annotations, so I didn't have to implement that.
Nonetheless I think that starting type checking with a type annotation, if it
exists, is a good idea to obtain better error messages.
The type checker for Miranda that I implemented was actually part of a third
year project at the University of Kent, under the supervison of Simon Thompson.
The aim was a tool that helps the user to understand type errors. Well, at that
time I did not know much about type checking and now I know that my type checker
handled locally quantified type variables incorrectly. The whole tool was quite
buggy. The central idea of the project was that you could ask the tool for types
although the input was not type correct (unlike Gofer/Hugs). The tool would type
check a whole project and give a list of error message. The main feature was
that you could interactively mark any subexpression in the project and ask for
its type. I also thought about an order of type checking which would give better
error message, but I believe that wasn't very successful.
We actually considered using Gofer instead of Miranda, modifying the Gofer
system. However, your design document for Gofer didn't exist at the time and
there was the additional problem of type classes.
> Your comment about giving smaller strongly connected components is
> interesting. I noticed the same thing a couple of years ago, and the
> Hugs type checker uses this observation to type check some programs
> that might otherwise be rejected. I'd be interested to hear if you
> know of any other systems that do the same.
I'm sorry, I don't know. I don't even know how the Miranda type checker works.
Although we were at the source of information about Miranda, we didn't get
anything about the internals of the system. Always when the Miranda manual was
vague or didn't define anything, I just tried examples with the Miranda system
(even the manual and the system were inconsistent). So, because text books on
type checking don't say anything about signatures, I thought up two alternative
algorithms and tested Miranda, which one it seemed to use (maybe there are more
alternatives?).
Actually, I don't understand how a type checker without polymorphic recursion
could ever have been implemented. Type signatures provided by the user can
restrict a type. I'd imagine it to be quite complicated to infer a type first
and then restrict it according to the signature. Also, I believe that it is the
most natural thing to use given type signatures to obtain smaller strongly
connected components.
By the way, a year ago there was some talk that you would write a
simple-to-understand type checker for Haskell which would define the Haskell
type system. Did you do something like that? It's rather sad, that the Haskell
report does not define the type system (especially the version of the class
system it uses).
Olaf
--
OLAF CHITIL, Lehrstuhl fuer Informatik II, RWTH Aachen, 52056 Aachen, Germany
Tel: (+49/0)241/80-21212; Fax: (+49/0)241/8888-217
URL: http://www-i2.informatik.rwth-aachen.de/~chitil/
