i have been trying implement chinese remainder theorem, specific case of 2 equations, using data.modular package. idea can specify each equation 1 modular number (x = (mod m) using number a (mod m)). here implementation.
{-# language datakinds, scopedtypevariables, typeoperators #-} import ghc.typelits import data.proxy (proxy (..)) import data.modular crt :: forall k1 k2 i. (knownnat k1, knownnat k2, integral i) => `mod` k1 -> `mod` k2 -> `mod` (k1 * k2) crt a1 a2 = tomod $ (unmod a1)*n2*(unmod n2') + (unmod a2)*n1*(unmod n1') n1 = getmodulus a1 :: n2 = getmodulus a2 :: n2' = inv $ (tomod n2 :: `mod` k1) n1' = inv $ (tomod n1 :: `mod` k2) getmodulus :: forall n j. (integral i, integral j, knownnat n) => `mod` n -> j getmodulus x = frominteger $ natval (proxy :: proxy n) i following error: could not deduce (knownnat (k1 * k2)) arising use of ‘tomod’. however, shouldn't ghc able arithmetic knownnat (k1 * k2)? also, weird reason, looks if had constructor mod type instead of tomod function, work. fail see how should make difference either...
i looking fix compile, including whatever extensions. would, however, not have make own version of data.modular if possible. (i think make work inelegantly , clumsily using mod constructor directly).
the cheap, cheesy way make compile add flexiblecontexts, add knownnat (k1 * k2) context of crt. once did this, call in ghci:
> crt (3 :: mod integer 5) (5 :: mod integer 7) 33 have fun working out how express coprime k1 k2 constraint... ;-)
Comments
Post a Comment