Add ChineseRemainderS functions

[CarlEdman]

This proposed patch adds two new functions to this module; chineseRemainders/chineseRemainders2 (note the trailing S). These are the equivalent of the existing chineseRemainder/chineseRemainder2 functions, except:

1. They use the recently introduced SomeMod type both for its parameters and its results.
2. As a consequence they handle single-point congruence classes constructed with SomeMod's InfMod constructor.
3. They will return a solution for non-pairwise co-prime moduli, if one exists.

[Bodigrim]

Yes, put tests into https://github.com/CarlEdman/arithmoi/blob/patch-1/test-suite/Math/NumberTheory/Moduli/ChineseTests.hs

You can continue editing files in https://github.com/CarlEdman/arithmoi/blob/patch-1 branch, changes will appear here automatically.

[Bodigrim]

Maybe one could even come up with some sort of type magic to construct the type Maybe (Mod (lcm m n)) to give the correct answer in all cases (#69).

It is possible, but clumsy, because there is no type level division available. Things may change, if https://ghc.haskell.org/trac/ghc/ticket/13652 get implemented. Once I have implemented GCD on type level, but it is too slow for any practical purposes.

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy
import GHC.TypeLits

type family Cmp123 (o :: Ordering) (x :: Nat) (y :: Nat) (z :: Nat) :: Nat where
  Cmp123 LT x y z = x
  Cmp123 EQ x y z = y
  Cmp123 GT x y z = z

type family GCD (x :: Nat) (y :: Nat) :: Nat where
  GCD 0 x = x
  GCD x 0 = x
  GCD x y = Cmp123 (CmpNat x y) (GCD x (y - x)) x (GCD (x - y) y)

test :: Proxy (GCD 372 48) -> Proxy 12
test = id

[Bodigrim]

Your suggestion regarding a chineseRemainders2' :: Mod m -> Mod n -> Maybe (Mod (m * n)) is well taken. I've not yet written it because I couldn't make it work, doubtlessly due to my imperfect understanding of the dependent type system (#69).

Sorry, I missed an important detail: the signature must contain KnownNat constraints. It may start like this:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators    #-}

import GHC.TypeNats.Compat
import Math.NumberTheory.Moduli.Class

chineseRemainders2'
  :: (KnownNat m, KnownNat n, KnownNat (m * n))
  => Mod m -> Mod n -> Maybe (Mod (m * n))
chineseRemainders2' x y = undefined

[Bodigrim]

Well, I'd better try it myself before giving wrong advices. The problem with the signature above is that in a context like

someChineseRemainders' :: SomeMod -> SomeMod -> SomeMod
someChineseRemainders' 
  (SomeMod x) (SomeMod y) 
  = (SomeMod x) (SomeMod y) = SomeMod (fromMaybe undefined $ chineseRemainders2' x y)

we have KnownNat m and KnownNat n, but not KnownNat (m * n). And if we remove the latter constraint from chineseRemainders2' declaration, we will not be able to wrap the result into SomeMod.

This is exactly a use case for ghc-typelits-knownnat package (add it to arithmoi.cabal). Following snippet should work fine:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators    #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

import Data.Maybe
import GHC.TypeNats.Compat
import Math.NumberTheory.Moduli.Class

chineseRemainders2'
  :: (KnownNat m, KnownNat n, KnownNat (m * n))
  => Mod m -> Mod n -> Maybe (Mod (m * n))
chineseRemainders2' x y = undefined x y

someChineseRemainders2'
  :: SomeMod -> SomeMod -> SomeMod
someChineseRemainders2'
  (SomeMod x) (SomeMod y) = SomeMod (fromMaybe undefined $ chineseRemainders2' x y)

[Bodigrim]

@CarlEdman feel free to poke me, if there are difficulties (especially technical) of any kind. I am afraid that my comments above appeared to be too frightening.

[CarlEdman]

@Bodigrim No need for fear! Your comments are much appreciated. My tardiness is related to other time pressures, rather than anything you said.

[Bodigrim]

Cool. I did not mean to put pressure on you; sorry, if it sounded this way.

[Bodigrim]

BTW there is a simpler solution to KnownNat issue, without type checker plugins. timesNat from constraints should do the job.

http://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint-Nat.html#v:timesNat

[Bodigrim]

The complete snippet with constraints looks this way:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}

import Data.Maybe
import GHC.TypeNats.Compat
import Math.NumberTheory.Moduli.Class
import Data.Constraint
import Data.Constraint.Nat (timesNat)

chineseRemainders2'
  :: (KnownNat m, KnownNat n)
  => Mod m -> Mod n -> Maybe (Mod (m * n))
chineseRemainders2' x y = undefined x y

someChineseRemainders2'
  :: SomeMod -> SomeMod -> SomeMod
someChineseRemainders2'
  (SomeMod (x :: Mod m)) (SomeMod (y :: Mod n)) = case timesNat @m @n of
    Sub Dict -> SomeMod (fromMaybe undefined $ chineseRemainders2' x y)

[Bodigrim]

It is possible, but clumsy, because there is no type level division available. Things may change, if https://ghc.haskell.org/trac/ghc/ticket/13652 get implemented.

Type-level division landed into base-4.11, shipped with GHC 8.4: https://downloads.haskell.org/~ghc/master/libraries/base/base/GHC-TypeNats.html#t:Div
Now one can implement an honest type-level GCD.

[Bodigrim]

@CarlEdman thanks for valuable ideas! I reworked your code in a1d86d8, avoiding factorisation.

Unfortunately and despite all discussion above, having a function with known moduli on type level is next to useless.

chineseCoprimeMod :: (KnownNat m1, KnownNat m2) => Mod m1 -> Mod m2 -> Maybe (Mod (m1 * m2))

The problem is that even if inside chineseCoprimeMod we have a proof of KnownNat (m1 * m2), the consumers of its results does not. We should either return the proof explicitly (which is too much type-foo IMO), or repeat the proof each time, where we call chineseCoprimeMod. For instance,

:set -XDataKinds -XTypeApplications
import Data.Constraint
import Data.Constraint.Nat (timesNat)
print $ case timesNat @2 @3 of 
  Sub Dict -> fmap SomeMod (chineseCoprimeMod (1 :: Mod 2) (2 :: Mod 3))

It does not look worth a trouble, so I decided to remove such functions from API.