使用具有特定上下文的功能同质化异构列表

Question

我正在摆弄 Haskell 中类型级编程的基础知识，我试图编写一个函数，使用具有(* -> *) -> Constraint类型上下文(例如，length或fmap (/= x))的函数"同质化"异构列表。

异构列表定义如下：

data HList ls where
HNil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)

我已经定义了一个类型族AllKind2：

type family AllKind2 c t li :: Constraint where
AllKind2 _ _ '[] = ()
AllKind2 c t ((t _) : xs)) = (c t, AllKind2 c t xs)

类型族按预期工作(据我有限的知识所知)，如此函数所示，如果提供可以满足AllKind2的异构列表，则仅返回单元：

unitIfAllIsWell :: forall c t li. AllKind2 c t li => Proxy c -> Proxy t -> HList li -> ()
unitIfAllIsWell _ _ _ = ()

>>> unitIfAllIsWell (Proxy :: Proxy Foldable) (Proxy :: Proxy []) ([] ::: "ok" ::: [1,2] ::: HNil)
()
>>> unitIfAllIsWell (Proxy :: Proxy Foldable) (Proxy :: Proxy []) ("is_list" ::: 10 ::: HNil)
<interactive>:414:1: error:
• Could not deduce: AllKind2 Foldable [] '[Integer]
arising from a use of ‘unitIfAllIsWell’

但是，我编写的均质化函数在类型检查中失败：

homogenize
:: forall c t li q. AllKind2 c t li 
=> Proxy c 
-> Proxy t 
-> (forall p q. c t => t p -> q)
-> HList li                      
-> [q]
homogenize _ _ _ HNil = []
homogenize _ _ f (x ::: xs) = f x : homogenize (Proxy :: Proxy c) (Proxy :: Proxy t) f xs

• Could not deduce: a ~ t p0
from the context: AllKind2 c t li
bound by the type signature for:
homogenize :: forall (c :: (* -> *) -> Constraint)
(t :: * -> *) (li :: [*]) q.
AllKind2 c t li =>
Proxy c
-> Proxy t
-> (forall p q1. c t => t p -> q1)
-> HList li
-> [q]
at HList.hs:(134,1)-(140,8)
or from: li ~ (a : as)
bound by a pattern with constructor:
::: :: forall a (as :: [*]). a -> HList as -> HList (a : as),
in an equation for ‘homogenize’
at HList.hs:142:24-31
‘a’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (as :: [*]). a -> HList as -> HList (a : as),
in an equation for ‘homogenize’
at HList.hs:142:24-31

约束AllKind2不足以告诉编译器HList li中的任何元素都将满足约束c t，因此，应用提供的函数f应该在类型级别有效？

我在这里错过了什么吗？我正在尝试的可能吗？

Answer 1

即使例如AllKind2 Foldable [] '[Int]与任何AllKind2方程都不匹配，它不被理解为一个不满足的约束。(一般原则是未定义类型系列应用程序就是：未定义，从某种意义上说，它可能是某种东西，但你不知道它是什么。这就是为什么，即使你知道AllKind2 c t (x : xs),，你也不能通过说"这是从AllKind2获得定义的约束的唯一方法"来推断某些yx ~ t y。 对于一般AllKind2 c t (x : xs)情况，您需要一个公式，该公式调度到将包含实际信息的类。

-- if you know some types satisfy a typeclass, you know they satisfy the superclasses
-- this lets us store and extract the information that x needs to be of form t _
class (c t, x ~ t (UnwrapAllKind2 t x)) => AllKind2Aux c t x where
type UnwrapAllKind2 t x
instance c t => AllKind2Aux c t (t y) where
type UnwrapAllKind2 t (t y) = y
type family AllKind2 c t xs :: Constraint where
AllKind2 c t '[] = ()
AllKind2 c t (x : xs) = (AllKind2Aux c t x, AllKind2 c t xs)

然后，您的homogenize无需修改即可通过。

请注意，homogenize过于复杂。c根本没有做任何事情：homogenize将c t实例作为输入，只是将其转发给正在映射的函数。该函数只能使用自己的c t实例，因为t是固定的。没有什么homogenize可以做的是以下函数无法更清楚地做的(请注意，您的homogenize甚至无法"限制"映射函数仅使用c t而不是t的任何其他属性，因此它可以混淆得多，而不是它可以澄清

)：

class x ~ t (UnApp t x) => IsApp t x where
type UnApp t x
instance IsApp t (t y) where
type UnApp t (t y) = y
type family AllApp t xs :: Constraint where
AllApp t '[] = ()
AllApp t (x : xs) = (IsApp t x, AllApp t xs)
homogenize' :: AllApp t xs => Proxy t -> (forall x. t x -> r) -> HList xs -> [r] -- also, the Proxy t is not strictly necessary
homogenize' t f HNil = []
homogenize' t f (x ::: xs) = f x : homogenize' t f xs -- note that dealing with Proxys is much nicer if you treat them as things that can be named and passed around instead of rebuilding them every time
-- homogenize' (Proxy :: Proxy []) length ([] ::: "ok" ::: [1,2] ::: HNil) = [0, 2, 2]