On Thu, Jan 8, 2009 at 3:11 PM, DavidA wrote:

Hi,

I have run into what appears to be an inconsistency in the support for using phantom types to parameterize other types. Here's an example (don't pay too much attention to the maths, it's just there to motivate the example). I want to define types for the finite fields with 2, 3 and 5 elements (clock arithmetic modulo 2, 3 or 5).

{-# OPTIONS_GHC -fglasgow-exts #-}

class IntegerAsType a where value :: a -> Integer

-- three phantom types: data T2 instance IntegerAsType T2 where value _ = 2 data T3 instance IntegerAsType T3 where value _ = 3 data T5 instance IntegerAsType T5 where value _ = 5

newtype Fp n = Fp Integer deriving (Eq,Ord)

-- our three finite field types: type F2 = Fp T2 type F3 = Fp T3 type F5 = Fp T5

-- Show and Num instances instance Show (Fp n) where show (Fp x) = show x

instance IntegerAsType n => Num (Fp n) where Fp x + Fp y = Fp $ (x+y) `mod` value (undefined :: n) negate (Fp 0) = 0 negate (Fp x) = Fp $ value (undefined :: n) - x Fp x * Fp y = Fp $ (x*y) `mod` value (undefined :: n) fromInteger m = Fp $ m `mod` value (undefined :: n)

Now, we can also define a Fractional instance, using the extended Euclid algorithm (given at the end)

-- n must be prime instance IntegerAsType n => Fractional (Fp n) where recip 0 = error "Fp.recip 0" recip (Fp x) = let p = value (undefined :: n) (u,v,1) = extendedEuclid x p -- so ux+vp = 1. (We know the gcd is 1 as p prime) in Fp $ u `mod` p

Now, the problem I've run into is, what do I do if I want to define a function parameterised over the phantom types, but without doing it as part of a type class instance? For example, suppose that I had just wanted to define "inv" as a synonym for "recip":

inv :: IntegerAsType n => Fp n -> Fp n inv 0 = error "Fp,inv 0" inv (Fp x) = let p = value (undefined :: n) (u,v,1) = extendedEuclid x p in Fp $ u `mod` p

"inv" has exactly the same code as "recip", but now the IntegerAsType constraint is part of the type signature, rather than an instance constraint. It seems that this means that the constraint is not available to the code during compilation, because when I try to compile this I get Ambiguous type variable `n' in the constraint: `IntegerAsType n' arising from a use of `value' at Test.hs:52:21-42 Probable fix: add a type signature that fixes these type variable(s)

It seems to me highly desirable that this code should compile as expected, just as the recip code compiles. Is it a bug in GHC, or a missing language feature, or is there a "better" way to do what I'm trying to do?

Type variables don't scope over function definitions, so your example is equivalent to:

inv :: IntegerAsType n => Fp n -> Fp n inv 0 = error "Fp,inv 0" inv (Fp x) = let p = value (undefined :: a) (u,v,1) = extendedEuclid x p in Fp $ u `mod` p

In GHC, you can use the ScopedTypeVariables extension to avoid that problem. (See section 8.8.6 of the manual.)

{-# LANGUAGE ScopedTypeVariables #-} ... inv :: forall n. IntegerAsType n => Fp n -> Fp n inv 0 = error "Fp,inv 0" inv (Fp x) = let p = value (undefined :: n) (u,v,1) = extendedEuclid x p in Fp $ u `mod` p

Or, for Haskell 98 compatibility, you can use a function to transform the types.

getFpType :: Fp n -> n getFpType _ = undefined

inv :: IntegerAsType n => Fp n -> Fp n inv 0 = error "Fp,inv 0" inv n@(Fp x) = let p = value (getFpType n) (u,v,1) = extendedEuclid x p in Fp $ u `mod` p

-- Dave Menendez http://www.eyrie.org/~zednenem/

inv :: IntegerAsType n => Fp n -> Fp n ^ ^ ^

On 8 Jan 2009, at 23:11, DavidA wrote: this "n" --------------+-------+-------|

inv 0 = error "Fp,inv 0" inv (Fp x) = let p = value (undefined :: n) ^ and this one ------------------------------|

are different beasts. You can try something like this: getN :: Fp n -> n getN _ = undefined inv a@(Fp x) = let p = value $ getN a ...