On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean 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

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 3:21 AM, Jules Bean 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

On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer wrote: 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 ==============================================================================

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 wrote:

...

On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean 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

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 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 wrote:

...

On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean 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

Hi all, On Wed, Nov 12, 2008 at 2:09 PM, 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.

...

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 monomorphic type. In the interpretation of 'let', and of top-level definitions, on the other hand, we don't have 'mono' -- we update the environment with an OverloadedValue. I was surprised to have the "lambda arguments are monomorphic" rule from the Hindley-Milner system forced upon me like that! :-) * Neil's example, (show (f [])) where either f = id :: [Int] -> [Int] or f = id :: [Char] -> [Char], is taken care of straight-forwardly. The interpretation of f = (id :: [Int] -> [Int]]) is bottom at all types except [Int] -> [Int]; therefore, (f []) is bottom at all types except [Int]; therefore, in the join over all possible types in the application (show (f [])), only the type ([Int] -> String) of show is actually used. Comments? Problems? [ I hope *somebody* is actually going to read this mail -- I don't have the time to make it less confusing, sorry :-( ] Thanks, - Benja

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 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 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

On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson 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) david@mel:~$ ./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).

david.maciver:

On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson 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)

david@mel:~$ ./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.

On Wed, 2008-11-12 at 23:02 +0000, David MacIver wrote:

On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart wrote:

...

david.maciver:

...

On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson 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)

david@mel:~$ ./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

On Wed, 2008-11-12 at 23:18 +0000, David MacIver wrote:

On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast wrote:

...

On Wed, 2008-11-12 at 23:02 +0000, David MacIver wrote:

...

On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart wrote:

...

david.maciver:

...

On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson 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)

david@mel:~$ ./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

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

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