Skip to content

Add GCD and LCM type families to GHC.TypeNats

Motivation

Several libraries define a type family for the greatest common divisor on Nat:

  • constraints defines Gcd and provides a magic hack to derive (KnownNat n, KnownNat m) :- KnownNat (Gcd n m) .
  • ghc-typelits-extra defines GCD and provides a type checker plugin to evaluate this type family.
  • o-clock defines Gcd, which can be evaluated only for statically known Nats.
  • typenums defines GCD, 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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information