Экземпляры Eq или Ord для экзистенциального GADT - PullRequest
Новая
       46

Экземпляры Eq или Ord для экзистенциального GADT

0 голосов
/ 05 марта 2019

Есть ли удобный способ получить экземпляр Ord (или Eq) для сравнения любых двух значений GADT, независимо от параметра типа.

В GADT параметром типа является фантом, просто предназначенный для связи каждого конструктора с типом, например, GADT представляет ключи / запросы, а параметр типа является типом связанного значения / результата.

Для иллюстрации: 

{-# 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, которые появляются в структуре.Я могу легко собрать [Some GetStuff], но не Set (Some GetStuff), из-за отсутствия экземпляра Ord.

Я вижу, что 

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

Опять же, есть ли лучший способ?

1 Ответ

0 голосов
/ 05 марта 2019

Начиная с вашего примера 

{-# 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" в последнем случае. 

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

Для Ord GADT существует класс GCompare.

Таким образом, проблема сводится к тому, "как"получить GEq или GCompare автоматически ".Я думаю, что для специальных GADT, таких как ваш GetStuff, вы можете написать быструю и грязную TH, чтобы сгенерировать код.

Generic -подобная альтернатива, о которой я могу подумать, потребует от вас написания преобразованияфункции от и до 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 мы можем написать универсальные функции.Equality, GGEq для Generic Gadt Equality Класс выглядит как GEq, но мы используем Sum в качестве аргументов. 

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

Нам понадобятся два экземпляра, дляноль и минусы коды : 

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

Используя этот механизм, написание geq для GetStuff тривиально: 

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