On 11 Nov 2010, at 08:36, Luke Palmer wrote:

On Thu, Nov 11, 2010 at 12:53 AM, Jesse Schalken wrote:

...

I have had a look at hs-plugins, but it is unclear how to derive a simple pair of functions `(a -> b) -> ByteString` and `ByteString -> Either ParseError (a -> b)`, for example, from the functionality it provides, if it is possible at all. I guess such a thing requires thorough digging into the depths of GHC, (or maybe even LLVM if an architecture independent representation is sought, but I don't know enough to say.). Perhaps this is more a question for those interested and knowledgable in Haskell compilation (and, to some extent, decompilation). If not Haskell, are there any languages which provide a simple serialization and deserialization of functions?

As far as I know, GHC has no support for this. There are issues with the idea that will come out pretty fast, such as:

(1) Those cannot be pure functions, because it differentiate denotationally equal functions. So it would have to be at least (a -> b) -> IO ByteString.

I don't think I agree, I didn't see a rule f == g => serialise f == serialise g anywhere. Bob

On Thursday 11 November 2010 4:25:46 am Thomas Davie wrote:

I don't think I agree, I didn't see a rule f == g => serialise f == serialise g anywhere.

That equal things can be substituted for one another is one of the fundamental ideas of equality (the other is that anything is equal to itself). In fact, in second order logic, equality can be *defined* as (roughly): (x = y) means (forall P. P x -> P y) That is, x is equal to y if all predicates satisfied by x are also satisfied by y. Using this, one can derive other typical laws for equality. Transitivity is pretty easy, but surprisingly, even symmetry can be gotten: If P z is z = x, using substitution we get x = x -> y = x, and x = x is trivially true. And of course, we also get congruence: Given a function f, let P z be f x = f z, substitution yields f x = f x -> f x = f y, where f x = f x is again trivial. The equality that people typically expect to hold for Haskell expressions is that two such expressions are equal if they denote the same thing, as Max said. Expressions with function type denote mathematical functions, and so if we have something like: serialize :: (Integer -> Integer) -> String it must be a mathematical function. Further, its arguments will denote functions, to, and equality on mathematical functions can be given point-wise: f = g iff forall x. f x = g x Now, here are two expressions with type (Integer -> Integer) that denote equal functions: \x -> x + x \x -> 2 * x So, for all this to work out, serialize must produce the same String for both of those. But in general, it isn't possible to decide if two functions are point-wise equal, let alone select a canonical representative for each equivalence class of expressions that denote a particular function. So there's no feasible way to implement serialize without breaking Haskell's semantics. How making serialize :: (Integer -> Integer) -> IO String solves this? Well, that's another story. -- Dan

On Thu, Nov 11, 2010 at 12:22 PM, Sjoerd Visscher wrote:

...

The equality that people typically expect to hold for Haskell expressions is that two such expressions are equal if they denote the same thing, as Max said. Expressions with function type denote mathematical functions, and so if we have something like:

 serialize :: (Integer -> Integer) -> String

it must be a mathematical function. Further, its arguments will denote functions, to, and equality on mathematical functions can be given point-wise:

 f = g iff forall x. f x = g x

Now, here are two expressions with type (Integer -> Integer) that denote equal functions:

 \x -> x + x  \x -> 2 * x

So, for all this to work out, serialize must produce the same String for both of those.

What I'm wondering is if it would actually break things if serialize would not produce the same String for these functions. The reasoning above is used regularly to shoot down some really useful functionality. So what would go wrong if we chose to take the practical path, and leave aside the theoretical issues?

Yeah, my sense -- but correct my if I'm reading the original post incorrectly -- is that the whole thing with function equality is a distraction and not really relevant here. It is true that (a) per Luke Palmer, if we could serialize equal functions to equal representations then we could we could decide whether two pure functions were equal, which (if not done in the IO monad) would(?) break purity; and (b) per Dan Doel, if we wanted to implement our serialization in a way so that equal functions get equal representations, we couldn't do it, because it's an impossible problem. But these sort of cancel each other out, because (a) it's an impossible problem, and (b) we don't want to do it. A function which does "x+x" would simply be serialized as doing x+x, and a function which does "x*2" would be serialized as doing x*2, and when deserialized the resulting functions would continue to do those things, and it would be completely agnostic and indifferent as to whether or not they are in fact equal. Obviously there are questions here with regards to the functions which the to-be-serialized function makes use of -- should they be serialized along with it? Required to be present when it is deserialized? Is it OK for the function to do something different when it is loaded compared to when it was stored if its environment is different, or not OK?

Also, the above two functions might not be exactly denotationally equal if the type is (Float -> Float), or the speed or memory use might be different. Could it not be that requiring them to be equal could just as well break things?

greetings, Sjoerd Visscher

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Work is punishment for failing to procrastinate effectively.

On Thu, Nov 11, 2010 at 2:15 PM, Jesse Schalken wrote:

2010/11/11 Gábor Lehel

...

Obviously there are questions here with regards to the functions which the to-be-serialized function makes use of -- should they be serialized along with it? Required to be present when it is deserialized? Is it OK for the function to do something different when it is loaded compared to when it was stored if its environment is different, or not OK?

I would have say Yes, No, No. At the moment, when you serialise data structure A which references data structure B which references data structure C, using Data.Binary for example, the whole lot (A, B, and C) gets serialised, so that the resulting deserialization of A is denotationally equivalent to the original, regardless of the environment. I don't see why this shouldn't be the case for functions also. So a serialized function should include all its direct and indirect callees. This might result in potentially simple functions ending up enormous when serialized, simply because the call graph, including all it's libraries and their libraries etc, is that size, but such would be pure function serialization. This raises the question of what is left. The assembled machine code? For the architecture of the serializer or of the deserializer? Or LLVM IR for architecture independence? C--? Core? I don't know, but it would be awesome for the serialized representation to be both low-level and architecture independent, then having it JIT compiled when it is deserialized. To me, this means a virtual machine, which I guess is what you need when you want fast mobile code, but I'm just musing here as I know little about programming language implementation.

I'm not an expert here either, I'll just note that LLVM is only platform independent to a degree. Or rather, I believe the situation is that it *is* architecture independent, but it doesn't abstract anything else besides the architecture -- so if you have any other differences, it's not going to work. LLVM IR doesn't do #ifdefs.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Work is punishment for failing to procrastinate effectively.

On Thu, Nov 11, 2010 at 2:29 PM, Malcolm Wallace wrote:

...

I'll just note that LLVM is only platform independent to a degree. Or rather, I believe the situation is that it *is* architecture independent, but it doesn't abstract anything else besides the architecture

In particular, imagine how you might serialise a Haskell function which is an FFI binding to some external platform-specific library (e.g. Posix, Win32, Gtk+, WPF), such that you could save it on a Windows machine, copy to Linux or Mac, and start it running again.

...and FFI imports are something you definitely can't serialize, so that's one case where you either have it say "call the linked-in function with the name 'whatever'" and hope it's the same one, or just disallow it entirely.

Regards,    Malcolm _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Work is punishment for failing to procrastinate effectively.

Dan Doel writes:

You'd lose the whole notion of 'the category of haskell types and functions' goodbye, too. Does f . id = f? Not if the former serializes as "f . id".

..and you are able to tell the difference. Am I wrong in thinking that this could be made to work if serialization was to/from an opaque type instead of (Byte)String, so that the *only* operations would be serialization and deserialization (and possibly storing to/from file)? -k -- If I haven't seen further, it is by standing in the footprints of giants

"C. McCann" writes:

This was my first thought as well! However, reading to/from a file would of course be in IO, at which point you'd be free to read the file back in through normal means to get at the representation. So in that respect, this is equivalent to (a -> b) -> IO String.

IMO, it's morally different, you're now operating on a file, and you shouldn't rely on the contents being predictable. You can make the sin-bin argument that IO can do anything, but I think there's a moral distinction between serialize :: a -> IO ByteString x <- serialize f and serialize :: a -> Opaque store :: Opaque -> FilePath -> IO () do x <- serialize f store x n B.readFile n You could probably already snarf chunks of the heap and dump them to file.

I suppose one could object that this isn't actually serializing anything at all; to which I would respond that, in pure code, how do you expect to tell the difference?

Nice one :-) I guess the real question is what are the useful, pure operations on an opaque type that can contain arbitrary functions. -k -- If I haven't seen further, it is by standing in the footprints of giants

