On Thu, Jan 8, 2009 at 3:11 PM, DavidA <polyom...@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 <d...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
