Eq or Ord instances for existential GADT

Question

Is there a convenient way to get an instance of Ord (or Eq) to compare any two values of a GADT, irrespective of the type parameter.

In the GADT, the type parameter is phantom, just meant to associate each constructor with a type, e.g. the GADT represent keys/queries, and the type parameter is the type of the associated value/result.

To illustrate:

{-# LANGUAGE GADTs, Rank2Types #-}

data Car = Car   -- whatever
data Food = Food

data CarRental  = CarRental  {passengers :: Int, mileage :: Int}
  deriving (Eq, Ord)
data ErrandList = ErrandList {avoidJunkFood :: Bool}
  deriving (Eq, Ord)

data GetStuff a where
  RentACar :: CarRental  -> GetStuff Car
  BuyFood  :: ErrandList -> GetStuff Food

data Some t = forall a. Some (t a)

GetStuff is a GADT, so that each item is associated with a result type, Car or Food. I can use that in e.g Free or FreeApplicative. I may want to retrieve all the GetStuff that appear in the structure. I can easily build [Some GetStuff], but not a Set (Some GetStuff), for lack of an Ord instance.

I see that

data GetSomeStuff = RentSomeCar CarRental | BuySomeFood ErrandList
  deriving (Eq, Ord)

is isomorphic to Some GetStuff (a is phantom in GetStuff), so I can get Eq, Ord, and possibly others by writing this isomorphism:

existentialToUntyped :: Some GetStuff -> GetSomeStuff
untypedToExistential :: GetSomeStuff -> Some GetStuff

untypedToExistential (RentSomeCar x) = Some $ RentACar x
untypedToExistential (BuySomeFood x) = Some $ BuyFood x
existentialToUntyped (Some (RentACar x)) = RentSomeCar x
existentialToUntyped (Some (BuyFood x)) = BuySomeFood x

but it's tedious for protocols much larger than GetStuff. Is there a better way, with or without GADT?

Also, I intend to write code parametric in the "protocol" type (here GetStuff) at this point, where I would like a signature such as

queries :: SomeConstraint protocol => 
  FreeApplicative protocol 
  -> Set (Some protocol)

I may have to do

myFunction :: Ord untyped => 
  Iso (Some protocol, untyped) 
  -> FreeApplicative protocol
  -> Set untyped

Again, is there a better way?

Strictly speaking, GetSomeStuff is only isomorphic to sigma a. GetStuff a (a type which doesn’t exist in Haskell). In particular note that [GetSomeStuff] and [GetStuff a] are not isomorphic. Alternatively, consider that no halting function of type GetSomeStuff -> GetStuff a exists. — Dan Robertson
@DanRobertson I meant between (Some GetStuff) and GetSomeStuff. I added an implementation above, it feels ok to me, but I'm just getting my feet wet here. Do I miss something ? — Didier Dupont

phadej phadej · Accepted Answer · 2019-03-05T08:48:14

Starting with your example

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}

import Data.Type.Equality

data Car
data Food

data CarRental  = CarRental  {passengers :: Int, mileage :: Int}
  deriving (Eq, Ord)
data ErrandList = ErrandList {avoidJunkFood :: Bool}
  deriving (Eq, Ord)

data GetStuff a where
  RentACar :: CarRental  -> GetStuff Car
  BuyFood  :: ErrandList -> GetStuff Food

data Some t = forall a. Some (t a)

You'll need to write an instance of http://hackage.haskell.org/package/dependent-sum-0.4/docs/Data-GADT-Compare.html#t:GEq

class GEq f where
  geq :: f a -> f b -> Maybe (a :~: b)

Then you'll be able to define an instance of Eq (Some f)

instance GEq f => Eq (Some f) where
    Some fa == Some fb = case geq fa fb of
        Just Refl -> True
        Nothing   -> False

Writing an instance by hand is repetitive, but not awful. Note that I wrote in the way without "catch all" last case.

instance GEq GetStuff where
  geq (RentACar x) z = case z of
    RentACar x' -> if x == x' then Just Refl else Nothing
    _           -> Nothing

  geq (BuyFood x) z = case z of
    BuyFood x' -> if x == x' then Just Refl else Nothing
    _          -> Nothing

There's a GCompare class for Ord of GADTs.

So the problem reduces to "how to derive GEq or GCompare automatically". I think that for special GADTs, like your GetStuff, you can write quick-n-dirty TH, to generate the code.

Generic-like alternative I can think of would require you to write conversion functions from and to GetStuff, which might be a win if you need to write more generic functions. Let's explore that too. First we define a generic representation of GADTs we are interested in:

data Sum (cs :: [(*, *)]) a where
  Z :: a :~: c -> b -> Sum ( '(c, b) ': cs) a
  S :: Sum cs a -> Sum (c ': cs) a

We can convert between GetStuff and Sum. That we'll need to write for each GADT, this is O(n) where n is constructors count.

type GetStuffCode =
  '[ '(Car, CarRental)
  ,  '(Food, ErrandList)
  ]

toSum :: GetStuff a -> Sum GetStuffCode a
toSum (RentACar x) = Z Refl x
toSum (BuyFood x)  = S (Z Refl x)

fromSum :: Sum GetStuffCode a -> GetStuff a
fromSum (Z Refl x)     = RentACar x
fromSum (S (Z Refl x)) = BuyFood x
fromSum (S (S x))      = case x of {} -- silly GHC requires this :)

Now, as we have generic representation, Sum, we can write generic functions. Equality, GGEq for Generic Gadt Equality The class looks like GEq, but we use Sum as an arguments.

class GGEq code where
  ggeq :: Sum code a -> Sum code b -> Maybe (a :~: b)

We'll need two instances, for nil and cons codes:

instance GGEq '[] where
  ggeq x _ = case x of {}

instance (Eq b, '(x, b) ~ c, GGEq cs) => GGEq (c ': cs) where
  ggeq (Z Refl x) (Z Refl y) = if x == y then Just Refl else Nothing
  ggeq (S x)      (S y)      = ggeq x y

  ggeq (Z _ _) (S _)   = Nothing
  ggeq (S _)  (Z _ _) = Nothing

Using that machinery, writing geq for GetStuff is trivial:

geq1 :: GetStuff a -> GetStuff b -> Maybe (a :~: b)
geq1 x y = ggeq (toSum x) (toSum y)

Eq or Ord instances for existential GADT

1 Answers