haskell - 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)

和来自 fromFunction 类型的统一变量 out0。本质上，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 ~ Bool 要求，即用于实例化p1。对于 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