On Wednesday 12 November 2008 7:05:02 pm Jonathan Cast wrote:
I think the point is that randomIO is non-deterministic (technically,
pseudo-random) but causal --- the result is completely determined by
events that precede its completion. unsafeInterleaveIO, by contrast, is
arguably (sometimes)
Lennart Augustsson wrote:
You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
You could use a two step approach: first make a static semantics that
does type
It's possible that there's some more direct approach that
represents types as some kind of runtime values, but nobody
(to my knowledge) has done that.
It don't think its possible - I tried it and failed.
Consider:
show (f [])
Where f has the semantics of id, but has either the return
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On Nov 12, 2008, at 7:09 AM, Lennart Augustsson wrote:
It's possible that there's some more direct approach that represents
types as some kind of runtime values, but nobody (to my knowledge) has
done that.
I think JHC passes types at runtime,
Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up that
claim. I know that, in practice, I can't write any counter-examples but
that's a bit handy-wavy. Is there a formal proof that, for
Correct Lennart. The below mentioned papers assume some
evidence translation of type class programs. If you need/want
a direct semantics/translation of programs you'll need to
impose some restrictions on the set of allowable type class programs.
For such an approach see
Martin Odersky,
I had a quick look at Stuckey and Sulzmann, A Theory of Overloading
and it looks to me like the semantics is given by evidence
translation. So first you do evidence translation, and then give
semantics to the translated program. So this looks like the two step
approach I first mentioned.
Or have
Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up that
claim. I know that, in practice, I can't write any counter-examples but
that's a bit handy-wavy. Is there a formal proof that, for
See What is a purely functional language by Sabry. Not quite a
formal proof about *Haskell*, but then we would first need a formal
semantics of Haskell to be able to do that proof ;-)
On 12 Nov 2008, at 10:11, Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is
On 12 Nov 2008, at 11:11, Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up
that claim. I know that, in practice, I can't write any counter-
examples but that's a bit handy-wavy. Is
On a totally non-theory side, Haskell isn't referentially transparent.
In particular, any code that calls unsafePerformIO or
unsafeInterleaveIO is not necessarily RT. Given that getContents and
interact use unsafeInterleaveIO, this includes most toy programs as
well as almost every non-toy
On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean [EMAIL PROTECTED] wrote:
Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially transparent?
Many people state haskell is RT without backing up that claim. I know
that, in practice, I can't write any
Hi all,
On Wed, Nov 12, 2008 at 2:09 PM, Lennart Augustsson
[EMAIL PROTECTED]wrote:
You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
...
It's possible that
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Since you are talking to the outside world any behaviour is acceptable.
All the weird interactions between getContents and writing the same
file from the same program could, in principle, happen if a different
program wrote
On 12 Nov 2008, at 14:47, Mitchell, Neil wrote:
It's possible that there's some more direct approach that
represents types as some kind of runtime values, but nobody
(to my knowledge) has done that.
It don't think its possible - I tried it and failed.
Consider:
show (f [])
Where f has
On Wed, Nov 12, 2008 at 12:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Since you are talking to the outside world any behaviour is acceptable.
All the weird interactions between getContents and writing the same
file
You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
You could use a two step approach: first make a static semantics that
does type inference/checking and translates
Edsko de Vries wrote:
See What is a purely functional language by Sabry. Not quite a formal
proof about *Haskell*, but then we would first need a formal semantics
of Haskell to be able to do that proof ;-)
Thanks for the reference, and also to everyone who replied - all very
useful and
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which when passed to
ostensibly pure functions yield different results depending on their
evaluation
On Wed, 2008-11-12 at 22:16 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which when passed to
ostensibly pure
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which when passed to
ostensibly pure functions yield different results
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of
On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast
[EMAIL PROTECTED] wrote:
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED]
On Wed, 2008-11-12 at 23:18 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast
[EMAIL PROTECTED] wrote:
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12,
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of
On Wednesday 12 November 2008 6:18:38 pm David MacIver wrote:
To put it a different way, in the absence of unsafeInterleaveIO the IO
monad has the property that if f and g are observably equal up to
termination then x = f and x = g are equivalent in the IO monad
(actually this may not be true
On Wed, 2008-11-12 at 18:47 -0500, Dan Doel wrote:
On Wednesday 12 November 2008 6:18:38 pm David MacIver wrote:
To put it a different way, in the absence of unsafeInterleaveIO the IO
monad has the property that if f and g are observably equal up to
termination then x = f and x = g are
But how can you tell something being causal or not?
Assuming that all IO operations return random result, of course. :)
From a practical point of view unsafeInterleaveIO can give suspect results.
But theoretically you can't fault it until you have given a semantics
for the IO monad operations so
Interesting posts. Thanks!
On Wed, Nov 12, 2008 at 2:02 PM, Andrew Birkett [EMAIL PROTECTED] wrote:
Thanks for the reference, and also to everyone who replied - all very
useful and interesting. For what it's worth, the blog posts I was writing
are here:
30 matches
Mail list logo
