[Prev][Next][Index][Thread]
typed versus untyped/didactic versus logical
Date: Wed, 12 Oct 88 14:57:28-0000
To: types@theory.LCS.MIT.EDU
>From Roger Hindley;
The interesting discussion on teaching typed \ or type-assignment
is beginning to widen from the original didactic question to
one of logical development.
Perhaps we should keep the difference between these two in mind,
as anyone with teaching experience knows that they are not
necessarily related, indeed can be wildly different,
unless the students are so bright that teaching-technique does
not matter.
On the didactic side,
here is an aspect I think worth stressing: the contrast
between typed-term systems and type-assignment (TA) systems
can be seen very clearly in the 2 different ways that a type
a->b
is interpreted. In Church-style typed-term systems, a->b is thought
of as a set of functions whose domain is a and range is a subset of b.
But in TA systems, a->b is thought of as a class of operators f such
that
x in a ==> f(x) in b, if f(x) is defined.
This does not commit f to having domain restricted to a, and hence
allows one term to have many types.
(It seems neat to call these interpretations the Church and
the Curry interpretation, respectively.)
Didactically, this point and similar semantic points can
probably be best brought out before any formal semantics is
given. In fact, I think the students should be given the
chance to play with \-terms as an uninterpreted game for a
while, and will probably learn best this way, before any
mention of formal semantics is made. For this reason I would
favour teaching untyped \-calculus first, and telling any
student who asks what it all means to shut up and ask the
same question again in a few weeks' time.
(After all, we do not demand that our children know what numbers
are before we teach them arithmetic!)