使用具有特定类型上下文的函数对异构列表进行同质化

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 的异构列表，那么简单的 returns 单元:

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 获得已定义约束的唯一方法”来推断某些 y 的 x ~ t y。对于一般 AllKind2 c t (x : xs) 情况，您需要一个方程式，该方程式将发送到包含实际信息的 class。

-- 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 而不是 [ 的任何其他属性=25=], 所以它能混淆的比它能澄清的要多得多):

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]

使用具有特定类型上下文的函数对异构列表进行同质化

Homogenize a heterogenous list with a funtion that has a particular kind of context

haskell

static-typing

higher-kinded-types

type-level-computation