类型对的约束

Question

我正在尝试定义一个类型对的每个元素都满足约束的类型类：

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}

data a ::: b = a ::: b

class    (c1 x, c2 y) => CP c1 c2 (k :: x ::: y)
instance (c1 x, c2 y) => CP c1 c2 (k :: x ::: y)

然而，这不是我需要的，因为 CP 是错误的

:kind CP
CP :: (* -> Constraint) -> (* -> Constraint) -> (x ::: y) -> Constraint

怎样才能让c1和c2论据更加普遍样的k -> Constraint？

Answer 1

您正在将约束应用于该对元素的类型。要将其应用于元素，请执行以下操作：

class (k ~ (Fst k '::: Snd k), c1 (Fst k), c2 (Snd k)) => CP c1 c2 (k :: x ::: y) where
    type Fst k :: x
    type Snd k :: y
instance (c1 a, c2 b) => CP c1 c2 ((a :: x) '::: (b :: y)) where
    type Fst (a '::: b) = a
    type Snd (a '::: b) = b

类定义说每个k :: x ::: y都有 aFst k :: x和 a Snd k :: y（元素），为了CP c1 c2 k保持，元素必须满足各自的约束，并且k必须确实是它的元素对。然后实例声明重申了这一点，并且还定义了Fst和Snd。现在

ghci> :k CP
CP :: forall x y.
      (x -> Constraint) -> (y -> Constraint) -> (x ::: y) -> Constraint

例如，这有效：

type MyPair = String '::: Just False -- :: Type ::: Maybe Bool
class m ~ Just (FromJust m) => IsJust (m :: Maybe k) where type FromJust m :: k
instance IsJust (Just x) where type FromJust (Just x) = x

test :: ()
test = () :: CP Show IsJust MyPair => ()