% You can apply any constructor e1 with a kind (k1 -> k2), be it a
% variable, constant, or application, to any other constructor e2 of
% kind k1, forming a (possibly partial) application (e1 e2), as described
% on pages 31--32 of the (draft) report. As you say, this permits currying.
Yes, but these pages don't say anything about the restriction
w.r.t. type synonyms, and I think that's the place where this should
be stated -- it's a restriction on type( expression)s, not a
restriction on type synonym declarations.
(And what about type identifiers coming from other modules;
can we curry them iff they weren't originally type synonyms?)
I would suggest to solve this on the level of kinds, e.g.
distinguish the kinds k1->k2 and k1=>k2; the latter would be the one
that has always to be fully applied, and kind inference would always
infer the former. Type application (f a) would allow both kinds
k1->k2 and k1=>k2 as the kind for f.
The kind of a type synonym T a1...an = rhs would be k1=>...=>kn=>k, etc.
(Strictly, this gives more kinds then we need and want,
but this would only matter if we had explicit kind declarations.)
Considering my original problem about the interaction between type
inference and kind inference, there was a little misunderstanding with
what I meant by types (\x.x->x) etc.
Sure, these beasts don't exist in the syntax, but I was talking about
the (static) semantics --- there's conceptually a difference between
types and type expressions, e.g. () and (()) are different type
expressions but denote the same type. In the static semantics such a
thing as (\x.x->x) does exist, it's simply the semantic value the type
constructor T of the synonym
type T x = x -> x
is bound to.
I can elaborate a bit with the earlier example:
data App f a = A (f a)
value = A ()
As explained by Lennart and Mark, the value declaration does not
type-check, because e.g. App (\f.f) () would violate the
no-partial-applications-of-type-synonyms principle ((\f.f) would
correspond to a type synonym).
However, there is no partial application of a type synonym
in the above program TEXT, it only exists "semantically" when one
tries to infer a type for value.
The restriction on the currying of type synonyms is therefore
a semantic restriction on types, not just a syntactic restriction on
type expressions.
I don't think this is obvious.
Having said all that, I'm probably a bit spoilt by the style of the
SML definition which I know quite well.
Stefan Kahrs
