【问题标题】:Problems With Type Inference on (^)(^) 上的类型推断问题
【发布时间】:2017-10-31 16:08:50
【问题描述】:

所以,我正在尝试编写自己的 Prelude 替代品,并且我已将 (^) 实现为这样:

{-# LANGUAGE RebindableSyntax #-}

class Semigroup s where
    infixl 7 *
    (*) :: s -> s -> s

class (Semigroup m) => Monoid m where
    one :: m

class (Ring a) => Numeric a where
    fromIntegral :: (Integral i) => i -> a
    fromFloating :: (Floating f) => f -> a

class (EuclideanDomain i, Numeric i, Enum i, Ord i) => Integral i where
    toInteger :: i -> Integer
    quot :: i -> i -> i
    quot a b = let (q,r) = (quotRem a b) in q
    rem :: i -> i -> i
    rem a b = let (q,r) = (quotRem a b) in r
    quotRem :: i -> i -> (i, i)
    quotRem a b = let q = quot a b; r = rem a b in (q, r)

-- . . .

infixr 8 ^
(^) :: (Monoid m, Integral i) => m -> i -> m
(^) x i
    | i == 0 = one
    | True   = let (d, m) = (divMod i 2)
                   rec = (x*x) ^ d in
               if m == one then x*rec else rec

(注意这里使用的 Integral 是我定义的,不是 Prelude 中的,虽然类似。另外,one 是一个多态常数,它是幺半群运算下的恒等。)

数值类型是幺半群,所以我可以尝试做,比如 2^3,但是类型检查器给了我:

*AlgebraicPrelude> 2^3

<interactive>:16:1: error:
    * Could not deduce (Integral i0) arising from a use of `^'
      from the context: Numeric m
        bound by the inferred type of it :: Numeric m => m
        at <interactive>:16:1-3
      The type variable `i0' is ambiguous
      These potential instances exist:
        instance Integral Integer -- Defined at Numbers.hs:190:10
        instance Integral Int -- Defined at Numbers.hs:207:10
    * In the expression: 2 ^ 3
      In an equation for `it': it = 2 ^ 3

<interactive>:16:3: error:
    * Could not deduce (Numeric i0) arising from the literal `3'
      from the context: Numeric m
        bound by the inferred type of it :: Numeric m => m
        at <interactive>:16:1-3
      The type variable `i0' is ambiguous
      These potential instances exist:
        instance Numeric Integer -- Defined at Numbers.hs:294:10
        instance Numeric Complex -- Defined at Numbers.hs:110:10
        instance Numeric Rational -- Defined at Numbers.hs:306:10
        ...plus four others
        (use -fprint-potential-instances to see them all)
    * In the second argument of `(^)', namely `3'
      In the expression: 2 ^ 3
      In an equation for `it': it = 2 ^ 3

我知道这是因为 Int 和 Integer 都是 Integral 类型,但是为什么在普通 Prelude 中我可以做到这一点呢? :

Prelude> :t (2^)
(2^) :: (Num a, Integral b) => b -> a
Prelude> :t 3
3 :: Num p => p
Prelude> 2^3
8

即使我的部分应用的签名看起来相同?

*AlgebraicPrelude> :t (2^)
(2^) :: (Numeric m, Integral i) => i -> m
*AlgebraicPrelude> :t 3
3 :: Numeric a => a

我要怎样才能让 2^3 实际上起作用,从而得到 8?

【问题讨论】:

  • 如果我运行你的程序,我只会得到Ambiguous occurrence ‘^’。您不能简单地覆盖 Haskell 中的名称
  • 在我的代码中,我使用了 RebindableSyntax。 Prelude 的 (^) 不在范围内。编辑:另外,我使用的 Monoid 类型类也是我的。
  • 如果有帮助,我正在使用的代码都在这个 GitHub 存储库中:github.com/Crazycolorz5/AlgebraicPrelude/tree/…
  • 我怀疑这是由于 Num 在默认规则中的特殊性,尽管非常感谢 MVCE(因为我可以运行独立的东西来复制问题)。
  • @Alec 我认为你是对的;您知道在 Prelude 代码中指定默认值的位置,以及我如何自己定义它们吗?另外,很抱歉缺少 MVCE,有很多相互关联的代码;我链接的 repo 中的 Groups、Order 和 Numbers 模块应该是重新创建它所必需的。

标签: haskell type-inference exponentiation monoids hindley-milner


【解决方案1】:

Hindley-Milner 类型系统并不喜欢必须默认 任何东西。在这样的系统中,您希望类型是适当固定(刚性,skolem)或适当多态,但“这就像一个整数...... . 但如果您愿意,我也可以将其转换为其他语言”,因为许多其他语言并没有真正奏效。

因此,Haskell 很讨厌违约。它对此没有一流的支持,只有一个非常 hacky 的临时硬编码机制,主要处理内置数字类型,但在涉及更多内容时失败了。

因此,您应该尽量不要依赖默认设置。我的观点是^ 的标准签名是不合理的;更好的签名是

(^) :: Num a => a -> Int -> a

Int 可能会引起争议——当然Integer 在某种意义上会更安全;但是,指数太大而无法放入Int 通常意味着结果无论如何都将完全超出范围,并且无法通过迭代乘法进行计算;所以这种表达的意图很好。它在您只写 x^2 或类似的非常常见的情况下提供了最佳性能,这是您绝对不希望在指数中添加额外签名的情况。

在相当少的情况下,你有一个具体的例子。 Integer 数字并想在指数中使用它,您可以随时输入明确的 fromIntegral。这不是很好,但也没有什么不便。

作为一般规则,我尽量避免任何比结果更具多态性的函数参数。 Haskell 的多态性在“向后”时效果最好,即与动态语言中相反的方式:调用者请求结果应该是什么类型,编译器从中计算出参数应该是什么。这几乎总是有效的,因为一旦结果以某种方式在主程序中使用,整个计算中的类型必须链接到树结构。

OTOH,推断结果的类型通常是有问题的:参数可能是可选的,它们本身可能只链接到结果,或者作为多态常量(如 Haskell 数字文字)给出。因此,如果i 没有出现在^ 的结果中,请避免在参数中出现。


“避免”并不意味着我从不写它们,我只是不这样做,除非有充分的理由。

【讨论】:

  • Numbers mod some prime p 即使对于非常大的指数也可以在比例上,并且经常有用。
  • @DanielWagner 对,但您不会使用 ^ 来处理这类事情,对吗?
  • @DanielWagner 我知道模幂运算,我的意思是您无论如何都不会使用 Haskell 的 ^ 运算符计算它,而是使用围绕模数设计的函数行为。虽然 - 它实际上应该是可行的,比如Data.Modular...
  • 我为什么不用 Haskell 的 ^ 运算符来计算呢?我可以想到两个反对意见: 1. 你需要一个专门的运算符来首先减少指数 mod p。但我认为,一旦它有一个小指数,专业人士可能会调用^——而那个“小”指数可能仍然大于Int。 2. 很难编写一种类型,让您可以在运行时选择素数,而不会在+ 等操作中遇到不匹配问题。我在another answer 中概述了一个类似ST 的技巧来避免这个问题。
猜你喜欢
  • 2023-03-17
  • 2016-04-04
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
相关资源
最近更新 更多