Haskell - соответствие шаблона GADT с ограничениями класса - PullRequest
Новая
       7

Haskell - соответствие шаблона GADT с ограничениями класса

0 голосов
/ 29 сентября 2018

Рассмотрим следующий пример 

{-# LANGUAGE DataKinds, GADTs #-}
data Phantom = A | B
data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B
class PhantomConstraint (a :: Phantom)
instance PhantomConstraint 'A -- Note: No instance for 'B
someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()

Если я сделаю что-то подобное, GHC пожалуется, что совпадение с образцом не является исчерпывающим для someFunc, однако, если я попытаюсь включить случай для FooB (который яне хочет делать это по конкретным доменным причинам) он жалуется, что не может вывести экземпляр PhantomConstraint для Foo 'B

Есть ли какой-нибудь способ заставить сопоставление с шаблоном GADT учитывать ограничения класса типов, такие, чтоэто устраняет необходимые руки сопоставления с образцом?

РЕДАКТИРОВАТЬ: Более подробно о том, что я хочу сделать.У меня есть набор типов, которые все связаны, но имеют разные свойства.В мире ОО это то, для чего люди используют подтипы и наследование.Однако в сообществе FP, похоже, все согласны с тем, что нет действительно хорошего способа сделать подтип, поэтому в этом случае мне нужно взломать его.Таким образом, у меня есть GADT, который объединяет все типы, но с различными параметрами для этого типа.Затем я перехожу к написанию различных классов типов и экземпляров классов типов для параметров типа (включается datakinds, нет представления термина).Я хочу иметь возможность выразить, что некоторые из этих типов из типов данных имеют свойство, которого нет у других, но все они имеют определенные общие свойства, поэтому я не хочу разбивать тип.Единственный другой вариант, который я могу предвидеть, - это создать таксономию для части типа, но затем типы DataKinds будут испорчены.

1 Ответ

0 голосов
/ 29 сентября 2018

Я не могу воспроизвести проблему.Это загружает без предупреждений или ошибок в GHCi 8.4.3. 

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}
module GADTwarning2 where

data Phantom = A | B

data Foo (a :: Phantom) where
  FooA :: Foo 'A
  FooB :: Foo 'B

class PhantomConstraint (a :: Phantom)

instance PhantomConstraint 'A -- Note: No instance for 'B

someFunc :: PhantomConstraint a => Foo a -> ()
someFunc FooA = ()
someFunc FooB = ()

Как пояснил luqui в комментарии, мы не можем избежать случая FooB, так как классы типов открыты, и другой экземпляр может бытьпозже добавленный другим модулем, что делает сопоставление с шаблоном не исчерпывающим.

Если вы абсолютно уверены, что вам не нужны никакие другие экземпляры, кроме одного для A, вы можете попробовать использовать 

class a ~ 'A => PhantomConstraint (a :: Phantom)

Или, если индекс a может быть 'A или 'B, но не может быть третьим конструктором 'C, тогда мы можем попытаться подтвердить этот факт: 

class PhantomConstraint (a :: Phantom) where
   aIsAOrB :: Either (a :~: 'A) (a :~: 'B)

а затем использовать этот член позже.

...