On Nov 12, 2010, at 10:40 AM, roconnor@theorem.ca wrote:
[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 don't see where IO comes in if you're dealing with pure functions. Serializing pure structures is really really easy and can be done entirely purely. The tricky part is finding a good encoding. As I said in my original message on this topic, you are embedding a compiler and interpreter into your runtime. That can be as easy as what is below, or as tricky as embedding GHC in your runtime, or anywhere in between. But you simply cannot serialize IO actions without the GHC runtime. The GHC runtime sequences IO actions in ways that depend on the unserializable environment. (Imposed) Sequencing + Concrete representation = Serialization. class Serialize a where serialize :: a -> ByteString unSerialize :: ByteString -> Maybe a -- Parsers can fail instance (Serialize a) => Serialize [a] where ... instance (Serialize a, Serialize b) => Serialize (a, b) where ... -- We can conclude that a and b must be enumerable from the requirement that -- f is recursively enumerable: instance (Serialize a, Enum a, Serialize b, Enum b) => Serialize (a -> b) where serialize f = serialize $ ( zip [minBound..maxBound] (fmap f [minBound..maxBound]) ) -- A map instance might be better: we trade some serialization time for more -- deserialization time. instance (Serialize a, Serialize b) => Serialize (Map a b) where ... instance (Enum a, Enum b, Serialize a, Serialize b) => Serialize (a -> b) where serialize f = serialize . fromList $ ( zip [minBound..maxBound] (fmap f [minBound..maxBound]) ) deserialize map = \x -> lookup x (bytestring_decode_map map) where bytestring_decode_map = ...