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
