Search code examples
haskelltype-inferenceexponentiationmonoidshindley-milner

Problems With Type Inference on (^)


So, I'm trying to write my own replacement for Prelude, and I have (^) implemented as such:

{-# 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

(Note that the Integral used here is one I defined, not the one in Prelude, although it is similar. Also, one is a polymorphic constant that's the identity under the monoidal operation.)

Numeric types are monoids, so I can try to do, say 2^3, but then the typechecker gives me:

*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

I get that this arises because Int and Integer are both Integral types, but then why is it that in normal Prelude I can do this just fine? :

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

Even though the signatures for partial application in mine look identical?

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

How would I make it so that 2^3 would in fact work, and thus give 8?


Solution

  • A Hindley-Milner type system doesn't really like having to default anything. In such a system, you want types to be either properly fixed (rigid, skolem) or properly polymorphic, but the concept of “this is, like, an integer... but if you prefer, I can also cast it to something else” as many other languages have doesn't really work out.

    Consequently, Haskell sucks at defaulting. It doesn't have first-class support for that, only a pretty hacky ad-hoc, hard-coded mechanism which mainly deals with built-in number types, but fails at anything more involved.

    You therefore should try to not rely on defaulting. My opinion is that the standard signature for ^ is unreasonable; a better signature would be

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

    The Int is probably controversial – of course Integer would be safer in a sense; however, an exponent too big to fit in Int generally means the results will be totally off the scale anyway and couldn't feasibly be calculated by iterated multiplication; so this kind of expresses the intend pretty well. And it gives best performance for the extremely common situation where you just write x^2 or similar, which is something where you very definitely don't want to have to put an extra signature in the exponent.

    In the rather fewer cases where you have a concrete e.g. Integer number and want to use it in the exponent, you can always shove in an explicit fromIntegral. That's not nice, but rather less of an inconvenience.

    As a general rule, I try to avoid any function-arguments that are more polymorphic than the results. Haskell's polymorphism works best “backwards”, i.e. the opposite way as in dynamic language: the caller requests what type the result should be, and the compiler figures out from this what the arguments should be. This works pretty much always, because as soon as the result is somehow used in the main program, the types in the whole computation have to be linked to a tree structure.

    OTOH, inferring the type of the result is often problematic: arguments may be optional, may themselves be linked only to the result, or given as polymorphic constants like Haskell number literals. So, if i doesn't turn up in the result of ^, avoid letting in occur in the arguments either.


    “Avoid” doesn't mean I don't ever write them, I just don't do so unless there's a good reason.