I have been trying to writing a program to implement polynomials on arbitrary field, a mathematical structure. I chose Haskell as the programming language, and I used the GADTs language extension. However, I don’t understand why GHCi can’t deduce the constraints of a.
The context:
-- irreducible.hs
{-# LANGUAGE GADTs #-}
infixl 6 .+
infixl 7 .*
class Ring a where
(.+) :: a -> a -> a
(.*) :: a -> a -> a
fneg :: a -> a
fzero :: a
funit :: a
class (Ring a) => Field a where
finv :: a -> a
data Polynomial a where
Polynomial :: (Field a) => [a] -> Char -> Polynomial a
instance (Show a) => Show (Polynomial a) where
show (Polynomial (a0:ar) x)
= show a0
++ concatMap (\(a, k) -> "+" ++ show a ++ x:'^':show k) (zip ar [0..])
show (Polynomial [] _) = show (fzero::a)
Explanation: A ring is something with addition and multiplication defined, where addition forms an (actually abelian) group, and multiplication forms a monoid. A field is a ring with the inverse of multiplication defined. The polynomials on a field is represented by a list of coefficients and a character. The character, for example 'x', indicates this polynomial is about the unknown variable x. For the zero polynomial, which is written as Polynomial [] 'x', I want it shows the zero element of the underlying field.
After running on GHCi, I got this:
irreducible.hs:59:28: error:
• Could not deduce (Show a0) arising from a use of ‘show’
from the context: Show a
bound by the instance declaration at irreducible.hs:55:10-40
or from: Field a
bound by a pattern with constructor:
Polynomial :: forall a. Field a => [a] -> Char -> Polynomial a,
in an equation for ‘show’
at irreducible.hs:59:9-23
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance (Show a, Show b) => Show (Either a b)
-- Defined in ‘Data.Either’
instance Show Ordering -- Defined in ‘GHC.Show’
instance Show Integer -- Defined in ‘GHC.Show’
...plus 25 others
...plus 87 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression: show (fzero :: a)
In an equation for ‘show’:
show (Polynomial [] _) = show (fzero :: a)
In the instance declaration for ‘Show (Polynomial a)’
|
59 | show (Polynomial [] _) = show (fzero::a)
| ^^^^^^^^^^^^^^^
irreducible.hs:59:34: error:
• Could not deduce (Ring a1) arising from a use of ‘fzero’
from the context: Show a
bound by the instance declaration at irreducible.hs:55:10-40
or from: Field a
bound by a pattern with constructor:
Polynomial :: forall a. Field a => [a] -> Char -> Polynomial a,
in an equation for ‘show’
at irreducible.hs:59:9-23
Possible fix:
add (Ring a1) to the context of
an expression type signature:
forall a1. a1
• In the first argument of ‘show’, namely ‘(fzero :: a)’
In the expression: show (fzero :: a)
In an equation for ‘show’:
show (Polynomial [] _) = show (fzero :: a)
|
59 | show (Polynomial [] _) = show (fzero::a)
|
Now let’s focus on the questionable part:
instance (Show a) => Show (Polynomial a) where
show (Polynomial (a0:ar) x) = show a0 ++ [...]
show (Polynomial [] _) = show (fzero::a)
In my opinion, Polynomial a guarantees a is an instance of Field, which implies a is an instance of Ring. So calling fzero::a, just like 42::Int, should be reasonable. Besides, I already wrote Show a as a constraint, and the constructor of Polynomial a has the shape Polynomial [a] Char, so it should also know the type of a0 is an instance of Show.
Apparently, the interpreter thinks differently. Where did I make a mistake?
From arrowd's comment:
The code is fine, but requires the ScopedTypeVariables extension, which makes the type variable a in fzero :: a refer to the previously introduced a.