6
- self-reference -- recursive types
- object semantics -- unrolling
- inheritance -- dynamic binding
- subtyping -- inconsistencies
slide: Section 9.6: Self-reference
Finally, in section 6, we discussed self-reference
and looked at a calculus employing recursive
types.
It was shown how object semantics may be determined
by unrolling, and we studied the semantic
interpretation of dynamic binding.
Concluding this chapter, an example was given
showing an inconsistency in the
Eiffel type system.
- How would you characterize inheritance
as applied in knowledge representation?
Discuss the problems that arise
due to non-monotony.
- How would you render the meaning of
an inheritance lattice?
Give some examples.
- What is the meaning of a type?
How would you characterize the relation between
a type and its subtypes?
- Characterize the subtyping rules for ranges,
functions, records and variant records.
Give some examples.
- What is the intuition underlying the
function subtyping rule?
- What is understood by the notion
of objects as records?
Explain the subtyping rule for objects.
- Discuss the relative merits of typed
formalisms and untyped formalisms.
- What flavors of polymorphism
can you think of?
Explain how the various flavors are
related to programming language constructs.
- Discuss how inheritance may be understood
as an incremental modification mechanism.
- Characterize the simple type calculus
$\%l\_\{<=\}$, that is the syntax, type
assignment and refinement rules.
Do the same for $F\_\{\; /\backslash \; \}$
and $F\_\{<=\}$.
- Type the following expressions:
(a) $\{\; a\; =\; 1,\; f\; =\; \%l\; x:Int.\; x\; +\; 1\; \}$,
(b) $\%l\; x:Int\; .\; x\; *\; x$,
and
(c) $\%l\; x:\{\; b:Bool,\; f:\{\; a:Bool\; \}\; \}\; ->\; Int.x.f(x)$.
- Verify whether:
(a) $f\text{'}\; :\; 2..5\; ->\; Int\; <=\; f:1..4\; ->\; Int$,
(b) $\{\; a:Bool,\; f:Bool\; ->\; Int\; \}\; <=\; \{\; a:Int,\; f:\; Int\; ->\; Int\; \}$, and
(c) $\%l\; x:\; \{\; a:Bool\; \}\; ->\; Int\; <=\; \%l\; x:\; \{\; a:Bool,\; f:Bool\; ->\; Int\; \}\; ->\; Int$.
- Explain how you may model abstract
data types as existential types.
- What realizations of
the type
$\backslash E\; \%a.\; \{\; a:\%a,\; f:\%a\; ->\; Bool\; \}$
can you think of?
Give at least two examples.
- Prove that
$\%m\; \%a\; .\; \{\; c:\%a,\; b:\%a\; ->\; \%a\; \}\; \backslash not<=\; \%m\; \%a\; .\; \{\; b\; :\; \%a\; ->\; \%a\; \}$.
- Prove that
$\%m\; \%a\; .\; \{\; c\; :\; \%a,\; b:\; \%t\; ->\; \%a\; \}\; <=\; \%t$, for $\%t\; =\; \%m\; \%a.\{\; b:\; \%a\; ->\; \%a\; \}$.
slide: Questions
As further reading I recommend
[CW85] and [Pierce93].
As another source of material
and exercises consult [Palsberg94].
[BG93] contains a number of relevant papers.
An exhaustive overview of the semantics of object systems,
in both first order and second order calculi, is further
given in [ObjectCalculus].
[]
readme
course
preface
1
2
3
4
5
6
7
8
9
10
11
12
appendix
lectures
resources
eliens@cs.vu.nl
draft version 0.1 (15/7/2001)