On Jan 2, 2012, at 1:30 PM, Conal Elliott wrote: > On 2012/1/1 Ertugrul Söylemez <e...@ertes.de> wrote: > > And that's fine, because IO is an embedded DSL. A better view of IO is > a GADT like: > > data IO :: * -> * where > GetLine :: IO String > PutStrLn :: String -> IO () > ... > > This is still hypothetical, but it shows how even IO is easily > referentially transparent (as long as you don't use unsafe* cheats). > > What?? I see how a definition like this one shows how something else that you > call "IO" can be denotative & RT. I don't see how what that conclusion has to > do with Haskell's IO.
Whether you say such a beast "is" IO or "something else that you call 'IO'", I don't see the problem with positing an open GADT of this form, new constructors of which are introduced by built-in magic and/or by 'foreign import', and letting the denotation of IO be terms in the free algebraic theory on the resulting signature. It is then the job of the compiler, linker, et al, to implement a model of that algebraic theory in the machine language. Foreign imports introduce new "external names" - constructors of the GADT - and the linker connects those names to their "implementations" - giving them denotations as terms in the target machine's language. Maybe I'm missing something but, in the presence of FFI, how can the world-interfacing portion of a programming language possibly be any more denotative than that? Once you cross that threshold, I'd much rather have an operational semantics anyway. Ultimately, programming a computer is about making the computer _do_ things. No matter what sort of denotational semantics you come up with, I don't see any way to avoid it eventually "bottoming out" at some abstract representation which must then either have an operational semantics or an informal "everyone who matters knows what that means" semantics. Eventually, the denotation of anything that potentially involves interaction with the real world must be "a program" in some real or imaginary machine's language. This model chooses a very reasonable place to sever the infinite tower of turtles because it produces a language that is universal: it is the free algebra of the signature specified by the GADT. Incidentally, this model also addresses a concern I've heard voiced before that IO isn't demonstrably a monad. The whole point of IO is, as I understand it, that it is a monad _by construction_ - specifically, it is the monad whose Kleisli category is the category of contexts and substitutions in the free algebraic theory generated on this signature. There are even at least 2 published implementations of this construction in Haskell - the MonadPrompt and operational packages - and it has been shown that it does, in fact, form a monad. I would assert that if there is any sense in which the IO type _implementation_ fails to be a monad, it is a bug and not a flaw in the concept of an IO monad. > I also wonder whether you're assuming that all of the IO primitives we have > in Haskell treat their non-IO arguments denotationally/extensionally, so that > there cannot be operations like "isWHNF :: a -> IO Bool". Correct me if I'm wrong, but it appears the implication here is that [[isWHNF x]] /= [[isWHNF]] [[x]]. I don't think this is necessarily true though. Somewhere in any formal model of any language which takes the real world into account, there must be some translation from a denotational semantics to an operational one. If the denotational semantics is not computable, that translation necessarily must introduce some kind of "accidental" extra state. The denotational semantics will generally include no concept of this state, so no denotation can mention it. But I see no problem in there being a value in the denotation which is translated to an operation which does make use of this state. In this model, [[isWHNF x]] is something like "IsWHNF [[x]]", which the compiler then translates into some code that, at run time, checks the progress of the attempt to compute the denotation of x. At no point is there a term whose denotation depends on that state; instead, there is a computation which chooses how to proceed to do based on that state. This does not infect the denotation with the forbidden knowledge, it only allows you to denote operations which are aware of the mechanism by which the denotation is computed. Similarly, the operations 'peek' and 'poke' allow you to denote operations which may do unspeakably evil things at runtime, including entirely subverting that mechanism. That doesn't mean the denotation is wrong, it means the machine has a back door. Certainly it would be better, all other things being equal, if the translation did not open the back door like that but, as is so often the case, all other things are not equal. The FFI and the occasional heinous performance hack are far too useful for most people to ever consider throwing out. This may mean that my concept of Haskell does not match your definition of denotational. But if that's the case, I'm perfectly OK with that. Furthermore, I'd like to know how any real programming language actually could be. In any case, the real power of Haskell's IO model is that it gives you first class procedures and treats them on an absolutely equal footing with numbers, functions, mutable references, data structures, etc. Whether you call that "purity", "referential transparency", "denotationality", or something else, the fact is that Haskell has it and very few other languages do. Personally, I call it "nifty". -- James
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
