Test on identity?

classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

Test on identity?

Dušan Kolář

Dear Café,


I'm trying to build a DAG from a binary tree. I don't think there's a big trouble. Nevertheless, I do even some transformations. Thus, I would like to know it is still a DAG, not adding, accidentally, a node.


Is there any way, if I have data like


data Ex

  = Val Int

  | Add Ex Ex

 

so that I can test that some value Val i === Val i ? I mean, the pointers go to the same data box? I could do that via some IORefs, AFAIK, but I don't think it is feasible. Maybe to tune the algorithm...


Best regards,


Dusan



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Haskell - Haskell-Cafe mailing list
Hi Dusan,

containers uses pointer equality in some places:

https://github.com/haskell/containers/search?q=ptrEq&unscoped_q=ptrEq

I'd suggest to read up on reallyUnsafePtrEquality#, before you rely on
it though.

Hope that helps!
Simon

Am Mi., 8. Juli 2020 um 08:18 Uhr schrieb Dušan Kolář <[hidden email]>:

>
> Dear Café,
>
>
> I'm trying to build a DAG from a binary tree. I don't think there's a big trouble. Nevertheless, I do even some transformations. Thus, I would like to know it is still a DAG, not adding, accidentally, a node.
>
>
> Is there any way, if I have data like
>
>
> data Ex
>
>   = Val Int
>
>   | Add Ex Ex
>
>
>
> so that I can test that some value Val i === Val i ? I mean, the pointers go to the same data box? I could do that via some IORefs, AFAIK, but I don't think it is feasible. Maybe to tune the algorithm...
>
>
> Best regards,
>
>
> Dusan
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Viktor Dukhovni
In reply to this post by Dušan Kolář
On Wed, Jul 08, 2020 at 08:17:41AM +0200, Dušan Kolář wrote:

> Nevertheless, I do even some transformations. Thus, I would like to know it is still a
> DAG, not adding, accidentally, a node.
>
> Is there any way, if I have data like
>
> data Ex
>   = Val Int
>   | Add Ex Ex
>  
> so that I can test that some value Val i === Val i ? I mean, the pointers go to the
> same data box? I could do that via some IORefs, AFAIK, but I don't think it is
> feasible. Maybe to tune the algorithm...

If, for the same "n", two "distinct" leaf nodes "Val n" are possible, in
what sense is what you have still a DAG?  If there's a difference
between:

        Add
       /   \
      /     \
     /       \
    v         v
  Val 1     Val 1

and:

        Add
       /   \
      /     \
      \    /
       v  v
       Val 1

then perhaps the data model is flawed by failing to capture the
distinguishing attributes of distinct leaf objects.  And of course
you might also have:

         Add
        /   \
       /     \
       \    /
        v  v
        Add
       /   \
      /     \
     /       \
    v         v
  Val 1     Val 2

So the most portable approach would be to assign a unique serial number
all the nodes, both "Add", and "Val", and check that there's only path
from the root to each distinct node (by serial number).  Or, equivalently,
a recursive enumeration of all the serial numbers contains no duplicates.

--
    Viktor.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Dušan Kolář
Well, it makes a difference for me if I have twice the same subtree or sharing one subtree from several places. Later, I add some markers, thus, I know it is already processed or not.

Adding unique numbers and counting them makes sense if I know the result. If not then I don't know how to exploit it. But I may be tired too much already. :-(

Anyway, probably more imperative style would be a better option.

Thanks all,

Dušan


8. července 2020 18:13:34 SELČ, Viktor Dukhovni <[hidden email]> napsal:
On Wed, Jul 08, 2020 at 08:17:41AM +0200, Dušan Kolář wrote:

Nevertheless, I do even some transformations. Thus, I would like to know it is still a
DAG, not adding, accidentally, a node.

Is there any way, if I have data like

data Ex
= Val Int
| Add Ex Ex

so that I can test that some value Val i === Val i ? I mean, the pointers go to the
same data box? I could do that via some IORefs, AFAIK, but I don't think it is
feasible. Maybe to tune the algorithm...

If, for the same "n", two "distinct" leaf nodes "Val n" are possible, in
what sense is what you have still a DAG? If there's a difference
between:

Add
/ \
/ \
/ \
v v
Val 1 Val 1

and:

Add
/ \
/ \
\ /
v v
Val 1

then perhaps the data model is flawed by failing to capture the
distinguishing attributes of distinct leaf objects. And of course
you might also have:

Add
/ \
/ \
\ /
v v
Add
/ \
/ \
/ \
v v
Val 1 Val 2

