[Haskell-cafe] Explicitly calling syntactic equality on datatypes

[Sylvain Henry]

I have created an issue: https://gitlab.haskell.org/ghc/ghc/issues/17210


On 17/09/2019 18:03, Sylvain Henry wrote:
> 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.
>>
> _______________________________________________
> 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.