Add GCD and LCM type families to GHC.TypeNats
Motivation
Several libraries define a type family for the greatest common divisor on Nat
:
-
constraints
definesGcd
and provides a magic hack to derive(KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
. -
ghc-typelits-extra
definesGCD
and provides a type checker plugin to evaluate this type family. -
o-clock
definesGcd
, which can be evaluated only for statically knownNat
s. -
typenums
definesGCD
, also only for statically known indices.
This is a suboptimal situation, causing significant duplication and (more importantly) complicating APIs of respective packages and interoperation between them.
(The main application of type-level gcd is defining type-level rational numbers, but it is also important for safe modular arithmetic)
Proposal
Provide a type family GCD
(and, probably, LCM
) immediately from GHC.TypeNats
with built-in evaluation support.