[Haskell-cafe] Explicitly calling syntactic equality on datatypes

[Sylvain Henry]

Hi,

The usual (cumbersome) solution would be to use a newtype wrapper. 
Something like:

```

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}

import Data.Coerce

data Sum
    = Value Int
    | Sum Sum Sum
    deriving stock Eq
    deriving stock Show

normalize :: Sum -> Sum
normalize (Value i)                 = Value i
normalize (Sum (Value i) b)         = Sum (Value i) (normalize b)
normalize (Sum (Sum x y) b)         = normalize (Sum x (Sum y b))


-- | Normalized sum
newtype NSum
    = NSum Sum
    deriving Show via Sum

instance Eq NSum where
    NSum a == NSum b = normalize a == normalize b


sample1 :: Sum
sample1 = Value 10 `Sum` (Value 11 `Sum` Value 12)

sample2 :: Sum
sample2 = (Value 10 `Sum` Value 11) `Sum` Value 12

sample1' :: NSum
sample1' = coerce sample1

sample2' :: NSum
sample2' = coerce sample2

test1 = sample1 == sample2

test2 = sample1' == sample2'

```


It would be interesting to combine DerivingVia and DerivingStrategies to 
allow what you want:

```
data Sum
    = Value Int
    | Sum Sum Sum
    deriving stock Eq via normalize

```

It would require a GHC proposal though (and some more thinking).

Sylvain


On 17/09/2019 15:56, Juan Casanova wrote:
> Hello,
>
> Pretty simple question here really. I think I've searched for it 
> several times in the past and ended up surprised I did not find an 
> answer.
>
> Simple example: sum expressions.
>
> One way to define this, one that is comfortable to construct new sums, 
> would be:
>
> data Sum = Value Int | Sum Sum Sum
>
> Another one, one that is comfortable to check equality with (and other 
> similar things that rely on some notion of normal form), would be 
> (essentially non-empty lists of ints):
>
> data Sum = Value Int | Sum Int Sum
>
> Now, in many cases you really want to go with the first one for 
> several reasons. You just do not care about normalization in most 
> cases, or maybe you do something more abstract and complicated on top 
> of it that delays the possibility or the sensibility of normalization 
> until something else happens later. So say, that I have the first 
> definition.
>
> But then, I want to define equality semantically. An obvious way to go 
> is to produce a function that normalizes Sums (from the first 
> definition) to guarantee that the first sub-sum is always going to be 
> a value, and then check that these two are "equal".
>
> And this is where my question comes in, because, of course, the 
> following is infinite recursion:
>
> instance Eq Sum where a == b = (normalize a) == (normalize b)
>
> What I'd like is to be able to override the default implementation of 
> Eq, but be able to *explicitly* call syntactic equality in calculating 
> it, so that I can do:
>
> instance Eq Sum where a == b = (syntacticEq (normalize a) (normalize b))
>
> So, I can see how this is not as straightforward as a function. You 
> cannot correctly produce a polymorphic function syntacticEq :: a -> a 
> -> Bool that works on the SYNTAX of a because it is hidden inside the 
> polymorphic function. What (deriving Eq) does (as I understand it) is 
> to produce an instance at compilation time by looking at how the 
> specific type is presented. But that same compilation time producing 
> could be done to produce it as a function instead of as an 
> implementation of Eq, so that syntacticEq would not be an actual 
> function, but some sort of "macro" that, on compile time, creates the 
> default implementation of equality, but instead of defining it as (==) 
> it defines it as a new function that is only used there.
>
> Of course, I can just implement syntactic equality myself explicitly, 
> but when I have to do this for 3, 4, 7 types, some of which have many 
> cases, and a lot of these are polymorphic, so that I have to put all 
> the (Eq arg1, Eq arg2, Eq arg3, ...) => constraints before all of 
> them, it gets old quick.
>
> So, is there something like this? Am I saying something really dumb? 
> Of course, I am thinking about equality here, but the same could be 
> said for any standard derivation of classes, like Functor, Show, etc. 
> ALL of them sound like I've wanted to do them at some point in the past.
>
> Thanks,
> Juan.
>