On Nov 11, 2010, at 3:36 PM, Dan Doel wrote:

On Thursday 11 November 2010 6:22:06 am Sjoerd Visscher wrote:

...

The reasoning above is used regularly to shoot down some really useful functionality. So what would go wrong if we chose to take the practical path, and leave aside the theoretical issues?

You would lose many uses of equational reasoning in your programs. Have you every substituted 'x * 2' for the expression 'x + x' in one of your programs, or vice versa? You can no longer do that, because someone may be serializing the function you're writing, checking how it's implemented, and relying it.

Yes, but it would not break any existing code. It would only break code that knowingly did the wrong thing.

We already have a weak case of this, since (\x -> undefined x) can be distinguished from undefined using seq, but that can be hand-waved away by not worrying about bottoms so much. That isn't going to work for serialize.

Why not? -- Sjoerd Visscher http://w3future.com

On Thu, Nov 11, 2010 at 6:16 PM, Dan Doel wrote:

serialize is not at all the same in this regard. There is no class of functions that is immune to its inspection powers, presumably, because that's its whole point. But that also means that there is no class of functions for which we are justified in reasoning equationally using the standard extensional equality. The only way that would be justified is saying, "serialize doesn't exist."

Admittedly, the class of reasoning I usually use in my Haskell programs, and the one that you talked about using earlier this message, is essentially "seq doesn't exist". However, I prefer to use this class of reasoning because I would prefer if seq actually didn't exist (er, I think the implication goes the other way). Not so for serialize: I would like a serialize function, but I don't want the semantic burden it brings. If only there were a way to... oh yeah. serialize :: (a -> b) -> IO String I still don't really get what we're arguing about. Luke

