Haskell 中的类型类和类型推断

Question

我正试图弄清楚类型推断如何与类型类一起工作，到目前为止我还很难完全掌握它。

让我们定义以下简单的HList：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

infixr 6 :::

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

现在我要定义类型类，它允许将任何函数“uncurry”到 HList 类型的单个参数的函数中：

class FnToProduct fn ls out | fn ls -> out where
  fromFunction :: fn -> HList ls -> out

instance (FnToProduct' (IsArity1 fn) fn ls out) => FnToProduct fn ls out where
  fromFunction = fromFunction' @(IsArity1 fn)

class FnToProduct' (arity1 :: Bool) fn ls out | fn ls -> out where
  fromFunction' :: fn -> HList ls -> out

instance FnToProduct' True (input -> output) '[input] output where
  fromFunction' fn (a ::: tail) = fn a

instance (FnToProduct fnOutput tail out') => FnToProduct' False (input -> fnOutput) (input ': tail) out' where
  fromFunction' fn (input ::: tail) = fromFunction (fn input) tail

type family IsArity1 fn where
  IsArity1 (a -> b -> c) = False
  IsArity1 (a -> b) = True

现在我要中断编译：

test = fromFunction (\a b -> a) (True ::: False ::: HNil)

• Ambiguous type variables ‘p0’, ‘p1’,
                               ‘out0’ arising from a use of ‘fromFunction’
      prevents the constraint ‘(FnToProduct'
                                  'False (p1 -> p0 -> p1) '[Bool, Bool] out0)’ from being solved.
        (maybe you haven't applied a function to enough arguments?)
      Relevant bindings include test :: out0 (bound at src/HList.hs:98:1)
      Probable fix: use a type annotation to specify what ‘p0’, ‘p1’,
                                                          ‘out0’ should be.
      These potential instance exist:
        one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression:
        fromFunction (\ a b -> a) (True ::: False ::: HNil)
      In an equation for ‘test’:
          test = fromFunction (\ a b -> a) (True ::: False ::: HNil)
   |
98 | test = fromFunction (\a b -> a) (True ::: False ::: HNil)
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

但如果我明确指定函数类型：

test = fromFunction (\(a :: Bool (b :: Bool) -> a) (True ::: False ::: HNil)

效果很好。我如何在此处强制执行类型推断，以便编译器获取 HList 的类型以找出函数中的类型？到目前为止，我还尝试使用 infixl/r 运算符，但没有任何运气。

Answer 1

类型类是“匹配的”。在您的示例中，GHC 表示它正在尝试解决约束

FnToProduct' 'False (p1 -> p0 -> p1) '[Bool, Bool] out0

其中统一变量p1 和p0 来自第一个参数的隐式扩展：

(\(a :: _p1) (b :: _p0) -> a)

和统一变量out0 来自fromFunction 的类型。本质上，GHC 不知道参数类型应该是什么，也不知道 fromFunction 调用最终应该返回什么，因此它创建了三个变量来表示它们并试图找出它们应该是什么。

没有instance 匹配此约束。

instance _ => FnToProduct' False (input -> fnOutput) (input ': tail) out'

要求p1 和Bool 相同，但它们不是。正如您在类型注释示例中所展示的那样，它们可能存在，但 GHC 认为它们并非必须存在。你可以想象添加

instance _ => FnToProduct' False (Int -> fnOutput) (Bool ': tail) out'

现在你不知道是a :: Int 还是a :: Bool，因为这两个实例都“适合”。但是，在开放世界假设下，您必须假设可以随时添加这样的新实例。

一种解决方法是使用~ 约束：

instance (i ~ i', o ~ o') => FnToProduct' True (i -> o) '[i'] o'
instance (i ~ i', FnToProduct r t o) => FnToProduct' False (i -> r) (i' ': t) o

第二个实例现在匹配，因为两个 i 变量不同。它现在实际上引导类型推断，因为在这种情况下，i ~ i' 要求转换为用于实例化p1 的p1 ~ Bool 要求。对于p0，第一个实例也是如此。

或者，添加另一个函数依赖。这并不总是有效，但它似乎在这里完成了工作

class FnToProduct fn ls out | fn ls -> out, fn out -> ls
class FnToProduct' (arity1 :: Bool) fn ls out | fn ls -> out, fn out -> ls

这告诉 GHC fs（以及它的参数类型，这里是 p1 和 p0）可以从 ls（这里是 [Bool, Bool]）中计算出来。

除此之外，我认为您的功能可以简化为：

class AppHList ts o f | ts f -> o, ts o -> f where
   appHList :: f -> HList ts -> o
instance AppHList '[] o o where
   appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t -> f) where
   appHList f (x ::: xs) = appHList (f x) xs

人为地要求HList 提供所有参数并不是特别有用，而且它在多态上下文中确实会爆炸，因为您通常无法分辨“提供所有参数”应该是什么意思。例如。 const 可以有任意数量的参数，从 2 开始。所以，appHList const (id ::: 'a' ::: HNil) 6 可以工作（const 有 3 个参数），但fromFunction 在这种情况下会失败。

如果你真的想要的话，你仍然可以将“返回非函数”属性从外部强加给更有用的函数。

type family IsFun f :: Bool where
  IsFun (_ -> _) = True
  IsFun _ = False
fullAppHList :: (IsFun o ~ False, AppHList ts o f) => f -> HList ts -> o
fullAppHList = appHList

Answer 2

这是一个选项：

class (f ~ AbstractList ts o) => AppHList ts o f where
  appHList :: f -> HList ts -> o

type family AbstractList xs o where
  AbstractList '[] o = o
  AbstractList (x ': xs) o =
    x -> AbstractList xs o

instance f ~ o => AppHList '[] o f where
  appHList x HNil = x

instance (AppHList ts o f', f ~ (t -> f'))  => AppHList (t ': ts) o f where
  appHList f (x ::: xs) = appHList (f x) xs

虽然只有一个等式约束，但这表示了多个方向的依赖关系。怎么样？关键是一旦知道列表的结构，类型族就可以减少；第二个参数不需要任何内容​​，也不需要任何列表元素。

这似乎与HTNW的简化版具有相同的推理能力，但它有两个优点：

1. 如果需要，可以获得平等证据。
2. 与PartialTypeSignatures 扩展配合使用效果更好。出于某种原因，GHC 似乎在这种情况下绊倒了 fundep 版本。请参阅 this ticket 我刚刚提交。

---

但是等等！还有更多！这个公式表明，即使有一个类也是可选的！当一切都专门化并完全内联时，基于类的方法可能是最有效的，但这个版本看起来要简单得多：

appHList' :: f ~ AbstractList ts o => f -> HList ts -> o
appHList' x HNil = x
appHList' f (x ::: xs) = appHList' (f x) xs