Arithmoi and phantom types

2
votes

I'm tyring to understand the use of phantom types in the package arithmoi (https://hackage.haskell.org/package/arithmoi-0.8.0.0). It helps to check if I'm working with the right residue class (Z/nZ).

The phantom type in question is data Mod (n :: Nat) = Mod Natural, and as I understand the constructor is not exported. But the constructor of SomeMod is exported, so I figure I must use it to construct ::Mod n variable. Moreover, one can read in the documentation, but I can't use it.

case modulo n m of
  SomeMod k -> process k -- Here k has type Mod m
  InfMod{}  -> error "impossible"

So I tried:

foo :: KnownNat m => Nat -> Nat -> Mod m
foo n m = case modulo n m of
    (SomeMod k) -> k
    otherwise -> error "some error"

I got an error about a variable m, m1 which is escaping its scope. I'm a bit puzzled.

1
haskellphantom-types
You might also like Statically enforcing that two objects were created from the same (Int) “seed”. While reading the question (and my answer there), when you see "seed", think "modulus"; when you see Collection, think Mod; when you see "merge collections", think "add" or "multiply" or similar such operations that only work when the moduli of the two arguments are equal. - Daniel Wagner

1 Answers

3
votes

Like IO, existentials cannot be escaped. Once in an existential, always in an existential. But that's okay -- if you're willing to admit KnownNat m, which your type signature claims you are willing to do, then you can just lift directly to that type.

foo :: KnownNat m => Natural -> Mod m
foo = fromIntegral