What does this mean again? I'm working on the assumption that
`context-sensitive' means `under some (not necessarily compositional
and/or continuous and/or monotonic) equivalence relation/
I'm using "contexts" as "expressions with holes", as used for "evaluation
contexts" in operational semanti
Jonathan Cast writes:
>> Couldn't you just substitute "catch exceptions" with "unsafePerformIO"
>> here, and make the same argument?
> This puzzled me, until I realized you meant `unsafeInterleaveIO'.
Aargh, yes of course! Sorry about that.
> Assuming you mean unsafeInterleaveIO, not quite.
On Tue, 2009-03-17 at 12:59 +0100, Ketil Malde wrote:
> Duncan Coutts writes:
>
> >> [..] I have a sneaking suspicion [exceptions] actually *is* `unsafe'. Or,
> >> at
> >> least, incapable of being given a compositional, continuous semantics.
>
> > Basically if we can only catch exceptions in
On Tue, 2009-03-17 at 12:40 +, Claus Reinke wrote:
> >> So that first step already relies on IO (where the two are equivalent).
> > Come again?
>
> The first step in your implication chain was (without the return)
>
> throw (ErrorCall "urk!") <= 1
> ==> evaluate (throw (ErrorCall "urk
So that first step already relies on IO (where the two are equivalent).
Come again?
The first step in your implication chain was (without the return)
throw (ErrorCall "urk!") <= 1
==> evaluate (throw (ErrorCall "urk!")) <= evaluate 1
but, using evaluation only (no context-sensitive IO),
Duncan Coutts writes:
>> [..] I have a sneaking suspicion [exceptions] actually *is* `unsafe'. Or, at
>> least, incapable of being given a compositional, continuous semantics.
> Basically if we can only catch exceptions in IO then it doesn't matter,
> it's just a little extra non-determinism an
On 17/03/2009, at 1:13 PM, Jonathan Cast wrote:
[Totally OT tangent: How did operational semantics come to get its
noun?
The more I think about it, the more it seems like a precís of the
implementation, rather than a truly semantic part of a language
specification.]
I haven't followed the w
On Tue, 2009-03-17 at 01:16 +, Claus Reinke wrote:
> >> > > "exception handling" which allows to "catch" programming errors.
> >> > And which I have a sneaking suspicion actually *is* `unsafe'. Or, at
> >> > least, incapable of being given a compositional, continuous semantics.
> >> "A semanti
> > "exception handling" which allows to "catch" programming errors.
> And which I have a sneaking suspicion actually *is* `unsafe'. Or, at
> least, incapable of being given a compositional, continuous semantics.
"A semantics for imprecise exceptions"
http://research.microsoft.com/en-us/um/people
On Mon, 2009-03-16 at 22:01 +, Duncan Coutts wrote:
> On Mon, 2009-03-16 at 14:17 -0700, Jonathan Cast wrote:
> > On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote:
> > > On Sun, 15 Mar 2009, Claus Reinke wrote:
> > >
> > > > import Data.IORef
> > > > import Control.Exception
> > > >
On Mon, 2009-03-16 at 14:17 -0700, Jonathan Cast wrote:
> On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote:
> > On Sun, 15 Mar 2009, Claus Reinke wrote:
> >
> > > import Data.IORef
> > > import Control.Exception
> > >
> > > main = do
> > > r <- newIORef 0
> > > let v = undefined
> >
On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote:
> On Sun, 15 Mar 2009, Claus Reinke wrote:
>
> > import Data.IORef
> > import Control.Exception
> >
> > main = do
> > r <- newIORef 0
> > let v = undefined
> > handle (\(ErrorCall _)->print "hi">>return 42) $ case f v of
> > 0
On Sun, 15 Mar 2009, Claus Reinke wrote:
import Data.IORef
import Control.Exception
main = do
r <- newIORef 0
let v = undefined
handle (\(ErrorCall _)->print "hi">>return 42) $ case f v of
0 -> return 0
n -> return (n - 1)
y <- readIORef r
print y
I don't see what this has
On Sun, 15 Mar 2009, Ryan Ingram wrote:
unsafeInterleaveIO allows embedding side effects into a pure
computation. This means you can potentially observe if some pure
value has been evaluated or not; the result of your code could change
depending how lazy/strict it is, which is very hard to pr
On Monday 16 March 2009 2:11:10 pm Ryan Ingram wrote:
> However, I disagree with your description of what "unsafe" should be
> used for. "unsafe" calls out the need for the programmer to prove
> that what they are doing is safe semantically, instead of the compiler
> providing those proofs for you
On Mon, Mar 16, 2009 at 7:55 AM, Jake McArthur wrote:
> I think it depends on what we want to take "unsafe" to mean. In my
> opinion, the word "unsafe" should really only be used in cases where
> using the function can case an otherwise well-typed program to not be
> well-typed. I'm pretty sure I
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Yusaku Hashimoto wrote:
| I was studying about what unsafeInterleaveIO is.I understood
| unsafeInterleaveIO takes an IO action, and delays it. But I couldn't
| find any reason why unsafeInterleaveIO is unsafe.
I think it depends on what we want to ta
On 2009 Mar 16, at 8:48, Yusaku Hashimoto wrote:
On 2009/03/16, at 10:04, wren ng thornton wrote:
Moreover, let's have two pure implementations, f and g, of the same
mathematical function. Even if f and g are close enough to
correctly give the same output for inputs with _|_ in them, we may
Hi,
On 2009/03/16, at 10:04, wren ng thornton wrote:
> next r = do n <- readIORef r
> writeIORef r (n+1)
> return n
Now, if I use unsafeInterleaveIO:
> main = do r <- newIORef 0
> x <- do a <- unsafeInterleaveIO (next r)
>b <- unsafeInter
On Sun, 2009-03-15 at 18:11 -0700, Ryan Ingram wrote:
> On Sun, Mar 15, 2009 at 1:56 PM, Jonathan Cast
> wrote:
> >> But not if you switch the (x <- ...) and (y <- ...) parts:
> >>
> >> main = do
> >> r <- newIORef 0
> >> v <- unsafeInterleaveIO $ do
> >> writeIORef r 1
> >>
On Sun, Mar 15, 2009 at 1:56 PM, Jonathan Cast
wrote:
>> But not if you switch the (x <- ...) and (y <- ...) parts:
>>
>> main = do
>> r <- newIORef 0
>> v <- unsafeInterleaveIO $ do
>> writeIORef r 1
>> return 1
>> y <- readIORef r
>> x <- case f v of
>>
Yusaku Hashimoto wrote:
Hello,
I was studying about what unsafeInterleaveIO is.I understood
unsafeInterleaveIO takes an IO action, and delays it. But I couldn't
find any reason why unsafeInterleaveIO is unsafe.
I have already read an example in
http://www.haskell.org/pipermail/haskell-cafe/2009
On Mon, 2009-03-16 at 01:04 +0100, Daniel Fischer wrote:
> Am Montag, 16. März 2009 00:47 schrieb Jonathan Cast:
> > On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote:
> >
> > > > > However, I understand
> > > > > "unsafeInterleaveIO allows IO computation to be deferred lazily. When
> > > > >
Am Montag, 16. März 2009 00:47 schrieb Jonathan Cast:
> On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote:
>
> > > > However, I understand
> > > > "unsafeInterleaveIO allows IO computation to be deferred lazily. When
> > > > passed a value of type IO a, the IO will only be performed when the
On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote:
> Am Sonntag, 15. März 2009 23:30 schrieb Jonathan Cast:
> > On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote:
> > > Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:
> > > > There is *no* guarantee that main0 prints 0, while main
main = do
r <- newIORef 0
v <- unsafeInterleaveIO $ do
writeIORef r 1
return 1
x <- case f v of
0 -> return 0
n -> return (n - 1)
y <- readIORef r
print y
-- a couple of examples:
f x = 0 -- program prints "0"
-- f x = x -- program prints "1"
Am Sonntag, 15. März 2009 23:30 schrieb Jonathan Cast:
> On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote:
> > Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:
> > > There is *no* guarantee that main0 prints 0, while main1 prints 1, as
> > > claimed. The compiler is in fact free to pr
On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote:
> Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:
> > There is *no* guarantee that main0 prints 0, while main1 prints 1, as
> > claimed. The compiler is in fact free to produce either output given
> > either program, at its option. S
Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast:
> There is *no* guarantee that main0 prints 0, while main1 prints 1, as
> claimed. The compiler is in fact free to produce either output given
> either program, at its option. Since the two programs do in fact have
> exactly the same set of p
On Sun, 2009-03-15 at 22:09 +0100, Daniel Fischer wrote:
> Am Sonntag, 15. März 2009 21:56 schrieb Jonathan Cast:
> > On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote:
> > > Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast:
> > > > On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:
>
Am Sonntag, 15. März 2009 21:56 schrieb Jonathan Cast:
> On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote:
> > Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast:
> > > On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:
> > > > Furthermore, due to the monad laws, if f is total, then re
On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote:
> Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast:
> > On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:
> >
> > > Furthermore, due to the monad laws, if f is total, then reordering the
> > > (x <- ...) and (y <- ...) parts of the p
Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast:
> On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:
>
> > Furthermore, due to the monad laws, if f is total, then reordering the
> > (x <- ...) and (y <- ...) parts of the program should have no effect.
> > But if you switch them, the progr
On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote:
> unsafeInterleaveIO allows embedding side effects into a pure
> computation. This means you can potentially observe if some pure
> value has been evaluated or not; the result of your code could change
> depending how lazy/strict it is, which
unsafeInterleaveIO allows embedding side effects into a pure
computation. This means you can potentially observe if some pure
value has been evaluated or not; the result of your code could change
depending how lazy/strict it is, which is very hard to predict!
For example:
> -- given
> f :: Inte
Hello,
I was studying about what unsafeInterleaveIO is.I understood
unsafeInterleaveIO takes an IO action, and delays it. But I couldn't
find any reason why unsafeInterleaveIO is unsafe.
I have already read an example in
http://www.haskell.org/pipermail/haskell-cafe/2009-March/057101.html
says la
36 matches
Mail list logo
