Noether

maximally polymorphic number theory / abstract algebra in haskell

The part I'm working on at present develops a highly polymorphic numeric hierarchy. Unlike almost every other project (including the great subhask, which is by far the biggest inspiration for this project), all typeclasses representing algebraic structures are "tagged" with the operations that the base type supports. The intention is to have, without newtyping, things like automatically specified L-vector space instances for any K-vector space with K / L a (nice) field extension.

Other stuff

Some other stuff I'm thinking about includes polymorphic numeric literals, possibly along the lines of this:

type family NumericLit (n :: Nat) = (c :: * -> Constraint) where
  NumericLit 0 = Neutral Add
  NumericLit 1 = Neutral Mul
  -- NumericLit 2 = Field Add Mul
  -- NumericLit n = NumericLit (n - 1)
  NumericLit n = Ring Add Mul

fromIntegerP :: forall n a. (KnownNat n, NumericLit n a) => Proxy n -> a
fromIntegerP p =
  case sameNat p (Proxy :: Proxy 0) of
    Just prf -> gcastWith prf zero'
    Nothing -> case sameNat p (Proxy :: Proxy 1) of
      Just prf -> gcastWith prf one'
      Nothing -> undefined -- unsafeCoerce (val (Proxy :: Proxy a))
        -- where
        --   val :: (Field Add Mul b) => Proxy b -> b
        --   val _ = one + undefined -- fromIntegerP (Proxy :: Proxy (n - 1))

The original core of the project is a short implementation of elliptic curve addition over Q, which I've put on hold temporarily as I try to work out the issues outlined above first. This part uses a Protolude "fork" called Lemmata that I expect will evolve over time.