search

cartazio / omega

Automatically exported from code.google.com/p/omega
Other
4 stars 0 forks source link

fresh, freshen break referential transparency #78

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
See following transcript:

prompt> let b = [fresh 'a', fresh 'a']

prompt> b

['x1043,'x1044] : [Symbol]
prompt> b

['x1043,'x1044] : [Symbol]
prompt> freshen b                     

(['x1049,'x1050],[('x1043,'x1049),('x1044,'x1050)]) : 
([Symbol],[(Symbol,Symbol)])

Same input results in different values --> referential transparency broken. 
This is not acceptable in a pure language. At least (fresh, freshen) should 
live in the IO monad.

Original issue reported on code.google.com by ggr...@gmail.com on 7 Dec 2010 at 12:10

GoogleCodeExporter commented 9 years ago 
Here is a demo of how it is wrong:

prompt> let c = freshen b
...
prompt> let d = freshen b
...
prompt> (let ([c1;_],_)=c in let ([d1;_],_)=d in symbolEq c1 d1)
False : Bool

'c' and 'd' should be indistinguishable in a referentially transparent system.

For this I did not use any illegal tricks such as 'show'.

Btw. the 'Atom' family is IO-based and provides the similar functionality:
freshAtom : forall (a:*1) (b:a:*1).IO (Atom b)
sameAtom : forall (a:*1) (b:a:*1) (c:a:*1).Atom b -> Atom c -> IO (Equal b c)
swapAtom : forall (a:*1) (b:a:*1) (c:a:*1) d.Atom b -> Atom c -> d -> d

Original comment by ggr...@gmail.com on 20 Jan 2011 at 6:09