So the most portable approach would be to assign a unique serial number
all the nodes, both "Add", and "Val", and check that there's only path
from the root to each distinct node (by serial number). Or, equivalently,
a recursive enumeration of all the serial numbers contains no duplicates.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Joachim Durchholz
Hi Dusan,

If you go imperative here, all code that builds on that data structure
will be imperative as well, and you'll lose much of what makes Haskell
interesting.

Try this mental model:

Step 1: Two objects are equal if all attributes are equal.
Just value equality here, i.e. assuming a language where you access all
attributes (reference or direct) through an accessor like a.x, two
objects a and b are equal if all accessor chains (e.g. x.y.z) that end
in primitive values give you primitive-equality (e.g. a.x.y.z ==
b.x.y.z, and this works for all valid accessor chains).
(As you can see, equality is not a simple concept, and in languages
where you have no primitives the definition becomes circular, but it's
good enough for the model here.)

Step 2: Define "identity" to be "equality under change".
I.e. a and b are identical that if you assign to a.x.y.z, the same value
will be found in b.x.y.z.
This "identity is equality under change" definition captures not just
two objects at identical addresses, but also proxies, network objects,
files, and whatever there is.

Step 3: Realize that if you have an immutable object, there is no
relevant difference between equality and identity anymore. (You can make
various formal statements about this.)

Step 4: So for an immutable object,
    A                                         B
   / \   is not just equal but identical to  / \
  /   \                                      \ /
x     x                                      x

Step 5: You want to be able to have
      A
     / \
    /   \
   x'    x''
after some updates.
That's not a problem! You "update" an object by creating a copy. Nothing
prevents your code from creating an A(x',x'') tree when given an A(x,x)
tree!


This train of thought helped my wrap my mind around some ideas in
Haskell; I hope it will help you, and possibly other readers.
Everybody feel free to make it even more generally helpful :-)

Regards,
Jo


Am 08.07.20 um 18:42 schrieb Dušan Kolář:

