Re: [Haskell-cafe] Proof that Haskell is RT
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) deterministic --- but is, regardless, definitely not causal. Sure, it's weird if you actually know how it's allegedly making its decisions (predicting the future, but not really). But all you can actually observe is that sometimes it gives (1,1), and sometimes it gives (2,1), and maybe it coincidentally always seems to give (1,1) to f, but to g, which is observationally equal to g, excepting bottoms, it always seems to give (2,1). That's a weird situation, but if you make things opaque enough, I think you can fall back on IO's nondeterminism. Another weird situation (it seems to me) goes like: foo = unsafeInterleaveIO $ fail foo do x - foo putStrLn bar return $! x where you can't simply fall back to saying, foo throws an exception, because it doesn't prevent bar from printing. So what is actually throwing an exception is some later IO action that doesn't have any relation to foo besides using a 'pure' result from it. However, I suppose you can push off such oddities in a similar way, saying that IO actions can throw delayed, asynchronous exceptions, and what do you know, it always happens to end up in the action that evaluated x. :) Of course, those sorts of explanations might be good enough to conclude that unsafeInterleaveIO doesn't break referential transparency, but they may make for a very poor operational semantics of IO and such. foo throws some delayed asynchronous exception? Well, that doesn't tell when or how. And it doesn't explain how weirdTuple 'nondeterministically' chooses between (1,1) and (2,1). So that would probably lead you to another semantics (a more operational one) that brings up how weirdTuple reads the future, or even that mutation happens as a result of evaluating pure values. But, the point is, I think, that such a semantics doesn't indicate that referential transparency is being violated (which would be a notion from another sort of semantics where there's no way to notice something weird is going on). Anyhow, I'm done rambling. (Hope it didn't go on too long; I know we weren't fundamentally in any kind of disagreement.) :) Cheers, -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Proof that Haskell is RT
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 all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? (I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this) Andrew -- - http://www.nobugs.org - ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 inference/checking and translates Haskell into a different form that has resolved all overloading. And, secondly, you can write a dynamic semantics for that language. But since the semantics has to have the type inference engine inside it, it's going to be a pain. 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. This has been done. For example, check out the type class semantics given in Thatte, Semantics of type classes revisited, LFP '94 Stuckey and Sulzmann, A Theory of Overloading, TOPLAS'05 Harrison: A Simple Semantics for Polymorphic Recursion. APLAS 2005 is also related I think. The ICFP'08 poster Unified Type Checking for Type Classes and Type Families , Tom Schrijvers and Martin Sulzmann suggests that a type-passing semantics can even be programmed by (mis)using type families. - Martin -- Lennart On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer [EMAIL PROTECTED] wrote: 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 counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Proof that Haskell is RT
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 type [Int] or [Char] - you get different results. Without computing the types everywhere, I don't see how you can determine the precise type of []. Thanks Neil On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer [EMAIL PROTECTED] wrote: 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 counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe == Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html == ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
-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, using them in C switch statements for overloading, but I don't know if an implementation like that is really what we would need for this. - - Jake -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.8 (Darwin) iEYEARECAAYFAkka6LcACgkQye5hVyvIUKnlfwCgmpcvghHK9lYd3XwK7sfwARnM xlYAoLXxw3sz4CNaThaNV9GGsX4ALR/L =0q26 -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Referential transparency would be an obvious property of the semantics. Soundness would show that it carried over to the language. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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, Philip Wadler, Martin Wehr: A Second Look at Overloading. FPCA 1995: Roughly, the restriction says, you can overload the argument but not the result (types). - Martin Lennart Augustsson wrote: 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 I misunderstood what you're doing? What I meant hasn't been done is a one step semantics directly in terms of the source language. I guess I also want it to be compositional, which I think is where things break down. -- Lennart On Wed, Nov 12, 2008 at 2:26 PM, Martin Sulzmann [EMAIL PROTECTED] wrote: 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 inference/checking and translates Haskell into a different form that has resolved all overloading. And, secondly, you can write a dynamic semantics for that language. But since the semantics has to have the type inference engine inside it, it's going to be a pain. 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. This has been done. For example, check out the type class semantics given in Thatte, Semantics of type classes revisited, LFP '94 Stuckey and Sulzmann, A Theory of Overloading, TOPLAS'05 Harrison: A Simple Semantics for Polymorphic Recursion. APLAS 2005 is also related I think. The ICFP'08 poster Unified Type Checking for Type Classes and Type Families , Tom Schrijvers and Martin Sulzmann suggests that a type-passing semantics can even be programmed by (mis)using type families. - Martin -- Lennart On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer [EMAIL PROTECTED] wrote: 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 counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 I misunderstood what you're doing? What I meant hasn't been done is a one step semantics directly in terms of the source language. I guess I also want it to be compositional, which I think is where things break down. -- Lennart On Wed, Nov 12, 2008 at 2:26 PM, Martin Sulzmann [EMAIL PROTECTED] wrote: 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 inference/checking and translates Haskell into a different form that has resolved all overloading. And, secondly, you can write a dynamic semantics for that language. But since the semantics has to have the type inference engine inside it, it's going to be a pain. 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. This has been done. For example, check out the type class semantics given in Thatte, Semantics of type classes revisited, LFP '94 Stuckey and Sulzmann, A Theory of Overloading, TOPLAS'05 Harrison: A Simple Semantics for Polymorphic Recursion. APLAS 2005 is also related I think. The ICFP'08 poster Unified Type Checking for Type Classes and Type Families , Tom Schrijvers and Martin Sulzmann suggests that a type-passing semantics can even be programmed by (mis)using type families. - Martin -- Lennart On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer [EMAIL PROTECTED] wrote: 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 counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? (I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this) Answering this question, or actually even formalizing the statement you want to prove, is more or less equivalent to writing down a full denotational candidate semantics for Haskell in a compositional style, and proving that it is equivalent to the *actual* semantics of Haskell Nobody has done this. Well, there is no *actual* semantics anywhere around to which you one could prove equivalence. So, to be precise, the question you are interested in cannot even really be asked at the moment. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 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 all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? (I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this) Andrew -- - http://www.nobugs.org - ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? (I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this) I think the informal proof goes along the lines of because that's what the spec says -- Haskell's operational semantics are not specified in the report, only IIRC a wooly description of having some sort of non-strict beta-reduction behavior. Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 program; almost all use unsafePerformIO intentionally. That said, the situations in which these functions are RT are not that hard to meet, but they would muddy up any formal proof significantly. Personally, I'm happy with the hand-wavy proof that goes like this: 1) pure functions don't have side effects. 2) side-effect free functions can be duplicated or shared without affecting the results of the program that uses them (in the absence of considerations of resource limitation like running out of memory) 3) any function that only uses other pure functions is pure 4) all Haskell98 functions that don't use unsafe* are pure 5) therefore Haskell98 minus unsafe functions is referentially transparent. Note that I am including I/O actions as pure when observed as the GHC implementation of IO a ~~ World - (World, a); the function result that is the value of main is pure. It is only the observation of that function by the runtime that causes side effects. -- ryan On Wed, Nov 12, 2008 at 2:11 AM, Andrew Birkett [EMAIL PROTECTED] 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 all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? (I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this) Andrew -- - http://www.nobugs.org - ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 there's some more direct approach that represents types as some kind of runtime values, but nobody (to my knowledge) has done that. It seems to me that if you don't need your semantics to do the work of type-*checking* (i.e., you don't care if the rules assign some strange denotation to an ill-typed term), there is a natural approach to giving semantics to 98-style type classes. I'm figuring out the details as I type, though; if anybody sees anything that does not work, please do tell! Let type mean a non-overloaded type expression (i.e., not containing variables). I'll suppose that you already know the set of types in the program and the domain associated with each type. (This is usual in denotational treatments, right?) Let the domains be such that all sets of elements have a join (i.e., complete lattices). Define the domain of overloaded values to be the domain of functions from types to values of these types or bottom (when I say bottom in the following, it is this bottom, which is below the domain's bottom), i.e., the product of the liftings of the domains of all possible types. The interpretation of bottom is, this overloaded value doesn't have an instance at this type (e.g., [7,9] is bottom at type Bool). An *environment* is a function from symbols to overloaded values. The denotation of an expression is a function from environments to overloaded values; the denotation of a definition list is a function from environments to environments; the denotation of a whole program is the least fixed point of the definition list that makes up the program. Expressions are interpreted as follows (update :: Symbol - OverloadedValue - Environment - Environment is defined in the natural way): [[x]] = \env type. env x type [[T :: TYPE]] = \env type. if type instance of TYPE then [[T]] env type else bottom [[F X]] = Join_type2. \env type1. [[F]] env (type1 - type2) $ [[X]] env type2 [[\x. T]] = \env type. case type of (type1 - type2) - \val. [[T]] (update x (mono type1 val) env) type2 otherwise - bottom where mono ty val = \ty'. if ty == ty' then val else bottom [[let x=S in T]] = \env type. [[T]] (fix $ \env'. update x ([[S]] env') env) type Simple definitions are interpreted in the obvious way: [[x = T]] = \env sym. if sym == x then ([[T]] env) else (env sym) [[x :: Ty; x = T]] = [[x = T :: Ty]] Finally, instance declarations are interpreted in a special way. To interpret the declaration instance C Ty1 .. Tyn where ...; xi = Ti; ... we need to know the set of possible types for xi. (No type inference should be necessary -- the class declaration + the Ty1 .. Tyn from the instance declaration should give us all the necessary information, right?) Call this set Types. Then, [[xi = Ti]] = \env sym type. if sym == xi type in Types then [[T]] env type else env sym type That is, an instance declaration sets the value of a symbol at some types, and leaves the values at the other types alone. Some notes: * If T is a well-typed term and type is *not* a type instance of that term, then ([[T]] env type) is bottom. * In particular, [[T :: TYPE]] env type = [[T]] env type, when type is an instance of TYPE; otherwise, [[T :: TYPE]] env type = bottom. * Application is supposed to be strict in bottom: bottom x = bottom; f bottom = bottom. * In interpreting [[F X]], we take the join over all possible types of X (type2). If X is monomorphic, then ([[X]] env type2) is bottom for all types except the correct one, so the join gives the correct denotation. If X is polymorphic, but the type of F together with the type forced by the context of (F X) together determine what type of X must be used, then either ([[F]] env (type1 - type2)) or ([[X]] env type2) will be bottom for every type2 exept for the one we want to use; so the application ([[F]] ... $ [[X]] ...) will be bottom except for the correct type; so again, the join will give the correct denotation. (Caveat lector: I haven't proved this, I'm running on intuition :)) * In the interpretation of expressions like (show (read 5)), the join is non-degenerate: it consists of the join of 5, 5.0 etc. But since such expressions are rejected by the type-checker, we don't care. * Lets containing multiple definitions can be translated as in the Haskell report, if we add an interpretation for a case construct (I'm too lazy to try): http://www.haskell.org/onlinereport/exps.html#sect3.12 * In the interpretation of the lambda expression, we need to interpret the body of the expression separately for every type of the lambda expression; the function 'mono' converts the monomorphic parameter value into an OverloadedValue that is bottom everywhere except at the
Re: [Haskell-cafe] Proof that Haskell is RT
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 the file. The unsafePerformIO function can break RT, but I think everyone is aware of that. :) -- Lennart On Wed, Nov 12, 2008 at 6:47 PM, Ryan Ingram [EMAIL PROTECTED] wrote: 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 program; almost all use unsafePerformIO intentionally. That said, the situations in which these functions are RT are not that hard to meet, but they would muddy up any formal proof significantly. Personally, I'm happy with the hand-wavy proof that goes like this: 1) pure functions don't have side effects. 2) side-effect free functions can be duplicated or shared without affecting the results of the program that uses them (in the absence of considerations of resource limitation like running out of memory) 3) any function that only uses other pure functions is pure 4) all Haskell98 functions that don't use unsafe* are pure 5) therefore Haskell98 minus unsafe functions is referentially transparent. Note that I am including I/O actions as pure when observed as the GHC implementation of IO a ~~ World - (World, a); the function result that is the value of main is pure. It is only the observation of that function by the runtime that causes side effects. -- ryan On Wed, Nov 12, 2008 at 2:11 AM, Andrew Birkett [EMAIL PROTECTED] 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 all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? (I was writing a blog post about the origins of the phrase 'referentially transparent' and it made me think about this) Andrew -- - http://www.nobugs.org - ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 the semantics of id, but has either the return type [Int] or [Char] - you get different results. Without computing the types everywhere, I don't see how you can determine the precise type of []. Surely all this means is that part of the semantics of Haskell is the semantics of the type system -- isn't this expected? Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 from the same program could, in principle, happen if a different program wrote the file. Yes, I was thinking about this on my way to work and thought that I may have spoken too soon; I couldn't come up with a way for unsafeInterleaveIO to break referential transparency (although I couldn't prove to myself that it couldn't, either). Your argument seems good to me, though. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 Haskell into a different form that has resolved all overloading. And, secondly, you can write a dynamic semantics for that language. But since the semantics has to have the type inference engine inside it, it's going to be a pain. 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. -- Lennart On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer [EMAIL PROTECTED] wrote: 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 counter-examples but that's a bit handy-wavy. Is there a formal proof that, for all possible haskell programs, we can replace coreferent expressions without changing the meaning of a program? The (well, a natural approach to a) formal proof would be to give a formal semantics for haskell. Haskell 98 does not seem that big to me (it's not teeny, but it's nothing like C++), yet we are continually embarrassed about not having any formal semantics. What are the challenges preventing its creation? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 interesting. For what it's worth, the blog posts I was writing are here: http://www.nobugs.org/blog/archives/2008/11/12/why-do-they-call-it-referentially-transparent/ http://www.nobugs.org/blog/archives/2008/11/12/why-do-they-call-it-referentially-transparent-ii/ Andrew ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 functions yield different results depending on their evaluation order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). It seems that this argument depends on being able to find a case where w1 and swap w1 actually behave differently. weirdTuple is non-deterministic, but that's fine, since it's in the IO monad. And w1 and w2 are simply two (distinct!) lambda-bound variables; there is no requirement that two different lambda-bound variables behave in the same fashion, regardless of how values may be expected to be supplied for them at run time (what values the functions in question may be expected to be applied to) unless the function(s) they are formal parameters of are (both) applied to the same expression. (=) certainly does not count as `application' for present purposes. Even if it is insisted (why? I don't think GHC actually guarantees to produce the above result when main is executed) that main must always yield the above result, it does not follow that unsafePerformIO is non-RT; it is still only non-causal. But referential transparency doesn't require that the result of an IO action must depend only on events that transpire by the time it finishes running; it places, in fact, no requirement on the run-time behavior of any IO action at all. It requires only that equal expressions be substitutable for equals; and, again, w1 and w2 being the result of calling a single IO action with no dependence on the outside world does not require them to be equal, under any system of semantics. So, no violation of RT. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 depending on their evaluation order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). Mmmm? No. Where's the pure function that's now producing different results? I only see IO actions at play, which are operating on the state of the world. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 when passed to ostensibly pure functions yield different results depending on their evaluation order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). Mmmm? No. Where's the pure function that's now producing different results? I only see IO actions at play, which are operating on the state of the world. I suppose so. The point is that you have a pure function (show) and the results of evaluating it totally depend on its evaluation order. But you're still in the IO monad at this point so I suppose it technically doesn't count because it's only observable as the result of IO. It's pretty suspect behaviour, but not actually a failure of referential transparency. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 view. Really? It seems easy to create things with it which when passed to ostensibly pure functions yield different results depending on their evaluation order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). Mmmm? No. Where's the pure function that's now producing different results? I only see IO actions at play, which are operating on the state of the world. I suppose so. The point is that you have a pure function (show) and the results of evaluating it totally depend on its evaluation order. Sure. But only because the argument to it depends on its evaluation order, as well. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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] 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 order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). Mmmm? No. Where's the pure function that's now producing different results? I only see IO actions at play, which are operating on the state of the world. I suppose so. The point is that you have a pure function (show) and the results of evaluating it totally depend on its evaluation order. Sure. But only because the argument to it depends on its evaluation order, as well. That's not really better. :-) 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 due to exception handling. Our three main weapons...). In the presence of unsafeInterleaveIO this property is lost even though referential transparency is retained. Anyway, I'll shut up now. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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, 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 order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). Mmmm? No. Where's the pure function that's now producing different results? I only see IO actions at play, which are operating on the state of the world. I suppose so. The point is that you have a pure function (show) and the results of evaluating it totally depend on its evaluation order. Sure. But only because the argument to it depends on its evaluation order, as well. That's not really better. :-) I never said it was. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 view. Really? It seems easy to create things with it which when passed to ostensibly pure functions yield different results depending on their evaluation order: module Main where import System.IO.Unsafe import Data.IORef main = do w1 - weirdTuple print w1 w2 - weirdTuple print $ swap w2 swap (x, y) = (y, x) weirdTuple :: IO (Int, Int) weirdTuple = do it - newIORef 1 x - unsafeInterleaveIO $ readIORef it y - unsafeInterleaveIO $ do writeIORef it 2 return 1 return (x, y) [EMAIL PROTECTED]:~$ ./Unsafe (1,1) (1,2) So show isn't acting in a referentially transparent way: If the second part of the tuple were evaluated before the first part it would give a different answer (as swapping demonstrates). Mmmm? No. Where's the pure function that's now producing different results? I only see IO actions at play, which are operating on the state of the world. I suppose so. The point is that you have a pure function (show) and the results of evaluating it totally depend on its evaluation order. But you're still in the IO monad at this point so I suppose it technically doesn't count because it's only observable as the result of IO. It's pretty suspect behaviour, but not actually a failure of referential transparency. Indeed. There's a difference between purity and referential transparency. A lack of purity is when behaviour, as in semantics, depends on evaluation order (modulo bottom of course). Referential transparency is being able to substitute equals for equals. These notions are related but independent. Examples of failures of referential transparency that aren't failures of purity are easy to find. A simple one would be some kind of introspection feature, such as various forms of quotation, being able to ask for the name of a variable, being able to serialize functions. So purity doesn't imply referential transparency. Failures of purity that aren't failures of referential transparency are a bit trickier since without purity (i.e. evaluation order independence) what constitutes a valid substitution may vary. Still, as an easy start, a language with no binding forms is trivially referentially transparent regardless of how impure it may be. If you use a call-by-name evaluation order, the full beta rule holds and evaluation proceeds by substituting equals for equals and therefore such a language is also referentially transparent. So referential transparency doesn't imply purity. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 due to exception handling. Our three main weapons...). In the presence of unsafeInterleaveIO this property is lost even though referential transparency is retained. I'm not sure what exactly you mean by this, but, for instance: randomIO = (print :: Int - IO ()) obviously isn't going to give the same results as: randomIO = (print :: Int - IO ()) every time. Your weirdTuple is semantically similar, in that it selects between returning (1,1) and (2,1), but instead of being random, it operationally selects depending on how you subsequently evaluate the value. That may not seem like the same thing, because you know what's going on, but formally, I imagine you can treat it all as a black box where either this time it gave (2,1) or this time it gave (1,1), and what you see is always consistent. The fact that it sort of uses an oracle to see what will happen in its future is just The Power of IO (it does have a sort of spooky action feel to it). :) -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 equivalent in the IO monad (actually this may not be true due to exception handling. Our three main weapons...). In the presence of unsafeInterleaveIO this property is lost even though referential transparency is retained. I'm not sure what exactly you mean by this, but, for instance: randomIO = (print :: Int - IO ()) obviously isn't going to give the same results as: randomIO = (print :: Int - IO ()) every time. Your weirdTuple is semantically similar, in that it selects between returning (1,1) and (2,1), but instead of being random, it operationally selects depending on how you subsequently evaluate the value. 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) deterministic --- but is, regardless, definitely not causal. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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 you have something to compare it against. -- Lennart On Thu, Nov 13, 2008 at 12:05 AM, Jonathan Cast [EMAIL PROTECTED] wrote: 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 equivalent in the IO monad (actually this may not be true due to exception handling. Our three main weapons...). In the presence of unsafeInterleaveIO this property is lost even though referential transparency is retained. I'm not sure what exactly you mean by this, but, for instance: randomIO = (print :: Int - IO ()) obviously isn't going to give the same results as: randomIO = (print :: Int - IO ()) every time. Your weirdTuple is semantically similar, in that it selects between returning (1,1) and (2,1), but instead of being random, it operationally selects depending on how you subsequently evaluate the value. 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) deterministic --- but is, regardless, definitely not causal. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
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: http://www.nobugs.org/blog/archives/2008/11/12/why-do-they-call-it-referentially-transparent/ http://www.nobugs.org/blog/archives/2008/11/12/why-do-they-call-it-referentially-transparent-ii/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