On Thu, 11 Nov 2010, Dan Doel wrote:

intensional equality: two values are provably equal if they evaluate to the same normal form

extensional equality: this incorporates non-computational rules, like the point-wise equality of functions.

Now, in a type theory where equality is intensional, I cannot prove:

(forall x. f x = g x) -> f = g

However, both these equalities (and others in between and on either side) are *compatible*, in that I cannot disprove the above theorem in an intensional theory.

What seq and serialize do is break from extensional equality, and allow us to disprove the above (perhaps not for seq within a hypothetical theory, since the invalidating case involves non-termination, but certainly for serialize). And that's a big deal, because extensional equality is handy for the above reasoning about programs.

As you are well aware in Coq, and in Agda we don't have an extensionality axiom; however this is not a problem because we simply use setoid equality to capture extenional reasoning and prove that in every specific case where we want to use extensioanl reasoning it is sound to do so. Now suppose I add the following consitent axiom to Coq: Axiom Church-Turing : forall f:Nat -> Nat, exists e:Nat, forall n:Nat, {e}(n) = f(n) This well-studied axiom is effectively what serialize is realizing[1]. Now, have I broken my old Coq proofs by adding this axiom? No, of course not, because it is a consistent axioms and my proofs didn't use it. My proofs were alreay explicity proving that extentional substitution was sound in those cases I was using it. The same will be true for reasoning in Haskell. Before serialization we knew that extensional substitution was sound, but after adding serialization we are now obligated to prove in the individual cases that extensional subsitution is sound and/or add extentionally preconditions to our proofs. So no big deal; people have already been doing this in Coq and Agda for years. [1]Actaully the realizer for serialize is *weaker* that this axioms. The realizer for serialize would be (Nat -> Nat) -> IO Nat instead of (Nat -> Nat) -> Nat, so should have less impact that the Church-Turing axiom. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

It took me a bit to decide whether this was an adequate counter to my objection, but ultimately, I don't think it is. I'll try to explain as well as possible. On Friday 12 November 2010 1:40:10 pm roconnor@theorem.ca wrote:

As you are well aware in Coq, and in Agda we don't have an extensionality axiom; however this is not a problem because we simply use setoid equality to capture extenional reasoning and prove that in every specific case where we want to use extensional reasoning it is sound to do so.

If we are talking about writing programs in a closed world, and proving things about said world, this is fine. But this is not always what we are doing in Haskell. For instance, if I am writing a library, am I justified in changing: f (g x) (g x) to: let y = g x in f y y without bumping the "semantics breaking change" version number? In a closed world, where I have proved that all the relevant code I have written admits extensionality, the answer is, "yes." But in an open world, where people are free to use serialize to inspect my implementations in pure code, the answer is, "no."

Now suppose I add the following consistent axiom to Coq:

Axiom Church-Turing : forall f:Nat -> Nat, exists e:Nat, forall n:Nat, {e}(n) = f(n)