> Well, it makes a difference for me if I have twice the same subtree or
> sharing one subtree from several places. Later, I add some markers,
> thus, I know it is already processed or not.
>
> Adding unique numbers and counting them makes sense if I know the
> result. If not then I don't know how to exploit it. But I may be tired
> too much already. :-(
>
> Anyway, probably more imperative style would be a better option.
>
> Thanks all,
>
> Dušan
>
>
> 8. července 2020 18:13:34 SELČ, Viktor Dukhovni <[hidden email]>
> napsal:
>
>     On Wed, Jul 08, 2020 at 08:17:41AM +0200, Dušan Kolář wrote:
>
>         Nevertheless, I do even some transformations. Thus, I would like
>         to know it is still a
>         DAG, not adding, accidentally, a node.
>
>         Is there any way, if I have data like
>
>         data Ex
>         = Val Int
>         | Add Ex Ex
>
>         so that I can test that some value Val i === Val i ? I mean, the
>         pointers go to the
>         same data box? I could do that via some IORefs, AFAIK, but I
>         don't think it is
>         feasible. Maybe to tune the algorithm...
>
>
>     If, for the same "n", two "distinct" leaf nodes "Val n" are possible, in
>     what sense is what you have still a DAG?  If there's a difference
>     between:
>
>              Add
>             /   \
>            /     \
>           /       \
>          v         v
>        Val 1     Val 1
>
>     and:
>
>              Add
>             /   \
>            /     \
>            \    /
>             v  v
>             Val 1
>
>     then perhaps the data model is flawed by failing to capture the
>     distinguishing attributes of distinct leaf objects.  And of course
>     you might also have:
>
>               Add
>              /   \
>             /     \
>             \    /
>              v  v
>              Add
>             /   \
>            /     \
>           /       \
>          v         v
>        Val 1     Val 2
>
>     So the most portable approach would be to assign a unique serial number
>     all the nodes, both "Add", and "Val", and check that there's only path
>     from the root to each distinct node (by serial number).  Or, equivalently,
>     a recursive enumeration of all the serial numbers contains no duplicates.
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Olaf Klinke
In reply to this post by Dušan Kolář
> Dear Café,
>
> I'm trying to build a DAG from a binary tree. I don't think there's a
> big trouble.
> Nevertheless, I do even some transformations. Thus, I would like to
> know it is still a
> DAG, not adding, accidentally, a node.
>
> Is there any way, if I have data like
>
> data Ex
>   = Val Int
>   | Add Ex Ex
>  
> so that I can test that some value Val i === Val i ? I mean, the
> pointers go to the
> same data box? I could do that via some IORefs, AFAIK, but I don't
> think it is
> feasible. Maybe to tune the algorithm...
>
> Best regards,
>
> Dusan

So the binary tree is a value e :: Ex, right? And the DAG (directed
acyclic graph) is an explicit representation of the internal pointer
structure in e? Did I understand you right?
This sounds like you should represent Ex as a fixed point and then
invoke some fixed point magic like catamorphisms. Your transformation
might have to be re-written as a cata/ana/hylomorphism, too. Below is a
recipe to turn any element of any fixed point type into a graph, that
is, into a list of nodes and edges. Of course this will loop if your
data was not a finite DAG, e.g. due to self-reference.

-- make type recursion for your type Ex explicit
data ExF x = Val Int | Add x x deriving (Show)
instance Functor ExF where
    fmap f (Val i) = Val i
    fmap f (Add x y) = Add (f x) (f y)
instance Foldable ExF where
    foldMap _ (Val _) = mempty
    foldMap f (Add x y) = f x <> f y
instance Traversable ExF where
    traverse f (Val i) = pure (Val i)
    traverse f (Add x y) = Add <$> (f x) <*> (f y)

-- represent Ex via the general
-- Fix :: (* -> *) -> *
-- See e.g. package data-fix or recursion-schemes
-- cataM below taken from the data-fix package
type Ex = Fix ExF -- = Fix {unFix :: ExF (Fix ExF)}

-- Add () () tells you the node is internal
type ExNode = ExF ()

data GraphElem f = Node Int (f ()) | Edge Int Int
instance Show (GraphElem ExF) where
    show (Node n (Val i))   = show n ++ ":Val " ++ show i
    show (Node n (Add _ _)) = show n ++ ":Add"
    show (Edge i j) = show i ++ " -> " ++ show j
type Graph = [GraphElem ExF]
type GraphM = StateT Int (Writer Graph)

structure :: (Traversable f,
    MonadState Int m,
    MonadWriter [GraphElem f] m) =>          
    f Int -> m Int
structure fi = do
    this <- get
    tell [Node this (void fi)]
    traverse (\child -> tell [Edge this child]) fi
    put (this+1)
    return this

-- depth-first traversal. More generally dag has type
-- (Traversable f) => Fix f -> [GraphElem f]
-- and the Traversable instance determines the order
-- of the traversal.
dag :: Ex -> Graph
dag = snd . runWriter . flip evalStateT 0 . cataM structure

-- Cheers, Olaf

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Olaf Klinke
In reply to this post by Dušan Kolář
Joachim Durchholz wrote:

> This "identity is equality under change" definition captures not
> just
> two objects at identical addresses, but also proxies, network
> objects,
> files, and whatever there is.
>
> Step 3: Realize that if you have an immutable object, there is no
> relevant difference between equality and identity anymore. (You can
> make
> various formal statements about this.)

Is that what is called "extensional equality"? Values a,b :: A are
extensionally equal if they behave the same in all contexts. That is,
there is no type X and no function f :: A -> X such that f a can be
observed to be different from f b, e.g. f a throws an exception and f b
does not, or X is in Eq and f a /= f b.
Can one write a function (even using reallyUnsafePtrEquality#) that
distinguishes the following?
a = Add (Val 1) (Val 1)
b = let v = Val 1 in Add v v

I tried:

import GHC.Exts
peq :: a -> a -> Bool
peq x y = I# (reallyUnsafePtrEquality# x y) == 1
f :: Ex -> Bool
f (Val _) = False
f (Add x y) = peq x y

But I get (even when I make the fields of Add strict):
peq a a == True
f a == False
f b == False

Olaf

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Zemyla
A safer way of doing object identity is with System.StableName.

On Thu, Jul 9, 2020, 13:27 Olaf Klinke <[hidden email]> wrote:
Joachim Durchholz wrote:
> This "identity is equality under change" definition captures not
> just
> two objects at identical addresses, but also proxies, network
> objects,
> files, and whatever there is.
>
> Step 3: Realize that if you have an immutable object, there is no
> relevant difference between equality and identity anymore. (You can
> make
> various formal statements about this.)

Is that what is called "extensional equality"? Values a,b :: A are
extensionally equal if they behave the same in all contexts. That is,
there is no type X and no function f :: A -> X such that f a can be
observed to be different from f b, e.g. f a throws an exception and f b
does not, or X is in Eq and f a /= f b.
Can one write a function (even using reallyUnsafePtrEquality#) that
distinguishes the following?
a = Add (Val 1) (Val 1)
b = let v = Val 1 in Add v v

I tried:

import GHC.Exts
peq :: a -> a -> Bool
peq x y = I# (reallyUnsafePtrEquality# x y) == 1
f :: Ex -> Bool
f (Val _) = False
f (Add x y) = peq x y

But I get (even when I make the fields of Add strict):
peq a a == True
f a == False
f b == False

Olaf

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Viktor Dukhovni
On Thu, Jul 09, 2020 at 03:12:47PM -0500, Zemyla wrote:

> A safer way of doing object identity is with System.StableName.

Minor correction: System.Mem.StableName

    https://hackage.haskell.org/package/base-4.14.0.0/docs/System-Mem-StableName.html

with the internals in:

    https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-StableName.html

--
    Viktor.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Carter Schonwald
Stable names are great! 

 And similar packages on hackage are a pure interfsce for them. I think they’re also used in eds ersatz package sortah. 

On Thu, Jul 9, 2020 at 4:23 PM Viktor Dukhovni <[hidden email]> wrote:
On Thu, Jul 09, 2020 at 03:12:47PM -0500, Zemyla wrote:

> A safer way of doing object identity is with System.StableName.

Minor correction: System.Mem.StableName

    https://hackage.haskell.org/package/base-4.14.0.0/docs/System-Mem-StableName.html

with the internals in:

    https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-StableName.html

--
    Viktor.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Joachim Durchholz
In reply to this post by Olaf Klinke
Am 09.07.20 um 20:26 schrieb Olaf Klinke:

> Joachim Durchholz wrote:
>> This "identity is equality under change" definition captures not
>> just
>> two objects at identical addresses, but also proxies, network
>> objects,
>> files, and whatever there is.
>>
>> Step 3: Realize that if you have an immutable object, there is no
>> relevant difference between equality and identity anymore. (You can
>> make
>> various formal statements about this.)
>
> Is that what is called "extensional equality"? Values a,b :: A are
> extensionally equal if they behave the same in all contexts.

To fully treat this, you have to explore some pretty interesting waters.

First, "all contexts" can mean pretty different things.
E.g. in Haskell (without unsafe* and similar), everything is immutable,
so you have contexts that exist in languages with mutability but not in
Haskell, and you'd have to define what "all contexts" means for a
general term like "extensional equality".

Second, "behave the same" means that for all functions, the result it equal.
That's a recursive definition. You need fixed-point theory to turn that
statement into an actual definition.
And that's surprisingly tricky.

One fixed point is to say "the largest set of equal objects", which
means everything is equal to everything - fits the above definition
(applying any function to anything will trivially return results that
are equal under this definition), but is obviously not what we wanted.

Another one would be to have what we'd intuitively define as equality.
Say, in Haskell, the minimum set of equalities that makes different
constructor calls unequal. (Plus a handful of clerical definitions to
catch special cases like integers.)

Another one would be to have what we'd intuitively define as identity.

Plus various other fixed points.

For example, consider proxies - say, an object that talks to a remote
machine to produce its function results.
Now if you assume a proxy for integer values, is the proxy equal to an
arbitrary integer you may have locally?
Again, this depends on what fixed point you choose for your equality
definition. You can define that as an exception, you consider two
objects equal if their functions return equal results, except for those
that inspect the proxy-specific state; then proxy and local value are
equal. Or you don't make an exception, then the two are not equal.
 From a mathematical standpoint, either fixed point will satisfy the
above recursive definition (definition template, if you will). From a
computing standpoint, you'll find that depending on context, you want
one or the other!

There are different types of proxy objects, and you can have different
kinds of equality depending on how you treat them.

That multitude of equality functions is pretty useless in a programming
context; nobody wants to mentally deal with a gazillion of subtly
different equalities!
So I belive what one should do in practice is to have converter
functions. E.g. one that turns an Int proxy into an Int, merely by
stripping the proxy-specific functions.
That keeps the special cases to the place where they belong - all those
types that have funky special kinds of equality.
Mutable data is another case of this. The equality of a mutable object
can be defined as identity, and a converter function returns an
immutable copy so that equality is what's usually considered "value
equality" (equals() in Java).
(Languages that do not cleanly separate mutable and immutable types will
still have to deal with two equalities, value equality and identity...
well, the above is type and language design theory, practical languages
are always a set of trade-offs, restricted by the limited knowledge and
experience of the language designer. I guess that's why we have so many
programming languages.)

Regards,
Jo
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Johannes Waldmann-2
In reply to this post by Dušan Kolář
> Stable names are great! ...
> I think they’re also used in eds ersatz package sortah.

Yes.

This is the package
https://hackage.haskell.org/package/ersatz

This is where they are used
https://github.com/ekmett/ersatz/blob/master/src/Ersatz/Problem.hs#L149

- J.W.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Test on identity?

Olaf Klinke
In reply to this post by Dušan Kolář
> Am 09.07.20 um 20:26 schrieb Olaf Klinke:
> > Joachim Durchholz wrote:
> >> This "identity is equality under change" definition captures not
> >> just
> >> two objects at identical addresses, but also proxies, network
> >> objects,
> >> files, and whatever there is.
> >>
> >> Step 3: Realize that if you have an immutable object, there is no
> >> relevant difference between equality and identity anymore. (You
> can
> >> make
> >> various formal statements about this.)
> >
> > Is that what is called "extensional equality"? Values a,b :: A are
> > extensionally equal if they behave the same in all contexts.
>
> To fully treat this, you have to explore some pretty interesting
> waters.
>
> First, "all contexts" can mean pretty different things.
> E.g. in Haskell (without unsafe* and similar), everything is
> immutable,
> so you have contexts that exist in languages with mutability but not
> in
> Haskell, and you'd have to define what "all contexts" means for a
> general term like "extensional equality".
>
> Second, "behave the same" means that for all functions, the result it
> equal.
> That's a recursive definition. You need fixed-point theory to turn
> that
> statement into an actual definition.
> And that's surprisingly tricky.
>
> One fixed point is to say "the largest set of equal objects", which
> means everything is equal to everything - fits the above definition
> (applying any function to anything will trivially return results
> that
> are equal under this definition), but is obviously not what we
> wanted.
>
> Another one would be to have what we'd intuitively define as
> equality.
> Say, in Haskell, the minimum set of equalities that makes different
> constructor calls unequal. (Plus a handful of clerical definitions
> to
> catch special cases like integers.)
>
> Another one would be to have what we'd intuitively define as
> identity.
>
> Plus various other fixed points.
>
> For example, consider proxies - say, an object that talks to a
> remote
> machine to produce its function results.
> Now if you assume a proxy for integer values, is the proxy equal to
> an
> arbitrary integer you may have locally?
> Again, this depends on what fixed point you choose for your equality
> definition. You can define that as an exception, you consider two
> objects equal if their functions return equal results, except for
> those
> that inspect the proxy-specific state; then proxy and local value
> are
> equal. Or you don't make an exception, then the two are not equal.
>  From a mathematical standpoint, either fixed point will satisfy the
> above recursive definition (definition template, if you will). From
> a
> computing standpoint, you'll find that depending on context, you
> want
> one or the other!
>
> There are different types of proxy objects, and you can have
> different
> kinds of equality depending on how you treat them.
>
> That multitude of equality functions is pretty useless in a
> programming
> context; nobody wants to mentally deal with a gazillion of subtly
> different equalities!
> So I belive what one should do in practice is to have converter
> functions. E.g. one that turns an Int proxy into an Int, merely by
> stripping the proxy-specific functions.
> That keeps the special cases to the place where they belong - all
> those
> types that have funky special kinds of equality.
> Mutable data is another case of this. The equality of a mutable
> object
> can be defined as identity, and a converter function returns an
> immutable copy so that equality is what's usually considered "value
> equality" (equals() in Java).
> (Languages that do not cleanly separate mutable and immutable types
> will
> still have to deal with two equalities, value equality and
> identity...
> well, the above is type and language design theory, practical
> languages
> are always a set of trade-offs, restricted by the limited knowledge
> and
> experience of the language designer. I guess that's why we have so
> many
> programming languages.)
>

I find it easier to intuitively define what extensional inequality
means: As a domain theorist I declare two values unequal if there is an
open set (a semi-decidable property) containing one but not the other
value. For pure types t (not involving IO) that means there is a
function
semidecide :: t -> ()
that returns () for the one value and bottom for the other. I can not
say how this would extend to impure types and I tend to agree with you
that the notion of equality then depends on the intended semantics.
Below the semidecision would have type t -> I0 ()

However, using StableName (thanks, Zemyla and Viktor!) indeed one is
able to detect sharing. It works only after forcing the values, though.
Apparently StableName does not work on thunks.

Olaf

ghci> import System.Mem.StableName
ghci> import  Control.Applicative
ghci> data Ex = Val Int | Add Ex Ex deriving (Show)
ghci> a = Add (Val 1) (Val 1)
ghci> b = let v = Val 1 in Add v v
ghci> show a
"Add (Val 1) (Val 1)"
ghci> show b
"Add (Val 1) (Val 1)"
ghci> let f :: Ex -> IO Bool; f (Val _) = return False; f (Add x y) =
liftA2 eqStableName (makeStableName x) (makeStableName y)
ghci> f a
False
ghci> f b
True

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.