[TYPES] Historical question: origin of the ":" symbol

Uday S Reddy u.s.reddy at cs.bham.ac.uk
Tue May 27 12:23:09 EDT 2008


Edsko de Vries writes:

> Can anyone refer me to a discussion of the history of the symbols used
> in type theory? In particular, the origin of the ":" symbol? I seem to
> recall reading somewhere that is derived from \epsilon, which in turn is
> the first letter of 'esti' (to be), but I cannot remember where I read
> this -- might have made it up myself :)

I always thought the notation of f: A -> B for function types must
have been the origin of the ":" symbol.  Does that predate set theory?

Cheers,
Uday


More information about the Types-list mailing list