I'm reluctant to get involved in this discussion, cheifly
because it seems to me that Jan is attacking a position that
has quite a long history with (inter alia) the argument that
a different position has a longer history, which doesn't
strike me as terribly likely to lead to insight.
Also my present powers of concentration don't allow me to
keep up with the argument, so I'll just drop in a couple of
points and duck out again.
> [Lars asked]
> > What is a 'type' in your oppinion?
[Jan replied]
> I look at it as a set (either a variable set or a specific set). E.g. I look
> at Bool as a specific set which itself contains
> values True , False that are not sets. Next I interpret something like f
> :: a -> Int as a family (indexed by a) of functions of " set" a into set
> Int. [snippety]
> It is up to someone else to say if such
> an interpretation shall lead into misinterpretation.
Interpreting types as sets is not straightforward: try
"Types are not sets" by James H. Morris, JR.
in POPL 1973
as one pointer into this area.
> I think Haskell will not be attractive to mathematicians
> if types MUST be read as formula's . If that is the case I
> can only say that I find the term "functional programming"
> a bit strange.
I don't think anyone said that they must. They can be, and
one useful way of interpreting a type is as a statement of
limitations on the use and behaviour of a term.
f :: A -> B can be read as "if x is of type A, then f x will
be of type B"
x :: forall a . E can be read as "for all types A, x :: E [A/a]"
I think the major source of confusion is that Haskell
started out using the convention that a type expression
containing a free variable was understood as being
universally quantified at the top level (a convention which,
I might add, I argued against in the first Haskell
committee, so nyaa...), but then added 'forall' as an
extension later (I thought this was going to happen :-))
Apart from that, I think that (once they have had the
conventions and notation described to them) most
mathematicians are not going to be put off by the type
system. Certainly mathematicians must be warned against
interpreting types simply as sets, but they also need to be
warned that a "function" is not a function in the
mathematical sense either, being constrained by the limits
of computation.
> >
> > Isn't a type a statement about pre- and post-conditions, i.e. a formula?
I'd say that's another reasonable way of reading them.
> I can't answer this since I have never read the definition of a type in say
> typed lambda calculus.
Go on then! It won't hurt!
Cheers,
Jón
--
Jón Fairbairn [EMAIL PROTECTED]
18 Kimberley Road [EMAIL PROTECTED]
Cambridge CB4 1HH +44 1223 570179 (after 14:00 only, please!)
