On Mon, Jun 20, 2016 at 05:14:45PM +0200, Erik Hesselink wrote:

It feels weird to me that this program transformation produces different output, and I can't seem to think of another IO action that behaves this way. Essentially, you'd want `IO a` to have different semantics from other `a`s, in that let binding it changes what it does.

It's definitely weird, but it seems consistent with some behaviour we see around lazy IO, Cf these threads https://mail.haskell.org/pipermail/haskell/2009-March/021064.html https://mail.haskell.org/pipermail/haskell/2009-March/021071.html

However, you can do this with the `qLocation` Template Haskell function in Language.Haskell.TH.Syntax. Does that help?

I meant it more as a sort of theoretical question.

On 20 June 2016 at 17:03, Tom Ellis wrote:

...

Is it compatible with the semantics of Haskell to have a function

sourceLocation :: IO String

which when run returns the source file location at which it is used? For example, suppose Main.hs is

module Main where

main = do putStrLn =<< sourceLocation putStrLn "Hello" putStrLn =<< sourceLocation

It would print the following when run

Main.hs:4 Hello Main.hs:6

and

module Main where

main = do let s = sourceLocation putStrLn =<< s putStrLn "Hello" putStrLn =<< s

It would print the following when run

Main.hs:4 Hello Main.hs:4

If this is not compatible with the semantics of Haskell, why not? I agree that the two programs must have the same denotation, but is there anything that requires them to have the same output when run?

...

Is it compatible with the semantics of Haskell to have a function sourceLocation :: IO String which when run returns the source file location at which it is used? It's totally compatible with Haskell semantics, since Haskell does not give any semantics to IO. Anything can happen when you do IO. But it's still a bit weird. :)

I think the weird feeling stems exactly from the fact that IO has no well-defined syntax. It's our convenient catch-all for anything remotely un-pure. Nondeterminism? Put it in IO! (Instead of a purely nondeterministic context) Non-destructive read access to a file? Put it in IO! (instead of adding Maybe to a nondeterministic context) Deterministic fire-and-forget write access to a log file? Put it in IO! (instead of a context that just provides an ordering) Firing missiles or calling the system to do an "rm -rf /"? Put it in IO! (instead of a System.Unsafe.Extras.Hidden.Unsafe.Very.WarningUnsafeDontTouchWhyDoWeEvenHaveThisOMGGetAwayFromMe) So let's just view IO as a shorthand for some unknown as-yet unspecified monad stack. (But note that most of the contexts I mentioned don't even need to be monadic) This is not to say IO is not good to have in this form. It's just not a helpful context to answer this question. From this vantage point a possibly better form of the question would be: Could we define a context which contains the required semantics that is consistent with Haskell syntax? Something like thisLine :: SourceInfo Int Of course once you have such a context you can just assume it's part of IO because everything is part of IO. To answer the modified question just think about these facts: 1. We can define contexts with 100% determinism across almost any transformation including changing all the source code around it, the compiler, the language version, and all optimizations. (pure functions, i.e. the Identity context) 2. We can also define contexts with almost 100% non-determinism even across two consecutive invocations with nothing else changed. (calls to external random number generators) 3. The context we are searching for would be deterministic across an intermediate subset of meta-transformations. So if these special semantics were not allowed we would have an inconsistent scale of determinism across meta-transformations, and that would need some serious explaining. Ergo it should be allowed. This trail of thought does bring up two interesting follow-up questions though: Is the hidden structure of the IO stack tightly bound to a theory of consistency across meta-transformations? And do we even have a suitable theory of such transformations if we would want to refine IO? I have no idea. MarLinn