cvs commit: fptools/ghc/compiler/typecheck TcMonad.lhs TcSimp lify.lhs fptools/ghc/compiler/types FunDeps.lhs Unify.lhs

[Marcin 'Qrczak' Kowalczyk]

30 Jan 2001 17:11:57 GMT, Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> pisze:

> Perhaps it would make sense to adopt OCaml's treatment of type
> signatures, at least for pattern and result type signatures.  Doing it
> for all signatures (thus eliminating many needs of using pattern
> signatures at all!) is probably too radical...

I was wrong. For plain signatures of let-bound variables it would
be a bad idea, not radical, because a type signature of a variable
completely specifies how I can use the variable. Another change
could be good: type variables from the signature could scope over the
definition, and *that* would be very intuitive for giving signatures
to local definitions which share types with the outer definition.

And BTW, there is an important difference between "C Char b" in a
context (where C has the fundep) and hypothetical (..) in a context.
The former accurately specifies how I can use the variable, even if
the description is not the shortest possible. The latter does not.


But for pattern and result type signatures changing the rules makes
sense.
    f (x::a) = ...
does not mean that x has type "forall a. a" anyway. It should actually
only give the type a name, no matter what it is.

Similarly,
    f (x :: (a,b)) = ...
should unify the appropriate type variable with (,), and give names
to monomorphic arguments of (,) used in the call we are in.

But currently they mean a slightly different thing.
    f (x::a) = ...
means that the compiler must not be able to determine any part of the
structure of its type constructors. It may find class constraints, but
it must not find anything that determines one of its type constructors
exactly, or that it must be "m a" for some types "m :: * -> *" and
"a:: *". If it does find something about this type, it's an error
and I must change the type here to match the amount of the compiler's
knowledge about it, and change all uses of "a" appropriately to the
elaborated type. This is very strange!

This is a negative constraint. Not: it is known to be a pair,
or: it is known to have equality, or: it is known to be the same
as another type, but: it must not be known at this place to be
any particular type constructor, or type application (it may only
have some generic constraints), and: it is different from all other
named type variables. Or rather that it might be the same, but this
place must not force it to be the same, so in principle it could be
different... There is no use of a negative constraint!

I propose to change the meaning of pattern and result type signatures.
They should only constrain the type to the amount of knowledge written,
and give names to types or appropriate parts of types. But they should
not require that the types involved are not determined in more details
somewhere else. It's a type *pattern*, where a type variable can
stand for anything, and means not "forall" anyway, but "don't care".

There is a subtlety and it's not new. As for implicit forall in plain
type signatures, when a type variable is not introduced there, but was
bound by some outer pattern or result type signature or class header,
then it's not a new variable, but similar to a constructor: it matches
only the type bound elsewhere and does not introduce a new name. Such
case is not recognizable at this very place, but one must scan outer
scopes for definitions of the type variables involved. Fortunately
the problem is not as big as for value constructors in SML, because
bound type variables can only be introduced locally, not imported
nor found in other toplevel definitions. We can live with it, IMHO
the results are more intuitive than for any alternative.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK