Ограниченное семейство закрытого типа

Могу ли я убедить компилятор, что ограничение всегда выполняется синонимами типа в закрытом типе? Семейство индексируется конечным набором продвинутых значений.

Я могу принудительно применять ограничение для типов открытых типов:

но компилятор тогда должен был бы рассуждать о том, что существует экземпляр SynonymClass a для каждого из V1, V2 и V3? Но в любом случае я бы предпочел не использовать семейство открытого типа.

Моей мотивацией для этого является то, что я хочу убедить компилятор, что все экземпляры семейства закрытого типа в моем коде имеют экземпляры Show/Read. Упрощенный пример:

[Кто-то упомянул в комментариях, что это невозможно - это потому, что это технически невозможно (и если да, почему) или просто ограничение реализации GHC?]

Ответы

Ответ 1

Проблема заключается в том, что мы не можем помещать Synonym в голову экземпляра, потому что это семейство типов, и мы не можем написать "универсально квантифицированное" ограничение, например (forall x. Show (Synonym x)) => ..., потому что в Haskell нет такой вещи.

Однако мы можем использовать две вещи:

forall x. f x -> a эквивалентен (exists x. f x) -> a
singletons defunctionalization позволяет нам поместить семейства типов в головы экземпляров в любом случае.

Итак, мы определяем экзистенциальную оболочку, которая работает с singletons -типными типами функций:

data Some :: (TyFun k * -> *) -> * where
  Some :: Sing x -> f @@ x -> Some f

И мы также включаем символ defunctionalization для LiftedType:

import Data.Singletons.TH
import Text.Read
import Control.Applicative

$(singletons [d| data LiftedType = V1 | V2 | V3 deriving (Eq, Show) |])

type family Synonym t where
  Synonym V1 = Int
  Synonym V2 = ()
  Synonym V3 = Char

data SynonymS :: TyFun LiftedType * -> * -- the symbol for Synonym
type instance Apply SynonymS t = Synonym t

Теперь мы можем использовать Some SynonymS -> a вместо forall x. Synonym x -> a, и эта форма также может использоваться в случаях.

instance Show (Some SynonymS) where
  show (Some SV1 x) = show x
  show (Some SV2 x) = show x
  show (Some SV3 x) = show x

instance Read (Some SynonymS) where
  readPrec = undefined -- I don't bother with this now...

parseLTandSynonym :: LiftedType -> String -> String
parseLTandSynonym lt x =
  case (toSing lt) of
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv =
      case (readEither flv :: Either String (Some SynonymS)) of
        Left err -> "Can't parse synonym: " ++ err
        Right x  -> "Synonym value: " ++ show x

Это не предоставляет нам Read (Synonym t) для любого конкретного выбора t, хотя мы все еще можем читать Some SynonymS, а затем сопоставление шаблонов на экзистенциальном теге, чтобы проверить, получили ли мы правильный тип (и не получим if это не так). Это в значительной степени охватывает все варианты использования read.

Если это не достаточно хорошо, мы можем использовать другую оболочку и поднять экземпляры Some f на "универсально квантифицированные" экземпляры.

data At :: (TyFun k * -> *) -> k -> * where
  At :: Sing x -> f @@ x -> At f x

At f x эквивалентен f @@ x, но мы можем записать для него экземпляры. В частности, мы можем написать здесь разумный универсальный экземпляр read.

instance (Read (Some f), SDecide (KindOf x), SingKind (KindOf x), SingI x) =>
  Read (At f x) where
    readPrec = do
      Some tag x <- readPrec :: ReadPrec (Some f)
      case tag %~ (sing :: Sing x) of
        Proved Refl -> pure (At tag x)
        Disproved _ -> empty

Сначала мы проанализируем Some f, а затем проверяем, равен ли индекс анализируемого типа индексу, который мы хотели бы проанализировать. Это абстракция шаблона, о котором я упоминал выше, для разбора типов с конкретными индексами. Это более удобно, потому что у нас есть только один случай в совпадении шаблонов на At, независимо от того, сколько у нас индексов. Обратите внимание, что ограничение SDecide. Он предоставляет метод %~, а singletons выводит его для нас, если мы включаем deriving Eq в одноточечные определения данных. Положив это на использование:

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv = withSingI slt $ 
      case (readEither flv :: Either String (At SynonymS lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right (At tag x)  -> "Synonym value: " ++ show (Some tag x :: Some SynonymS)

Мы также можем сделать преобразование между At и Some немного проще:

curry' :: (forall x. At f x -> a) -> Some f -> a
curry' f (Some tag x) = f (At tag x)

uncurry' :: (Some f -> a) -> At f x -> a
uncurry' f (At tag x) = f (Some tag x)

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv = withSingI slt $ 
      case (readEither flv :: Either String (At SynonymS lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right atx  -> "Synonym value: " ++ uncurry' show atx

Ответ 2

Если я правильно понимаю, что вы хотите сделать, это невозможно. Если бы это было так, вы могли бы легко построить непостоянную функцию типа Proxy t -> Bool по строкам

data YesNo = Yes | No
class Foo (yn :: YesNo) where foo :: Proxy yn -> Bool
type family (Foo (T t) => T t) where
    T X = Yes
    T y = No

f :: forall t. Proxy t -> Bool
f _ = foo (Proxy (T t))

Но вы не можете построить такую функцию, даже если все задействованные типы закрыты (что, конечно же, является функцией или ограничением GHC, в зависимости от вашей точки зрения).