Fri, 19 May 2000 19:47:38 +0200, Iavor Diatchki <[EMAIL PROTECTED]> pisze:
> i do not see the need for the "forall" quantifier to be written
> explicitly however,
It is needed when the quantifier is inside a function argument,
to spell the difference between
f1 :: forall a. ([a] -> [a]) -> [
>From: Peter Douglass <[EMAIL PROTECTED]>
>To: 'Jan Brosius' <[EMAIL PROTECTED]>; Frank Atanassow <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>
>Sent: Friday, May 19, 2000 6:03 PM
>Subject: RE: more detailed explanation about forall in Haskell
hello,
i have been following the evolution of haskell for about 2 years now in my spare
time, but haven't had time to really get into haskell programming. so i am not
an expert or anything. i do not see the need for the "forall" quantifier to be written
explicitly however, and i quite like the wa
Fri, 19 May 2000 14:48:24 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> On the other hand someone's remark and about the meaning Haskell gives to
> these two types and I wonder since today if one means by a -> a a type
> indication to be understood as a function having this type signature
Peter Hancock writes:
[..]
> Please guys, you are making clowns of yourselves.
Amen to that! I've just added the above subject line to my kill file,
rather than stop reading the Haskell list altogether.
--KW 8-)
--
: Keith Wansbrough, MSc, BSc(Hons) (Auckland) ---:
: PhD St
This is getting hysterically funny:
> *Jan Brosius writes:
> * > > > I must put this in the good way;
> * > > >
> * > > > [forall x . alpha(x)] => alpha(x) is True
> * > >
> * > > Yes, by instantiation.
> * >
> * > I disagree.
> *You disagree with my agre
Jan Brosius wrote:
> look at this example:
>
> alpha(x) == x is_an Integer => x^2 > -1
>
> this is an example of a formula that is true
>
> *If you want to come up with your own logic, where alpha(x)
> is equivalent to
> *forall x. alpha(x), then that's fine.
>
> No, i
> As Mark Jones has allready said this thread should end or come to a
> conclusion. Unfortunately he said more than that . He said that the
> discussion was all about the difference a -> a and forall a. a -> a . And
> that's not
> true . One only has to read the first 2 or 4 emails about this
59 PM
*Subject: Re: more detailed explanation about forall in Haskell
*Jan Brosius writes:
* > > > I must put this in the good way;
* > > >
* > > > [forall x . alpha(x)] => alpha(x) is True
* > >
* > > Yes, by instantiation.
* >
* > I disagree.
*
Frank Atanassow wrote:
> However, I think maybe it has demonstrated that the implicit
> forall'ing in
> Haskell can be confusing in practice. In particular, it makes
> it hard to talk
> unambiguously about types of non-top-level definitions/terms.
I'm sure this pot has been stirred up enough
|From: Lennart Augustsson <[EMAIL PROTECTED]>
|To: Jan Brosius <[EMAIL PROTECTED]>
|Cc: Frank Atanassow <[EMAIL PROTECTED]>; <[EMAIL PROTECTED]>
|Sent: Friday, May 19, 2000 12:07 PM
|Subject: Re: more detailed explanation about forall in Haskell
> Jan Brosius wrote
> Please could somebody post a short, plain text summary of the discussion
> in this thread? The recent exchanges have been long and involved, which
> has made it impossible for me (and other busy onlookers too, I suspect)
> to keep up. Without such a summary, I think that this thread may be
> r
On 19 May 2000, Ketil Malde wrote:
> Frank Atanassow <[EMAIL PROTECTED]> writes:
>
> > I agree, and I think it's hopeless. This is my last message to the Haskell
> > list on the subject. There is nothing Haskell-specific any longer about this
> > discussion.
>
> Uh, I feel I'm a bit of a hobbyi
There is a good introduction by Cardelli and Wegner:
Luca Cardelli and Peter Wegner. On understanding types, data abstraction,
and polymorphism. Computing Surveys, 17(4):471-522, 1985.
available from Cardelli's page at
http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.A4.ps
Frank Atanassow <[EMAIL PROTECTED]> writes:
> I agree, and I think it's hopeless. This is my last message to the Haskell
> list on the subject. There is nothing Haskell-specific any longer about this
> discussion.
Uh, I feel I'm a bit of a hobbyist on this list, but what exactly is
the relevance
Mark P Jones writes:
> Please could somebody post a short, plain text summary of the discussion
> in this thread? The recent exchanges have been long and involved, which
> has made it impossible for me (and other busy onlookers too, I suspect)
> to keep up. Without such a summary, I think th
Jan Brosius writes:
> > > I must put this in the good way;
> > >
> > > [forall x . alpha(x)] => alpha(x) is True
> >
> > Yes, by instantiation.
>
> I disagree.
You disagree with my agreeing with you?
> > > If alpha(x) is TRUE then the following is true : alpha(x) => [forall x.
> >
Jan Brosius wrote:
> > "x" in the domain of your model, and that that element, at least,
> satisfies
>
> x is a variable ; no domain ; no model
You must have some assumed convention that makes x a variable.
For the rest of us it might as well be a constant, because there is
no way to tell if it
Dear All,
Please could somebody post a short, plain text summary of the discussion
in this thread? The recent exchanges have been long and involved, which
has made it impossible for me (and other busy onlookers too, I suspect)
to keep up. Without such a summary, I think that this thread may be
>From: Frank Atanassow <[EMAIL PROTECTED]>
>To: Jan Brosius <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>
>Sent: Thursday, May 18, 2000 2:53 PM
>Subject: Re: more detailed explanation about forall in Haskell
> Jan Brosius writes:
> > I must put this in
Jan Brosius writes:
> I must put this in the good way;
>
> [forall x . alpha(x)] => alpha(x) is True
Yes, by instantiation.
> If alpha(x) is TRUE then the following is true : alpha(x) => [forall x.
> alpha(x)]
No, alpha(x) only asserts that some element named x satisfies alpha. It does
no
- Original Message -
From: Jan Brosius <[EMAIL PROTECTED]>
To: Carl R. Witty <[EMAIL PROTECTED]>
Sent: Thursday, May 18, 2000 12:06 PM
Subject: Re: Fw: more detailed explanation about forall in Haskell
> Thanks Carl for letting me see an ugly error that I made . SHAME
Sorry, if in some way I have upset you
Sincerely
Jan Brosius
>From: Frank Atanassow <[EMAIL PROTECTED]>
>To: Frank Atanassow <[EMAIL PROTECTED]>
>Sent: Wednesday, May 17, 2000 1:50 PM
>Subject: Fw: more detailed explanation about forall in Haskell
> Frank Atanass
>>>From: Frank Atanassow <[EMAIL PROTECTED]>
>To: Jan Brosius <[EMAIL PROTECTED]>
>Cc: <[EMAIL PROTECTED]>>
>Sent: Wednesday, May 17, 2000 1:35 PM
>Subject: Fw: more detailed explanation about forall in Haskell
> Jan Brosius writes:
> > &
ct: 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
> &
> 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 prefa
Frank Atanassow writes:
> Jan Brosius writes:
> > > Why do some computer scientists have such problems with the good logical
> > > forall
> > > and exist. Remember that good old logic came first.
> > > On it was build SET theory.
> > > On it was built topological space
> > >
> > >
Jan Brosius writes:
> > Why do some computer scientists have such problems with the good logical
> > forall
> > and exist. Remember that good old logic came first.
> > On it was build SET theory.
> > On it was built topological space
> >
> > To prove some theorem in lambda calculus one use
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 pr
On Wed, 17 May 2000, Dave Tweed wrote:
> [forall x.prime(x)] -||- [forall x.prime(x)]
>
> ie, a tautology.
^^^
Sorry, I really shouldn't email until _after_ my first cup of coffee...
I meant `trivially a correct statement about the logic', not tautology
which has a more precise meaning i
On 16 May 2000, Carl R. Witty wrote:
> "Jan Brosius" <[EMAIL PROTECTED]> writes:
>
> > > SORRY, this is quite TRUE , in fact [forall x. alpha(x)] <=> alpha(x)
> > >
> > > the above true equivalence seems to be easily considered as wrong . Why?
> > > Because alpha(x) is TRUE can be read as a
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
"Jan Brosius" <[EMAIL PROTECTED]> writes:
> > SORRY, this is quite TRUE , in fact [forall x. alpha(x)] <=> alpha(x)
> >
> > the above true equivalence seems to be easily considered as wrong . Why?
> > Because alpha(x) is TRUE can be read as alpha(x) is TRUE for ANY x.
> >
> > (Is there somet
- Original Message -
From: Jan Brosius <[EMAIL PROTECTED]>
To: Richard Uhtenwoldt <[EMAIL PROTECTED]>
Sent: Wednesday, May 17, 2000 1:23 AM
Subject: Re: more detailed explanation about forall in Haskell
>
> - Original Message -
> From: Richard Uhtenwo
>- Original Message -
>From: Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]>
>Sent: Tuesday, May 16, 2000 11:40 PM
>Subject: Re: more detailed explanation about forall in Haskell
> Tue, 16 May 2000 22:37:45 +0200, Jan Brosius <[EMAIL PROTECTED]>
pi
Tue, 16 May 2000 22:37:45 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> > newSTRef applied to some value can have a type ST s (STRef s T(s)),
>
> That is strange , can you give a little example?
I've given it four mail pairs ago, but here it is again:
refRef :: ST s Int
refRef = do
although this argument originated from a discussion of rank-2
polymorphism in Haskell's type system, the part I am replying to
addresses only first-order predicate logic (also called "predicate
calculus").
Jan Brosius asserts
> Now forall s1. ( ST s1 T(s)) IMPLIES forall s . ( ST s T(s) )
>- 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
>From: Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]>
>To: <[EMAIL PROTECTED]>
>Sent: Tuesday, May 16, 2000 11:42 AM
>Subject: Re: more detailed explanation about forall in Haskell
> Tue, 16 May 2000 10:54:59 +0200, Jan Brosius <[EMAIL PROTECTED]>
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?
Isn't a type a statement about pre- and post-c
Tue, 16 May 2000 10:54:59 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> > > newSTRef v has type ST s (STRef s (STRef s a))
> > > (THIS is of the form ST s (STRef s T(s))
> >
> > No. It has the type
> > ST s1 (STRef s1 (STRef s a))
>
> That is indeed what I said in my former email where
I reply , but I like to make some comments before:
As readers would have noticed from the former email my answers are put here
in a different context.
This might give the reader the false impression that I made some serious
mistakes in the formal
email.
> Fri, 12 May 2000 00:42:52 +0200, Jan Bro
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 ?
> > > > Anyway, in intuitionistic logic it is natural indentify proofs and
> > > > programs and proposition and types. Maybe best
Fri, 12 May 2000 00:42:52 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> newSTRef :: a -> ST s (STRef s a)
> readSTRef :: STRef s a -> ST s a
> and
>
> f:: STRef s a -> STRef s a
> f v = runST( newSTRef v >= \w -> readSTRef w)
>
> Let's start
>
> v has type STRef s a
...for "s" and "a"
Claus Reinke writes:
[nice exposition of C-H correspondence & state threads]
> The main caveat is the insistence on constructive proofs (in the classical
> logic most of us tend to learn, there is this favourite proof technique: if
> I assume that xs don't exist, I am led to a contradiction, so
> > > Anyway, in intuitionistic logic it is natural indentify proofs and
> > > programs and proposition and types. Maybe best illustrated by the BHK
> > > (Brouwer-Heyting-Kolmogoroff) semantics:
> > >
> > > A proof of a /\ b is a proof of a and a proof of b, hence a /\ b =
(a,b)
> >
> > Sorry, ar
On Fri, 12 May 2000, Jan Brosius wrote:
> >
> > Your example gave the same meaning to `b and forall.
>
> NOT true : forall works on a proposition and delivers another proposition .
> And this should REMAIN so.
>
> `b on the contrary works on a type and delivers a new type.
>
> Quite different
Dear Marcin,
I think we have reached now a point in the discussion that will only result
in yes and no.
1. Even as I still think that the forall in runST is misplaced I still stand
open for everyone that could
put forall s. (ST s a) in an acceptable logical phrase. forall and exist
work like th
Thu, 11 May 2000 13:48:56 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> > Types can be treated as logical formulas, according to the Curry-Howard
> > isomorphism.
>
> Sorry, never heard of in logic. But perhaps you can explain.
Others explained it better that I could.
> > > newSTRef:: forall
>
>
>
> > Jan Brosius writes:
> > > Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
> > > > > 2. Next let me point out once and for all that
> > > > > logical quantifiers are used only in logical formula's .
> > > >
> > > > Types can be treated as logical formulas, according to the
Thorsten Altenkirch writes:
> Jan Brosius writes:
> > Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
> > > > 2. Next let me point out once and for all that
> > > > logical quantifiers are used only in logical formula's .
> > >
> > > Types can be treated as logical formulas, accor
Jan Brosius writes:
> Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
> > > 2. Next let me point out once and for all that
> > > logical quantifiers are used only in logical formula's .
> >
> > Types can be treated as logical formulas, according to the Curry-Howard
> > isomorphism.
>
On Thu, 11 May 2000, Jan Brosius wrote:
> Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
>
> > Types can be treated as logical formulas, according to the Curry-Howard
> > isomorphism.
>
> Sorry, never heard of in logic. But perhaps you can explain.
>
M H Sørensen and P Urzyczyn.
Lectur
Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
> Wed, 10 May 2000 16:18:06 +0200, Jan Brosius <[EMAIL PROTECTED]>
pisze:
pisze ? you meant wrote? Please don't use Russian in your reply, I don't
know Russian.
Do You know what pisze in Dutch could mean if spoken out loosely?
>
> > 2. Next
Wed, 10 May 2000 16:18:06 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> 2. Next let me point out once and for all that
> logical quantifiers are used only in logical formula's .
Types can be treated as logical formulas, according to the Curry-Howard
isomorphism. I see no reason to change the n
Hi,
According to the reactions that I have received
I feel the need to explain in more detail my
email
in mime type entitled : about the abuse of
forall
in Haskell. The easiest thing for me would be to
send an attachment in pdf to the Haskell -
mailing
list. But I guess this is impossible.
56 matches
Mail list logo