So, your argument is, if I'm not mistaken, that intensional type theory can be consistently extended with this axiom. I believe this. In fact, I'd even be willing to accept that purely as an axiom, it might be consistent to add it to extensional type theory. However, this is not the whole story. One question I have to ask is: how does this compute? In Agda, and I suspect Coq, axioms simply do not compute (and this is the reason I'd be willing to believe Church-Turing is consistent with an extensional theory). However, serialize *will* compute, and I expect it to compute like this: forall e:Nat. serialize {e} => e And I can believe that even this is consistent with intensional type theory. In an intensional theory, I can imagine (Nat -> Nat) being interpreted not as a type of functions, but as a type of algorithms. There may be many algorithms that compute the same function, and Nat -> Nat contains them all. serialize/Church-Turing returns the source code of each one. When we assert extensionality, though, Nat -> Nat can no longer be inhabited by mere algorithms, though. In an extensional theory, Nat -> Nat is a quotient of the set of algorithms. And then we have only a few options: 1) serialize/Church-Turing violates the quotient 2) serialize/Church-Turing computes extensional equality of algorithms, and chooses a single 'source code' representation for each equivalence class 3) It is impossible for two different pieces of source code to compute the same function (so serialize {e} => e is valid because there is no e' /= e such that forall x. {e} x = {e'} x) *) ... 2 is, I think, impossible, and 3 is simply false, so the choice is 1, meaning that ITT + a Church-Turing that actually computes cannot be consistently extended with extensionality. And it is this that I care about, and what I was referring to in the mail you replied to: - Intensional type theory can be consistently extended to extensional type theory. - serialize is anti-extensional (similar to the way impredicative Set and injective type constructors are anti-classical). And it is this consistent extension that I care about. And, going back to my library example, the reason to care about this is abstraction. I want clients of my library to program to the abstraction of my code as functions, not as algorithms/source code, because that allows me leeway to tweak the algorithms as I see fit, so long as they compute the same function. And, for that matter, the compiler can do this kind of mucking around with algorithms. I think it's a big deal if, to enable optimization of a function, we have to prove that all code in our program treats it extensionally (I don't believe the compiler can do it, currently, barring serialize simply not being used; and say goodbye to separate compilation).

[1]Actaully the realizer for serialize is *weaker* that this axioms. The realizer for serialize would be (Nat -> Nat) -> IO Nat instead of (Nat -> Nat) -> Nat, so should have less impact that the Church-Turing axiom.

I have no problem with serialize :: (Nat -> Nat) -> IO Nat. The problem is with (Nat -> Nat) -> Nat. The former can respect the quotient in question via IO hand waving. Perhaps this distinction is frivolous, but it seems wrong to make the language in general anti-extensional when it could instead be put inside the sin bin. My quarrel is more with, "let's dump out the sin bin and just be careful." -- Dan [*] I have seen a paper about a type theory with quotients that has a function: choose : T / R -> T such that: choose (squish x) => x but it was meticulously designed to allow that in ways that I don't really remember, so I'm going to pretend it doesn't exist at the moment.

nstance Read (F a) where read str= eval str >>= F str sorry 2010/11/11 Alberto G. Corona

There are some straighforward tricks using the package eval (or hint)l.

This is more or less the idea in pseudocode:

type FuncExpr= String

data F a = F FuncExpr a

apply (F _ f) x= f x

instance Show (F a) where show (F str _)= str

instance Read (F a) where read (F str f)= eval f >>= F str

2010/11/11 Jesse Schalken

...

Is it possible to serialize and deserialize a function to/from binary form, perhaps using Data.Binary, for example? What about an IO action? If so, is there a way the serialized representation could be architecture-independent?

I have been shown how useful it can be to store functions inside data structures, and while looking at data serialization for the purpose of persistence I wondered "since functions are just values in Haskell, why can't we persist them, too?".

To me the idea has interesting implications. For example, an arbitrary program could simply be represented by a serialization of `IO ()`. In fact, you could load any program into memory from a file and use Control.Concurrent.forkIO to run it, and later kill it, giving you the beginnings of an operating environment. If such a serialization is architecture independent then to my understanding you have the beginnings of a virtual machine. You could break your program into pieces and store them in a database and load them when needed, or even pull updates to each piece individually from down the web etc, enabling interesting methods of software distribution. It would make very cool stuff possible.

I have had a look at hs-plugins, but it is unclear how to derive a simple pair of functions `(a -> b) -> ByteString` and `ByteString -> Either ParseError (a -> b)`, for example, from the functionality it provides, if it is possible at all. I guess such a thing requires thorough digging into the depths of GHC, (or maybe even LLVM if an architecture independent representation is sought, but I don't know enough to say.). Perhaps this is more a question for those interested and knowledgable in Haskell compilation (and, to some extent, decompilation).

If not Haskell, are there any languages which provide a simple serialization and deserialization of functions?

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe