在 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

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

Constraint

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!