[Prev][Next][Index][Thread]
terminology
Albert recently raised a question of terminology about
typing statements and typing derivations. Here is his
message to me:
By the way, I noticed in your paper with Harper you use the terminology ``a
typing'' for an assertion ``Gamma |- M: sigma''. I have been using the
terminolgy ``typing'' to refer to the DERIVATION of the assertion in
question, or what amounts to the same thing in most (not all) type systems,
the set of assertions, ``Gamma_i|-M_i:sigma_i'' for all the subterms M-i of
M. Hindley talks about principal ``typINGS'' as OPPOSED TO ``types'' in a
recent preprint he sent me; I assumed he was using my terminolgy, but I
haven't checked.
I think the issue is clouded by the difference between
natural deduction and sequent calculus formulations of
type derivation systems. I propose the following:
an assertion ``Gamma |- M: sigma'' should be called a
TYPING JUDGEMENT or TYPE ASSERTION when used as part of
a sequent calculus (i.e., in writiing this, we do not
mean a derivation of M:sigma from undischarged hypotheses
Gamma)
a derivation of a type assertions should be called a
TYPE DERIVATION
One terminological question I have is what to call a pair
<Gamma, sigma>. In an ML like system, the types of an open
term M are characterized using pairs <Gamma, sigma> such that
Gamma |- M:sigma are derivable. Therefore, it seems most natural
to me to talk about the "most general" or "principal" pair
<Gamma, sigma>. In a survey article in preparation, I had been
calling these "typings," tp distinguish them from type expressions
(e.g. sigma), but this conflicts with Alberts comments above.
Any suggestions?