Jon Awbrey
Registered: Feb 2004
Posts: 551 |
Propositions As Types
PAT. Note B1
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
- If we have the information that an element x
is constrained to be of the type X
and we have the information that a function f
is constrained to be of the type X -> Y
then we have the information that the element f(x)
is constrained to be of the type Y.
We can abbreviate this inference, that operates on
two pieces of information to produce another piece
of information, in the following conventional form:
- x : X
f : X -> Y
-----------
f(x) : Y
In this scheme of inference, the notations "x", "f", and "f(x)"
are taken to be names of formal objects. Some people will call
these notations by the name of "terms", while other people will
somewhat more confusedly say that the formal objects themselves
are the terms. Because it is so important to distinguish signs
denoting from objects denoted, I will make some effort to avoid
the latter usage, and recommend sticking with the first option.
In the same context, the notations "X", "X -> Y", and "Y" give us
information, or indicate formal constraints, that we may think of
as denoting the "types" of the formal objects under consideration.
By an act of "hypostatic abstraction", one may of course elect to
view these types as a species of formal objects existing in their
own right, inhabiting their own niche, as it were.
If a moment's spell of double vision leads us to see the
functional arrow "->" as the logical arrow "=>", then we
may observe that the right side of this inference scheme
follows the pattern of logical deduction that is usually
called "modus ponens". And so we forge a tentative link
between the pattern of information conversion implicated
in functional application and the pattern of information
conversion involved in the logical rule of modus ponens.
Jon Awbrey
Last edited by Jon Awbrey on 06-21-2004 at 03:50 PM
Report this post to a moderator | IP: Logged
|
06-21-2004 02:16 PM
