如何将这个封闭类型族与一个依赖类型类结合在一起

Question

我的问题

我有以下类型家族，可将参数从函数中分离出来：

type family
  SeparateArgs
    ( a :: Type )
      :: ( Type, [Type] )
  where
    SeparateArgs (a -> b) =
      SndCons2 a (SeparateArgs b)
    SeparateArgs a =
      '(a, '[])

我也有这个类型类做相反的事情：

class Refunct args goal newSig | args goal -> newSig where
  refunct :: (HList args -> goal) -> newSig
instance Refunct '[] goal goal where
  refunct makeA = makeA HNil
instance
  ( Refunct tailArgs goal c
  )
    => Refunct (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct hFunct x = refunct $ hFunct . (x :>)

现在几乎每次我使用这两个时，我都会像下面这样一起使用它们：

instance
  ( SeparateArgs a ~ '(goal, args)
  , Refunct goal args a
  , ...
  )
    => ...

这样一来，我可以断开参数，进行一些处理以创建该类型的函数，HList args -> goal然后将其转换为常规函数。

这行得通，但是由于我知道，这非常令人沮丧Separate a ~ '(goal, args) => Refunct args goal a，这意味着仅需要这些语句之一。但是编译器无法告诉您，因此我需要通知它。

这当然不是很关键，因为我的代码当前可以运行，但是我想将其合并为一个语句。理想情况下，通过添加第二个功能依赖项来Refunct像这样：

class
  ( SeparateArgs newSig ~ '(goal, args)
  )
    => Refunct args goal newSig
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

（当然这本身是行不通的）

有没有一种方法可以将两者（类型家族SeparateArgs和类型类Refunct）简化为一个约束？我仍然愿意定义其他构造，只要它们在结果中具有非冗余约束即可。我仍然需要该refunct功能。

如果需要，这是我的实现HList：

data HList (a :: [ Type ]) where
  HNil :: HList '[]
  (:>) :: a -> HList b -> HList (a ': b)

hHead :: HList (a ': b) -> a
hHead (a :> _) = a

hTail :: HList (a ': b) -> HList b
hTail (_ :> b) = b

我尝试过的

在其他地方讨论了此问题后，建议我尝试：

type family
  IsAtomic
    ( a :: Type )
      :: Bool
  where
    IsAtomic (a -> b) = 'False
    IsAtomic a = 'True

class
  Refunct args goal newSig
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True
  )
    =>  Refunct '[] goal goal
  where
  refunct makeA = makeA HNil
instance
  ( Refunct tailArgs goal c
  , IsAtomic (headArg -> c) ~ 'False
  )
    => Refunct (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct hFunct x = refunct $ hFunct . (x :>)

在这里，我们添加了一个额外的约束条件，即第一个实例仅在以下情况下才起作用IsAtomic goal ~ 'True，而第二个实例只有IsAtomic goal ~ 'False在IsAtomic我定义的类型族在哪里时才起作用，该族'False在函数以及'True所有其他方面。

在这里，编译器似乎无法确认两个实例没有违反功能依赖性。确切的错误是：

    Functional dependencies conflict between instance declarations:
      instance (IsAtomic goal ~ 'True) => Refunct '[] goal goal
      instance (Refunct tailArgs goal c, IsAtomic goal ~ 'False) =>
               Refunct (headArg : tailArgs) goal (headArg -> c)
    |
XXX |   ( IsAtomic goal ~ 'True
    |   ^^^^^^^^^^^^^^^^^^^^^^^...

（好的，因为我删除了所有识别信息，所以不完全正确）。

我的直觉是，它不知道IsAtomic goal ~ 'True并且IsAtomic goal ~ 'False不能同时都成立。这是合理的，因为如果不进行检查，我们就IsAtomic无法forall a. a确定不满足两个约束条件。

Answer 1

我们想要什么？

为了解决这个问题，我们首先要分解我们想要什么。

我们希望“落入”封闭类型族的行为（以便函数和非函数将匹配不同的实例），但我们也希望像类型类一样构造数据（这样我们就可以得到refunct）。

也就是说，我们想要一个具有紧密类型族逻辑的类型类。因此，为了做到这一点，我们可以将这两部分分开并分别实现；逻辑作为封闭类型族，其余作为类型类。

现在要做到这一点，我们采用我们的类型系列并添加另一个参数

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

变成

class
  Foo'
    (flag :: Flag)
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

该参数将充当一个标志来告诉我们要使用哪个实例。由于它是一种类型，Flag我们需要创建该数据类型。它应该为每个实例都有一个构造函数（在某些情况下我们可能会有点宽松，但一般来说你会想要一对一）

data Flag = Instance1 | Instance2 | Instance3 ...

^{（就我的问题而言，因为我们只使用两个实例Bool）}

现在我们构建一个封闭类型族来计算要匹配的实例。它应该从参数中获取相关参数Foo并产生一个Flag

type family
  FooInstance
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
      :: Flag
  where
    FooInstance ... = Instance1
    FooInstance ... = Instance2
    FooInstance ... = Instance3
    ...

^{就当前问题而言，我们称之为此名称IsAtomic，因为该名称描述了它的作用。}

现在我们修改实例以匹配正确的Flags。这非常简单，我们只需将实例标志添加到声明中即可：

instance
  ( Foo newBar newBaz newBax
  ...
  )
    => Foo' 'Instance3 foo bar baz bax
  where
    ...

重要的是，我们不会将递归调用更改为Foo对 的调用Foo'。我们将构建Foo一个包装器Foo'来管理我们的封闭类型系列（FooInstance在本例中），因此我们希望调用Foo以避免每次调用相同的逻辑。

是这样构建的：

instance
  ( Foo newBar newBaz newBax
  ...
  )
    => Foo' 'Instance3 foo bar baz bax
  where
    ...

如果我们想更加安全，我们可以向每个Foo'实例添加一行来检查它是否被正确调用：

instance
  ( Foo newBar newBaz newBax
  , FooInstance bar baz baz ~ 'Instance3
  ...
  )
    => Foo' 'Instance3 bar baz bax
  where
    ...

我的解决方案

所以现在我们在手头的具体问题上使用这个策略。这是完整的代码。相关类是SeparateArgs：

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
  where
    ...
instance
  ( Foo' (FooInstance bar baz bax) bar baz bax
  )
    => Foo bar baz bax
  where
    ...