Thanks for your comments.
They are to the point.
But the first email arose from the fact that someone else claimed that
the forall quantifier was used in the same way as in (say "classical")
logic.
I still claim that everything could be put in a classical logic framework,
which is then another framework than the one proposed in Haskell
Very friendly
Jan Brosius
>----- Original Message -----
>From: Lars Lundgren <[EMAIL PROTECTED]>
>To: Jan Brosius <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>
>Sent: Wednesday, May 17, 2000 10:56 AM
>Subject: Re: more detailed explanation about forall in Haskell
> On Tue, 16 May 2000, Jan Brosius wrote:
>
> >
> > >----- 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.
>
> So in other words, f will map any value - given that it is an element of
> the right set (i.e given that it satisfies the precondition) to a value
> that is an element of Int - sounds like a postcondition to me.
>
>
> > 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 .
>
> But of course, that is not the case, but it might help if you want to
> understand the rationale behind the choice of name for the type quantifier
> "forall".
>
> > 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 wasn't after a definition, I just tried to explain that it is quite
> natural to view types as formulas, and that it is not in conflict with
> other views. (and it is not restricted to type systems for fp languages)
>
> > 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.
>
> If you read the typing rules, remember to have a reference of the natural
> deduction rules with you...
>
> > And the only introduction about types were the general user's guides
> > from Clean , SML , Ocaml and of Haskell.
> > >
>
> If you are interested in systems that exploit the isomorphism further you
> can take a look at :
>
> cayenne, agda, alfa from:
>
> http://www.cs.chalmers.se/Cs/Research/Logic/implementation.mhtml
>
> /Lars L
>
>
>
>
>
