Refactor Symbolic & SymbolicData

[echatav]

• [x] Move & modify DiscreteField from Symbolic to Basic
• [x] Create a Trichotomy class for discrete fields with a total ordering with law of trichotomy
• [x] Create Trichotomy instances for Zp
• [ ] Create Trichotomy instance for ArithmeticCircuit
• [x] Redefine Symbolic using Trichotomy
• [x] Create a VectorSpace class for vector spaces over a field with a Basis type
• [ ] Create lots of VectorSpace instances and relate to Representable functors and generics
• [x] Redefine SymbolicData using VectorSpace
• [ ] Reimplement all SymbolicData instances as VectorSpace and associated instances
• [x] Create a Tensorial class for multlinear maps of vector spaces with InputBasis and OutputSpace types
• [ ] Redefine Arithmetizable using new SymbolicData
• [ ] Reimplement all Arithmetizable instances
• [ ] Create comparison classes Eq and Ord for symbolic data with default Foldable implementations and lots of instances
• [x] Create algebraic classes (AdditiveSemigroup, etc) for SymbolicData
• [ ] Implement algebraic classes for Identity, UInt n
• [ ] Implement algebraic classes for Vector n u
• [ ] Replace list algorithms in UInt and ByteString with vector algorithms

[echatav]

@TurtlePU

Arithmetization looks like this then:

class Arithmetizable a f where
type InputRep a f :: Type
type OutputRep a f :: Type
arithmetize :: f -> (InputRep a f -> ArithmeticCircuit a) -> OutputRep a f -> ArithmeticCircuit a

instance SymbolicData a u => Arithmetizable a (u (ArithmeticCircuit a)) where type InputRep a (u (ArithmeticCircuit a)) = Void type OutputRep a (u (ArithmeticCircuit a)) = Rep a u arithmetize c _ = index c

instance (SymbolicData a x, Arithmetizable a f) => Arithmetizable a (x (ArithmeticCircuit a) -> f) where type InputRep a (x (ArithmeticCircuit a) -> f) = Either (Rep a x) (InputRep a f) type OutputRep a (x (ArithmeticCircuit a) -> f) = OutputRep a f arithmetize f i = arithmetize (f $ tabulate (i . Left)) (i . Right)

[vlasin]

@TurtlePU

Arithmetization looks like this then:

class Arithmetizable a f where
  type InputRep a f :: Type
  type OutputRep a f :: Type
  arithmetize :: f -> (InputRep a f -> ArithmeticCircuit a) -> OutputRep a f -> ArithmeticCircuit a

instance SymbolicData a u => Arithmetizable a (u (ArithmeticCircuit a)) where
  type InputRep a (u (ArithmeticCircuit a)) = Void
  type OutputRep a (u (ArithmeticCircuit a)) = Rep a u
  arithmetize c _ = index c

instance (SymbolicData a x, Arithmetizable a f) => Arithmetizable a (x (ArithmeticCircuit a) -> f) where
  type InputRep a (x (ArithmeticCircuit a) -> f) = Either (Rep a x) (InputRep a f)
  type OutputRep a (x (ArithmeticCircuit a) -> f) = OutputRep a f
  arithmetize f i = arithmetize (f $ tabulate (i . Left)) (i . Right)

Why does arithmetize have this signature?

[TurtlePU]

@vlasin InputRep is an indexing type for function inputs, OutputRep is an indexing type for function outputs To arithmetize a function of type f, we need to have prepared inputs in a mapping of type InputRep a f -> ArithmeticCircuit a and generate outputs in form of a mapping OutputRep a f -> ArithmeticCircuit a

[vlasin]

@vlasin InputRep is an indexing type for function inputs, OutputRep is an indexing type for function outputs To arithmetize a function of type f, we need to have prepared inputs in a mapping of type InputRep a f -> ArithmeticCircuit a and generate outputs in form of a mapping OutputRep a f -> ArithmeticCircuit a

Got you, makes sense.

[echatav]

@TurtlePU here's a variant I got past GHC.

class Arithmetizable a f where
  arithmetize :: f -> (Inputs a f -> ArithmeticCircuit a) -> Outputs a f -> ArithmeticCircuit a

type family Inputs a f where
  Inputs a (x (ArithmeticCircuit a) -> f) =
    Either (Basis (ArithmeticCircuit a) x) (Inputs a f)
  Inputs a (u (ArithmeticCircuit a)) = Void

type family Outputs a f where
  Outputs a (x (ArithmeticCircuit a) -> f) = Outputs a f
  Outputs a (u (ArithmeticCircuit a)) = Basis (ArithmeticCircuit a) u

instance {-# OVERLAPPABLE #-}
  ( SymbolicData (ArithmeticCircuit a) u
  , Basis (ArithmeticCircuit a) u ~ Outputs a (u (ArithmeticCircuit a))
  ) => Arithmetizable a (u (ArithmeticCircuit a)) where
    arithmetize c _ = indexV c

instance {-# OVERLAPPING #-}
  ( SymbolicData (ArithmeticCircuit a) x
  , Arithmetizable a f
  ) => Arithmetizable a (x (ArithmeticCircuit a) -> f) where
    arithmetize f i = arithmetize (f $ tabulateV (i . Left)) (i . Right)