haskell - 如何让 GHC 相信递归类型的类型相等性

Question

我正在定义一个类型，其类型参数有一些关系。我有 Item 类型，它采用 Cat 和 SubCat，但您可以使用某些 SubCat 类型，具体取决于猫。例如，当您将 Cat1 指定为 Cat 时，您可以将 SubCat1 或 SubCat2 指定为 SubCat.

我使用 ValidSubCats 类型族实现它，为每个 Cat 和 OneOf 类型定义有效的 SubCat定义约束的系列。

{-# LANGUAGE DataKinds, GADTs, PolyKinds, StandaloneKindSignatures, TypeFamilies, TypeOperators #-}

import Data.Kind (Constraint, Type)
import Data.Type.Equality ((:~:)(..), TestEquality(..))
import Unsafe.Coerce (unsafeCoerce)

data Cat = Cat1 | Cat2
type SCat :: Cat -> Type
data SCat cat where
    SCat1 :: SCat 'Cat1
    SCat2 :: SCat 'Cat2

data SubCat = SubCat1 | SubCat2 | SubCat3
type SSubCat :: SubCat -> Type
data SSubCat subCat where
    SSubCat1 :: SSubCat 'SubCat1
    SSubCat2 :: SSubCat 'SubCat2
    SSubCat3 :: SSubCat 'SubCat3

type ValidSubCats :: Cat -> [SubCat]
type family ValidSubCats cat where
    ValidSubCats 'Cat1 = '[ 'SubCat1, 'SubCat2 ]
    ValidSubCats 'Cat2 = '[ 'SubCat2, 'SubCat3 ]

type OneOf :: k -> [k] -> Constraint
type family OneOf t ts where
    OneOf t (t ': _) = ()
    OneOf t (_ ': ts) = OneOf t ts
    OneOf _ _ = ('True ~ 'False)

type Item :: Cat -> SubCat -> Type
data Item cat subCat where
    Item :: OneOf subCat (ValidSubCats cat) => Item cat subCat

现在，我正在尝试定义一个函数来从 SCat 和 SSubCat 中创建一个 Item。

type HL :: (k -> Type) -> [k] -> Type
data HL f t where
    HCons :: f t -> HL f ts -> HL f (t ': ts)
    HNil :: HL f '[]
infixr 5 `HCons`

validSSubCats :: SCat cat -> HL SSubCat (ValidSubCats cat)
validSSubCats SCat1 = SSubCat1 `HCons` SSubCat2 `HCons` HNil
validSSubCats SCat2 = SSubCat2 `HCons` SSubCat3 `HCons` HNil

instance TestEquality SSubCat where
    testEquality SSubCat1 SSubCat1 = Just Refl
    testEquality SSubCat2 SSubCat2 = Just Refl
    testEquality SSubCat3 SSubCat3 = Just Refl
    testEquality _ _ = Nothing

oneOf :: TestEquality f => f t -> HL f ts -> Maybe (OneOf t ts :~: (() :: Constraint))
oneOf x (HCons y ys) = case testEquality x y of
                           Just Refl -> Just Refl
                           Nothing -> unsafeCoerce $ oneOf x ys
oneOf _ HNil = Nothing

makeItem :: SCat cat -> SSubCat subCat -> Maybe (Item cat subCat)
makeItem sCat sSubCat = case oneOf sSubCat (validSSubCats sCat) of
                            Just Refl -> Just Item
                            Nothing -> Nothing

但如您所见，我正在使用 unsafeCoerce 来定义 oneOf。删除它时出现此错误。

test.hs:54:39: error:
    • Could not deduce: OneOf t ts1 ~ OneOf t (t1 : ts1)
      from the context: ts ~ (t1 : ts1)
        bound by a pattern with constructor:
                   HCons :: forall {k} (f :: k -> *) (t :: k) (ts :: [k]).
                            f t -> HL f ts -> HL f (t : ts),
                 in an equation for ‘oneOf’
        at q.hs:52:10-19
      Expected: Maybe (OneOf t ts :~: (() :: Constraint))
        Actual: Maybe (OneOf t ts1 :~: (() :: Constraint))
      NB: ‘OneOf’ is a non-injective type family
    • In the expression: oneOf x ys
      In a case alternative: Nothing -> oneOf x ys
      In the expression:
        case testEquality x y of
          Just Refl -> Just Refl
          Nothing -> oneOf x ys
    • Relevant bindings include
        ys :: HL f ts1 (bound at q.hs:52:18)
        y :: f t1 (bound at q.hs:52:16)
        x :: f t (bound at q.hs:52:7)
        oneOf :: f t
                 -> HL f ts -> Maybe (OneOf t ts :~: (() :: Constraint))
          (bound at q.hs:52:1)
   |
54 |                            Nothing -> oneOf x ys
   |                                       ^^^^^^^^^^

我怎样才能让 GHC 相信它可以从 OneOf t ts :~: (()::约束) 而不使用 unsafeCoerce？

Answer 1

我建议使用具有值级别表示的东西，因为我们可以更轻松地直接操作这些东西。一般来说，这通常更容易使用。例如:

data OneOf' t ts where
  Here :: forall t ts. OneOf' t (t ': ts)
  There :: forall t t2 ts. OneOf' t ts -> OneOf' t (t2 ': ts)

oneOf' :: TestEquality f => f t -> HL f ts -> Maybe (OneOf' t ts)
oneOf' _ HNil = Nothing
oneOf' x (HCons y ys) =
  case testEquality x y of
    Just Refl -> Just Here
    Nothing -> There <$> oneOf' x ys

这并没有直接回答所问的问题，尽管如果你可以写一个带有类型的函数

convertOneOf :: forall t ts. OneOf' t ts -> (OneOf t ts :~: (() :: Constraint))

然后它会回答确切的问题。现在，我不确定该怎么做(甚至不知道是否可行)。我觉得你需要一个辅助功能

weakenOneOf :: forall t t2 ts. OneOfTrue t ts -> OneOfTrue t (t2 ': ts)

(我使用同义词 OneOfTrue 来使事情更容易阅读:type OneOfTrue t ts = OneOf t ts :~: (()::Constraint)).

如果这可以实现，那么你应该可以开始了，尽管我可能仍然更愿意尽可能使用 OneOf'。

值得注意的是，OneOf' 是依赖类型语言中相对常见的结构:有一个 Agda 示例 here , 一个 Idris 例子 here和 Coq 中类似的东西 here .这些中的每一个都以与 OneOf' 相同的方式具有值(value)级别的内容。

Item 可以重写为使用 OneOf'，如下所示:

type Item' :: Cat -> SubCat -> Type
data Item' cat subCat where
    Item' :: OneOf' subCat (ValidSubCats cat) -> Item' cat subCat

并且对 makeItem 进行了相应的重写以使用 Item'。

为什么原来的 OneOf 很棘手而 OneOf' 没那么棘手

通常很难使用像OneOf 这样的东西。原因之一是 Haskell 允许可以“卡住”的类型族。这可以防止某些类型级别的“减少”，并且我们没有规范形式之类的东西。

例如，考虑这个定义，它可能有助于处理传递给 OneOf 的类型级列表:

listDecideNilCons :: forall ts. Either (ts :~: '[]) (IsCons ts)
listDecideNilCons = ...

data IsCons a where
  MkIsCons :: forall t ts. IsCons (t ': ts)

listDecideNilCons 只会告诉您类型级列表要么是 nil 要么是 cons，这看起来很合理，而且使用起来很方便。事实上，我怀疑能够实现 listDecideNilCons 或类似的东西是必要的，以便能够实现 convertOneOf .我更强烈地怀疑有必要实现另一个方向的转换。

但是卡住类型族的存在，足以说明listDecideNilCons无法实现。考虑:

type family Sticky (b :: Bool) :: [Int] where
  Sticky True = '[]

example :: Either ((Sticky False) :~: '[]) (IsCons (Sticky False))
example = listDecideNilCons

此代码类型检查。 example 的值应该是多少？由于 Sticky False 无法进一步减少，因此 example 没有有意义的值。

请注意，如果我们也有 value 级别的信息，就像我们对 OneOf' 所做的那样，我们不会遇到这个问题，原因有二:Stuck types is not一个问题，因为我们可以控制哪些特定的“形状”(如 '[] 和 ... ': ...)我们被允许接受并且我们可以使用当我们构建新事物的证明时，证明值。

例如，在 OneOf' 的情况下，它确保类型级列表将具有“形状”... ': 。 ..。在函数 oneOf' 中，我们使用来自递归调用 oneOf' x ys 的证明值来构建更大的证明。

在原始的 oneOf 函数中，我们无法利用递归调用的结果将具有“cons 形状”或返回 Nothing(因为原始的 OneOf 没有给我们这个信息)。但是，我们必须知道这一点才能使用递归调用的结果来产生所需的结果，因为原始 OneOf 需要“cons shape” .