haskell - 如何将这个封闭类型族与依赖类型类结合起来

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，因为该名称描述了它的作用。}

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

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

重要的是，我们不会将对 Foo 的递归调用更改为对 Foo' 的调用。我们即将构建 Foo 作为 Foo' 的包装器，管理我们的封闭类型系列(在本例中为 FooInstance)，因此我们想要调用Foo 以避免每次都调用相同的逻辑。

它是这样构建的:

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

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

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

我的解决方案

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

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

class
  SeparateArgs
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

instance
  ( IsAtomic newSig ~ isAtomic -- For (possible? compilation time) speedup
  , SeparateArgs' isAtomic args goal newSig
  )
    => SeparateArgs args goal newSig
  where
    refunct = refunct' @isAtomic

class
  SeparateArgs'
    (isAtomic :: Bool)
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig isAtomic
  , newSig isAtomic -> args goal
  where
    refunct' :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True -- Only exists to ensure we are not invoking this in an illegal manner
  )
    => SeparateArgs' 'True '[] goal goal
  where
    refunct' makeA = makeA HNil
instance
  ( IsAtomic (headArg -> c) ~ 'False -- Only exists to ensure we are not invoking this in an illegal manner
  , SeparateArgs tailArgs goal c
  )
    => SeparateArgs' 'False (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct' hFunct x = refunct $ hFunct . (x :>)