>----- Original Message -----
>From: Lars Lundgren <[EMAIL PROTECTED]>
>
>Sent: Tuesday, May 16, 2000 1:54 PM
>Subject: Re: more detailed explanation about forall in Haskell
> On Tue, 16 May 2000, Jan Brosius wrote:
>
> > Ok I understand this isomorphism better. However this remark seems to be
of
> > no value to functional programmers.
> > Why trying to mix terms( otr types) with relations ?
> >
>
> What is a 'type' in your oppinion?
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.
I didn't come into problems by this interpretation after having read the
Haskell's User Guide. Which is my
only general source about Haskell. It is up to someone else to say if such
an interpretation shall lead into misinterpretation.
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.
>
> Isn't a type a statement about pre- and post-conditions, i.e. a formula?
I can't answer this since I have never read the definition of a type in say
typed lambda calculus.
I have a book about logic that deals about plain lambda calculus and that
deals about "restricted" typed lambda calculus (where a type is not
considered as a formula). I never read the definition of Hindley-Milner
types.And the only introduction about types were the general user's guides
from Clean , SML , Ocaml and of Haskell.
>
> /Lars L
>
>
>
>
