haskell - 在 GADT 数据构造函数中通过类型族指定依赖类型

Question

我一直在尝试实现一种看起来相当简单的类型。下面是一个演示问题的人为示例。它的核心是，我想实现一些 ComplexThing 类型，这是一个由更简单的类型 MyEnum 参数化的 GADT。不过，ComplexThing 有许多构造函数，它们仅在应用于 MyEnum 的某些(可能很多)成员时才有效。

解决此问题的一种方法是将这些构造函数分解为更简单的变体。下面我有一个这样的构造函数，NotSimple，它可以重铸为 NotSimple_B 或 NotSimple_C。总的来说，这似乎是一个不太优雅的解决方案。

我更喜欢这种类型的用户应该能够编写类似 NotSimple ThingB 或 NotSimple ThingC 的东西，而 NotSimple ThingA 不应进行类型检查。出于定义 ComplexThing 的目的，我还希望 MyEnum 的允许子集的规范相当通用(即重复规范中的元素应该没问题，顺序应该无关紧要，并且在允许的元素数量方面应该是灵活的)。出于这个原因，在单例类型 SMyEnum 的帮助下，我一直致力于使用类型级列表和遍历该列表的类型系列。

我已经非常接近我想要的了。我实际上可以使用我设置的内容，但不存在完整的可用性。特别是，编写 NotSimple SThingB 本身对于类型检查器来说太多了。有了适当的类型签名，它就变得可行了，但我认为这给潜在用户带来的负担太大了。

在下面查看我的实现，以及一些测试和结果。

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

import Data.Kind (Type)

data MyEnum = ThingA
            | ThingB
            | ThingC
            | ThingD

data family SMyEnum (e :: MyEnum)
data instance SMyEnum ThingA = SThingA
data instance SMyEnum ThingB = SThingB
data instance SMyEnum ThingC = SThingC
data instance SMyEnum ThingD = SThingD

type family MyEnumChoice (l :: [MyEnum]) (e :: MyEnum) :: Type where
  MyEnumChoice (e ': ls) e = SMyEnum e
  MyEnumChoice (f ': ls) e = MyEnumChoice ls e

data ComplexThing :: [(MyEnum,MyEnum)] -> Type where
  Simple :: ComplexThing [ '(ThingA, ThingA), '(ThingA, ThingB), '(ThingC, ThingB) ]
  NotSimple :: forall x. MyEnumChoice '[ ThingB, ThingC ] x -> ComplexThing '[ '(ThingA, x), '(x, ThingD) ]

test3 :: ComplexThing '[ '(ThingA, ThingB), '(ThingB, ThingD) ]
test3 = NotSimple SThingB
-- Checks!

test3_2 :: ComplexThing '[ '(_, ThingB), _]
test3_2 = NotSimple SThingB
-- Checks!

test4 = NotSimple SThingB
-- • Couldn't match expected type ‘MyEnumChoice
--                                   '[ 'ThingB, 'ThingC] x0’
--               with actual type ‘SMyEnum 'ThingB’
--   The type variable ‘x0’ is ambiguous
-- • In the first argument of ‘NotSimple’, namely ‘SThingB’
--   In the expression: NotSimple SThingB
--   In an equation for ‘test4’: test4 = NotSimple SThingB
-- • Relevant bindings include
--     test4 :: ComplexThing '[ '( 'ThingA, x0), '(x0, 'ThingD)]

我想我理解这种类型检查失败背后的原因。我希望 x0 可以神奇地与 NotSimple 的参数统一，但类型检查器看到的是它必须统一最终类型类型族(参数，SThingB)与该构造函数参数的一般的、普遍量化的规范。但是，我不确定解决此限制的最佳方法是什么。

如有任何关于我如何处理此问题的建议，我们将不胜感激!如果我证明了任何概念或术语上的误解，也欢迎对此发表评论。

Answer 1

我替换了你的类型

type family MyEnumChoice (l :: [MyEnum]) (e :: MyEnum) :: Type

带有约束

type family MyEnumCheck (l :: [MyEnum]) (e :: MyEnum) :: Constraint where

检查成员资格，并相应地调整您的 GADT。我不知道这对您来说是否足够通用，但这可能是一个起点。

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

import Data.Kind (Type, Constraint)

data MyEnum = ThingA
            | ThingB
            | ThingC
            | ThingD

data family SMyEnum (e :: MyEnum)
data instance SMyEnum ThingA = SThingA
data instance SMyEnum ThingB = SThingB
data instance SMyEnum ThingC = SThingC
data instance SMyEnum ThingD = SThingD

type family MyEnumCheck (l :: [MyEnum]) (e :: MyEnum) :: Constraint where
  MyEnumCheck (e ': ls) e = ()
  MyEnumCheck (f ': ls) e = MyEnumCheck ls e

data ComplexThing :: [(MyEnum,MyEnum)] -> Type where
  Simple :: ComplexThing [ '(ThingA, ThingA), '(ThingA, ThingB), '(ThingC, ThingB) ]
  NotSimple :: forall x. MyEnumCheck '[ ThingB, ThingC ] x => 
     SMyEnum x -> ComplexThing '[ '(ThingA, x), '(x, ThingD) ]

test3 :: ComplexThing '[ '(ThingA, ThingB), '(ThingB, ThingD) ]
test3 = NotSimple SThingB
-- Checks!

test3_2 :: ComplexThing '[ '(_, ThingB), _]
test3_2 = NotSimple SThingB
-- Checks!

test4 = NotSimple SThingB
-- Checks!