我有以下类型家族，可将参数从函数中分离出来：
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。
我的问题，我有以下类型家族，可将参数从函数中分离出来：类型家族SeparateArgs（a :: Type）::（Type，[Type]）其中SeparateArgs（a-> b）= ...