存在性 GADT 的 Eq 或 Ord 实例

Question

有没有方便的方法来获取 Ord（或 Eq）的实例来比较 GADT 的任意两个值，而不考虑类型参数。

在 GADT 中，类型参数是虚幻的，只是为了将每个构造函数与一个类型相关联，例如GADT代表keys/queries，类型参数是关联value/result的类型。

举例说明：

{-# 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 是一个 GADT，因此每个项目都与结果类型相关联，Car 或 Food。我可以在 Free 或 FreeApplicative 中使用它。我可能想要检索结构中出现的所有 GetStuff。由于缺少 Ord 实例，我可以轻松构建 [Some GetStuff]，但不能构建 Set (Some GetStuff)。

我看到了

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

与 Some GetStuff 同构（a 在 GetStuff 中是虚构的），因此我可以通过编写此同构来获得 Eq、Ord 和其他可能的值：

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

但是对于比 GetStuff 大得多的协议来说，它是乏味的。有没有更好的方法，有或没有 GADT？

此外，我打算此时在 "protocol" 类型（这里是 GetStuff）中编写参数化代码，我想要一个签名，例如

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

我可能不得不做

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

同样，有没有更好的方法？

Answer 1

从你的例子开始

{-# 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)

您需要编写一个实例 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)

然后您将能够定义 Eq (Some f)

的实例

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

手动编写实例是重复的，但并不可怕。注意我写的方式没有"catch all" 最后一个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

有 GCompare class Ord 个 GADT。

所以问题简化为"how to derive GEq or GCompare automatically"。我认为对于特殊的 GADT，比如你的 GetStuff，你可以编写 quick-n-dirty TH，以生成代码。

Generic-我能想到的替代方案需要你编写从 GetStuff 到 GetStuff 的转换函数如果您需要编写更多通用函数，这可能是一个胜利。让我们也探讨一下。首先我们定义一个通用表示我们感兴趣的 GADT：

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

我们可以在GetStuff和Sum之间转换。我们需要为每个 GADT 编写，这是 O(n) 其中 n 是构造函数计数。

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 :)

现在，因为我们有泛型表示，Sum，我们可以写泛型职能。平等，GGEq 通用 Gadt 平等 class 看起来像 GEq，但我们使用 Sum 作为参数。

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

我们需要两个实例，nil 和 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

使用那个机器，为 GetStuff 写 geq 是微不足道的：

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

存在性 GADT 的 Eq 或 Ord 实例

Eq or Ord instances for existential GADT

haskell

gadt

existential-type