3

我一直在尝试实现似乎相当简单的类型。下面是一个演示该问题的人为示例。在它的核心，我想实现某种ComplexThing类型，它是一个由更简单的类型参数化的 GADT MyEnum，. 但是，有许多构造函数ComplexThing仅在应用于 的某些（可能很多）成员时才有效MyEnum。

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

我更喜欢这种类型的用户应该能够编写类似NotSimple ThingBor的东西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）产生的最终类型与通用的、普遍量化的规范统一起来该构造函数的参数。但是，我不确定解决此限制的最佳方法是什么。

任何关于我如何解决这个问题的建议都值得赞赏！如果我证明了任何概念或术语上的误解，也欢迎对此发表评论。

4

1 回答 1

2

我替换了你的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!
于 2019-09-01T20:02:08.503 回答