对类型对的约束

Ryba 发表于 Dev

鱼

我试图定义一个类型类，每个类型对的每个元素都满足一个约束：

{-# 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？

高温超净水

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

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都有一个Fst k :: x和一个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 => ()

本文收集自互联网，转载请注明来源。

如有侵权，请联系 [email protected] 删除。