12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 23:36, 25 March 2009
, 23:36, 25 March 2009→Commentary Note 1: markup
===Commentary Note 1===
===Commentary Note 1===
I think it's best to begin with a few simple observations, as I frequently find it necessary to return to the basics again and again, even if I take a different path each time.
I think it's best to begin with a few simple observations,
as I frequently find it necessary to return to the basics
again and again, even if I take a different path each time.
Observation 1
;Observation 1
: If we have the information that an element <math>x\!</math> is constrained to be of the type <math>X\!</math>
: and we have the information that a function <math>f\!</math> is constrained to be of the type <math>X \to Y</math>
: then we have the information that the element <math>f(x)\!</math> is constrained to be of the type <math>Y.\!</math>
We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form:
We can abbreviate this inference, that operates on
two pieces of information to produce another piece
of information, in the following conventional form:
<pre>
x : X
x : X
f : X -> Y
f : X -> Y