> Ok I understand this isomorphism better. However this remark seems to be
> of no value to functional programmers.
Well, at least some functional programmers might disagree. Haskell was named
after the logician Haskell B. Curry (yes, that's the one in the Curry-Howard
isomorphism), and the preface of the Haskell reports has always acknowledged
his influence ("..whose work provides the logical basis for much of ours.").
Logicians have done a lot of useful work, and such correspondences are the
keys that enable us to import and use their work in new contexts. Without
such keys, the treasures of logic would remain locked away, so to speak.
> Why trying to mix terms( otr types) with relations ?
no mixing intended. I assume you are worried about the use of "logical"
quantifiers in types. But as you suggest, "normal" logic doesn't claim the
quantifiers for types as bodies, only for logical statements. So they are
free
for use, and as they happen to serve the purpose, we can (in typical Haskell
style;-) overload the syntax, and give quantified types a meaning as well.
And if we are careful, and let logic be our guide in the design of the type
system, we get a correspondence between formulae and types, which ensures
that we are not really talking about completely independent uses of a piece
of
syntax, but about related instances of a general concept.
So, the question should be:
Why invent new concepts and syntax when the familiar stuff does the job
so well?
> > It is this limitation of potential function definitions by their
> > required type that is used in the context of runST.
> >
> > runST :: forall a. (forall s. ST s a) -> a
> > -- read: for all a, if (a proof exists that),
> > -- for all s, objects of type ST s a exist,
> > -- then objects of type a exist
>
> I think a functional programmer wouldn't like to read it as that,
> sorry.
Noone has to read it as that (and you can arrive at similar conclusions if
you start from a different interpretation, as long as the two
interpretations
are consistent; see, e.g., the work on parametricity and free theorems).
> I just want to ask if this reflects completely the idea of runST as
> defined in Haskell?
There have been subtle bugs even in formal proofs, so it would be crazy to
claim completeness (with reference to what?) for an informal ad-hoc
explanation. I can say that the discussion of the ST type and its operations
in the light of the correspondence was meant to capture the essence of
the runST framework, but to answer your question, I would have to give
another explanation, formalize both, and show their equivalence..
You might want to reread the parts on runST in the "State in Haskell"
paper (which is as close to "the" idea of runST as we might get) and check
whether the technical explanations and proof outlines there make more
sense now, or whether there are any conflicts between their explanation
and mine (after all, you don't like to read types as logical formulae, so
you have to find another explanation;-).
> ARE we for this reason going to mix + with or etc.
>
> e.g. a or b + c and d . f
>
> This doen't look as a good logic course to me. It only confuses.
Again, no mixing is intended. There are quantifiers in several different
kinds of logic and there are quantifiers in some type systems. The former
quantify over formulae, the latter over types - no confusion possible.
Moreover, there are interpretations of type systems as logics that justify
the use of the concept and syntax of quantifiers.
As we are talking on the Haskell list, we can assume that people don't
want to invent an infinitude of names and symbols for different instances
of the same concept: no float-add, double-add, etc., just +, with different,
but hopefully related, interpretations on different, but related types; and
similarly, no classical-logic-forall, constructive-logic-forall,
Haskell-experimental-type-system-1-forall, etc., just one forall with
different, but hopefully related interpretations for different, but related
frameworks.
For this overloading to make sense, we need a correspondence that goes
beyond syntactic similarities. This is not a burden, but rather a major
benefit: designing "good" type systems is tricky, so we happily accept
any help we can get. If we can borrow concepts and proofs from logic,
we don't have to reinvent wheels (and we run a lower risk of promoting
square wheels) - the common syntax is a nice add-on, and reminds us
of our shared interests.
Yet another benefit, especially for people not involved in the design of
type systems, is that their intuitions about logic can help them to
understand
the intricacies of modern type systems.
Claus
