Information Technology Reference
In-Depth Information
-Terms:
x
:
A, b
:
B,
a, b
,ʻx.b
(
x
)
,...
- Dependent Types:
x
:
A
B
(
x
)
•
x
:
A, y
:
B
(
x
)
C
(
x, y
)
•
x
:
A
B
(
x
)
•
x
:
A
B
(
x
)
-Equations
s
=
t
:
A
It was originally intended as a foundation for constructive mathematics, but
is now used also in the theory of programming languages and as the basis of
computational proof assistants.
Propositions as Types
The system has a dual interpretation:
-
once as
mathematical
objects: types are “sets” and their terms are “ele-
ments”, which are being constructed,
-
once as
logical
objects: types are “propositions” and their terms are “proofs”,
which are being derived.
This is known as the
Curry-Howard correspondence
:
0 1
A
+
B A
B
x
:
A
B
(
x
)
x
:
A
B
(
x
)
×
B A
→
↥
T
A
∨
B A
∧
B A
⃒
B
∃
x
:
A
B
(
x
)
∀
x
:
A
B
(
x
)
Gives the system its
constructive character
.
Identity Types
It's natural to add a primitive relation of
identity
between any terms of the
same type:
Id
A
(
x, y
)
Logically
this is the proposition “x is identical to y”.
Butwhatisit
mathematically
?
x, y
:
A
The
introduction
rule says that
a
:
A
is always identical to itself:
r
(
a
):
Id
A
(
a, a
)
The
elimination
rule is a form of Lawvere's law:
d
(
x
):
R
x, x,
r
(
x
)
J
d
(
a, b, c
):
R
(
a, b, c
)
c
:
Id
A
(
a, b
)
x
:
A
Schematically:
“
a
=
b
&
R
(
x, x
)
⃒
R
(
a, b
)”
