如何让 GHC 相信递归类型的类型相等性
How to convince GHC about type equality on a recursive type
我正在定义一个类型，其类型参数有一些关系。我有 Item 类型，它采用 Cat 和 SubCat，但您可以根据 Cat 使用某些类型的 SubCat。例如，当您将 Cat1 指定为 Cat 时，您可以将 SubCat1 或 SubCat2 指定为 SubCat.
我使用 ValidSubCats 类型系列实现它，为每个 Cat 定义有效的 SubCat，并使用 OneOf 类型系列定义约束。
{-# 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 相信它可以在不使用 unsafeCoerce 的情况下从 OneOf t ts :~: (() :: Constraint) 推断出 OneOf t (t ': ts) :~: (() :: Constraint)？
我建议使用具有 value-level 表示的东西，因为我们可以更轻松地直接操作这些东西。一般来说，这通常更容易使用。例如：
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, an Idris example here and a similar thing in Coq here。每一个都有 value-level 的内容，与 OneOf' 的内容相同。
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 允许可能“卡住”的类型族。这可以防止一些type-level“减少”，我们没有规范形式之类的东西。
例如，考虑这个定义，它可能有助于处理像 type-level 传递给 OneOf 的列表：
listDecideNilCons :: forall ts. Either (ts :~: '[]) (IsCons ts)
listDecideNilCons = ...
data IsCons a where
MkIsCons :: forall t ts. IsCons (t ': ts)
listDecideNilCons 只会告诉你 type-level 列表要么是 nil 要么是 cons，这看起来很合理，而且使用起来很方便。事实上，我怀疑 必须 才能实现 listDecideNilCons 或类似的东西才能实现 convertOneOf。我更强烈地怀疑有必要实现转换的另一个方向。
但是卡住类型族的存在足以说明listDecideNilCons无法实现。考虑：
type family Sticky (b :: Bool) :: [Int] where
Sticky True = '[]
example :: Either ((Sticky False) :~: '[]) (IsCons (Sticky False))
example = listDecideNilCons
此代码type-checks。 example 的值应该是多少？由于无法进一步减少 Sticky False，因此 example 没有有意义的值。
请注意，如果我们也有 value 级别的信息，就像我们对 OneOf' 所做的那样，我们不会 运行 进入这个问题，原因有二: 固定类型不是问题，因为我们可以控制我们可以接受哪些特定的“形状”（如 '[] 和 ... ': ...），并且我们可以在构建新事物的证明时使用证明值.
例如，在 OneOf' 的情况下，它 确保 type-level 列表将具有“形状” ... ': ...。在函数 oneOf' 中，我们使用递归调用 oneOf' x ys 的证明值来构建更大的证明。
在原始的 oneOf 函数中，我们无法利用递归调用的结果将具有“cons 形状”或返回 Nothing 这一事实（因为original OneOf 没有给我们这个信息）。但是，我们 必须 知道这一点才能使用递归调用的结果来产生所需的结果，因为原始 OneOf 需要 一个“缺点形状"。
我正在定义一个类型，其类型参数有一些关系。我有 Item 类型，它采用 Cat 和 SubCat，但您可以根据 Cat 使用某些类型的 SubCat。例如，当您将 Cat1 指定为 Cat 时，您可以将 SubCat1 或 SubCat2 指定为 SubCat.
我使用 ValidSubCats 类型系列实现它，为每个 Cat 定义有效的 SubCat，并使用 OneOf 类型系列定义约束。
{-# 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 相信它可以在不使用 unsafeCoerce 的情况下从 OneOf t ts :~: (() :: Constraint) 推断出 OneOf t (t ': ts) :~: (() :: Constraint)？
我建议使用具有 value-level 表示的东西，因为我们可以更轻松地直接操作这些东西。一般来说，这通常更容易使用。例如：
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, an Idris example here and a similar thing in Coq here。每一个都有 value-level 的内容，与 OneOf' 的内容相同。
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 允许可能“卡住”的类型族。这可以防止一些type-level“减少”，我们没有规范形式之类的东西。
例如，考虑这个定义，它可能有助于处理像 type-level 传递给 OneOf 的列表：
listDecideNilCons :: forall ts. Either (ts :~: '[]) (IsCons ts)
listDecideNilCons = ...
data IsCons a where
MkIsCons :: forall t ts. IsCons (t ': ts)
listDecideNilCons 只会告诉你 type-level 列表要么是 nil 要么是 cons，这看起来很合理，而且使用起来很方便。事实上，我怀疑 必须 才能实现 listDecideNilCons 或类似的东西才能实现 convertOneOf。我更强烈地怀疑有必要实现转换的另一个方向。
但是卡住类型族的存在足以说明listDecideNilCons无法实现。考虑：
type family Sticky (b :: Bool) :: [Int] where
Sticky True = '[]
example :: Either ((Sticky False) :~: '[]) (IsCons (Sticky False))
example = listDecideNilCons
此代码type-checks。 example 的值应该是多少？由于无法进一步减少 Sticky False，因此 example 没有有意义的值。
请注意，如果我们也有 value 级别的信息，就像我们对 OneOf' 所做的那样，我们不会 运行 进入这个问题，原因有二: 固定类型不是问题，因为我们可以控制我们可以接受哪些特定的“形状”（如 '[] 和 ... ': ...），并且我们可以在构建新事物的证明时使用证明值.
例如，在 OneOf' 的情况下，它 确保 type-level 列表将具有“形状” ... ': ...。在函数 oneOf' 中，我们使用递归调用 oneOf' x ys 的证明值来构建更大的证明。
在原始的 oneOf 函数中，我们无法利用递归调用的结果将具有“cons 形状”或返回 Nothing 这一事实（因为original OneOf 没有给我们这个信息）。但是，我们 必须 知道这一点才能使用递归调用的结果来产生所需的结果，因为原始 OneOf 需要 一个“缺点形状"。