[Next][Index][Thread]
notation decision
After much agitation and Christmas pudding I have decided on
the following notation for systems that assign types to terms:
A TYPE-ASSIGNMENT is an expression of form
M:tau (M a term, tau a type).
A TYPE-ENVIRONMENT (E) is a set of type-assignments
{x-1:tau-1,..., x-n:tau-n}
where x-1,...,x-n are distinct variables.
A TA-FORMULA is
E |-> M:tau (E any type-environment).
To say
E |- M:tau
means that there exists a subset E' of E such that the
formula E' |-> M:tau is provable from the system's rules.
The notation "Environment" has seemed marginally preferable
over "context" because it has marginally fewer other meanings
in current use.
What we really need is a new notation and "Typothesis" fills this
need superbly, but I lack the courage to use it! Perhaps a
younger man...?
Happy New Year from Roger Hindley!
P.S. Thanks very much indeed to everyone who commented
on the type-notation question; the comments helped very much.