[Haskell-cafe] "Inconsistency" in support for phantom types?

[David Menendez]

On Thu, Jan 8, 2009 at 3:11 PM, DavidA <polyomino at f2s.com> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>