haskell - 约束封闭型族

Question

我可以让编译器相信封闭类型族中的类型同义词始终满足约束吗？该族由一组有限的提升值索引。

类似的东西

data NoShow = NoShow
data LiftedType = V1 | V2 | V3

type family (Show (Synonym (a :: LiftedType)) => Synonym (a :: LiftedType)) where
  Synonym V1 = Int
  Synonym V2 = NoShow -- no Show instance => compilation error
  Synonym V3 = ()

我可以对开放类型族实现约束:

class (Show (Synonym a)) => SynonymClass (a :: LiftedType) where
  type Synonym a
  type Synonym a = ()

instance SynonymClass Int where
  type Synonym V1 = Int

-- the compiler complains here
instance SynonymClass V2 where
  type Synonym V2 = NoShow

instance SynonymClass V3

但是编译器必须能够推断出存在 SynonymClass a 的实例这一事实。 V1 中的每一个, V2和 V3 ?但无论如何，我宁愿不使用开放式家族。

我要求这样做的动机是我想让编译器相信我的代码中所有封闭类型族的实例都有 Show/Read 实例。一个简化的例子是:

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 (Synonym lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right x  -> "Synonym value: " ++ show x 

[有人在评论中提到这是不可能的——这是因为它在技术上是不可能的(如果是的话，为什么)或者只是 GHC 实现的限制？]

Answer 1

问题是我们不能把 Synonym在实例头中，因为它是一个类型族，我们不能编写像 (forall x. Show (Synonym x)) => ... 这样的“普遍量化”约束因为在 Haskell 中没有这样的东西。

但是，我们可以使用两件事:

forall x. f x -> a相当于(exists x. f x) -> a

singletons的去功能化让我们无论如何都可以将类型族放入实例头中。

因此，我们定义了一个适用于 singletons 的存在包装器。 -style 类型函数:

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

我们还包括 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然后在存在标签上进行模式匹配以检查我们是否获得了正确的类型(如果不正确则失败)。这几乎涵盖了 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 上的模式匹配中只有一个 case。 ，无论我们有多少索引。请注意 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