37

我正在阅读ClassyPrelude的公告并到达这里：

instance (b ~ c, CanFilterFunc b a) => CanFilter (b -> c) a where
    filter = filterFunc

然后作者提到这行不通：

instance (CanFilterFunc b a) => CanFilter (c -> c) a where
    filter = filterFunc

这对我来说很有意义，因为c与左侧的约束完全无关。

但是，文章中没有提到并且我不明白的是为什么这不起作用：

instance (CanFilterFunc b a) => CanFilter (b -> b) a where
    filter = filterFunc

有人可以解释为什么这与第一个提到的定义不同吗？也许 GHC 类型推断的工作示例会有所帮助？

4

2 回答 2

56

Michael 在他的博客文章中已经给出了很好的解释，但我将尝试用一个（人为的，但相对较小的）示例来说明它。

我们需要以下扩展：

{-# LANGUAGE FlexibleInstances, TypeFamilies #-}

让我们定义一个比 简单的类，CanFilter只有一个参数。我正在定义该类的两个副本，因为我想演示两个实例之间的行为差​​异：

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

现在，让我们为每个类定义一个实例。对于Twice1，我们直接将类型变量固定为相同，对于Twice2，我们允许它们不同，但添加一个等式约束。

instance Twice1 (a -> a) where
  twice1 f = f . f

instance (a ~ b) => Twice2 (a -> b) where
  twice2 f = f . f

为了显示差异，让我们定义另一个重载函数，如下所示：

class Example a where
  transform :: Int -> a

instance Example Int where
  transform n = n + 1

instance Example Char where
  transform _ = 'x'

现在我们已经到了可以看到差异的地步。一旦我们定义

apply1 x = twice1 transform x
apply2 x = twice2 transform x

并向 GHC 询问推断的类型，我们得到了

apply1 :: (Example a, Twice1 (Int -> a)) => Int -> a
apply2 :: Int -> Int

这是为什么？好吧，Twice1仅当函数的源类型和目标类型相同时才会触发实例。对于transform给定的上下文，我们不知道。GHC 只会在右侧匹配时应用实例，所以我们留下了未解析的上下文。如果我们尝试说apply1 0，则会出现类型错误，表示仍然没有足够的信息来解决重载问题。Int在这种情况下，我们必须明确指定要通过的结果类型。

但是，在 中Twice2，实例适用于任何函数类型。GHC 会立即解决它（GHC 永远不会回溯，所以如果一个实例明显匹配，它总是被选中），然后尝试建立先决条件：在这种情况下，相等约束，然后强制结果类型为Int，并允许我们也解决Example约束。我们可以说apply2 0没有进一步的类型注释。

所以这是关于 GHC 的实例解析的一个相当微妙的点，这里的等式约束有助于 GHC 的类型检查器以一种需要用户更少类型注释的方式进行。

于 2012-07-19T06:02:24.147 回答
0

完成@kosmikus 的回答

这同样适用于 purescript - 您需要等式约束才能正确派生类型（您可以在此处尝试http://try.purescript.org）

module Main where

import Prelude

-- copied from https://github.com/purescript/purescript-type-equality/blob/master/src/Type/Equality.purs
class TypeEquals a b | a -> b, b -> a where
  to :: a -> b
  from :: b -> a

instance refl :: TypeEquals a a where
  to a = a
  from a = a

-----------------

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

instance mytwice1 :: Twice1 (a -> a) where
  twice1 f = f >>> f

instance mytwice2 :: TypeEquals a b => Twice2 (a -> b) where
  twice2 f = f >>> from >>> f

class Example a where
  transform :: Int -> a

instance exampleInt :: Example Int where
  transform n = n + 1

instance exampleChar :: Example Char where
  transform _ = 'x'

{--
-- will raise error
--   No type class instance was found for Main.Twice1 (Int -> t1)

apply1 x = twice1 transform x

-- to resolve error add type declaration
apply1 :: Int -> Int

--}

-- compiles without error and manual type declaration, has type Int -> Int automatically
apply2 x = twice2 transform x

但是在 idris 你没有

module Main

import Prelude

interface Twice f where
  twice : f -> f

Twice (a -> a) where
  twice f = f . f

interface Example a where
  transform : Int -> a

Example Int where
  transform n = n + 1

Example Char where
  transform _ = 'x'

-- run in REPL to see that it derives properly:

-- $ idris src/15_EqualityConstraint_Twice_class.idr
-- *src/15_EqualityConstraint_Twice_class> :t twice transform
-- twice transform : Int -> Int

-- Summary:
-- in idris you dont need equality constaint to derive type of such functions properly
于 2018-10-17T20:18:11.440 回答