logic hierarchy

[echatav]

No description provided.

[echatav]

The Conditional (as well as Eq) instance for Vectors is derived via the Generically1 newtype. This is because the instance definition works for any Representable (and Foldable) over a Conditional (and Eq). But the choice of the Generically1 newtype is arbitrary. Similarly the choice of the Identity newtype for deriving Conditional (and Eq) instances from their Prelude variants is arbitrary.

Are there better newtypes to use for this purpose? Maybe new Representably and Prelusively newtypes are warranted?

[TurtlePU]

I think Generically1 is fine here

[TurtlePU]

Maybe it's better to use something else instead of Identity for Haskell types though...

[TurtlePU]

I think some documentation describing the laws of the class could be useful here

[TurtlePU]

Suggestion: move deriving stuff to corresponding .Generic/.Deriving modules (e.g. ZkFold.Base.Data.Eq.Generic or ZkFold.Base.Data.Eq.Deriving) to make modules shorter and more readable. I guess instances for K1 would still need to be defined in the main module, but this still would look cleaner and understandable (because it would be near instances of the main class for tuples which need it)

[echatav]

So 5 modules instead of 1? 🙃 I don't understand how this would work and not require mutually importing modules. I split it into 3 for now.

[TurtlePU]

ok, maybe at least visually separate the part on Generic deriving from the rest by a comment

[TurtlePU]

If we intend to use this instance in a generic context, then it is not as efficient as can be in a usual Haskell context as this would require $O(n)$ instead of the standard $O(1)$

[TurtlePU]

Don't know what to do here right now, I have the following idea but I don't know if this looks clean to you

type Choose a b = a -> a -> b -> a

class Boolean b where
  ...
  choice :: Choose a b -> Choose (e -> a) b
  -- chooses a closure for @b ~ base.Data.Bool@,
  -- creates new closure for @b ~ ZkFold.Symbolic.Data.Bool@

[TurtlePU]

(Terminology borrowed from here as this looks familiar)

[TurtlePU]

OR we could define two overlapping instances for Vector, but this would require the user to propagate the Conditional (Vector n x) constraint until BooleanOf x is known to be either base.Data.Bool or not

[TurtlePU]

OR we could define this choice to have a type (Conditional a, BooleanOf a ~ b) => Choose (e -> a) b, but this is not really better looking and makes Boolean and Conditional depend on each other unless we drop the dependency on Boolean in Conditional, but I don't like this approach

[echatav]

Hmmm, or perhaps it would be better to return to the design of having Conditional and Eq being multiparameter typeclasses? This is where we're heading for elliptic curve classes too. And it kind of makes sense, right? Because in particular a symbolic type is conditional in two ways with either a Haskell or Symbolic Bool. Associated type families mean making only one choice. Having it be multiparameter would mean we'd need to add an extra bool parameter the curve and point classes alongside their field parameter. On the otherhand, using multiparameter classes without functional dependencies degrades type inference, which makes it less usable. It's a design decision...

[vlasin]

Here is my reasoning. For x such that SymbolicData x, there is only one choice of boolean: Bool (Context x). So, ideally, there should be only one choice of Eq and Conditional for x.

Maybe we could override the generic implementation in the case of Interpreter? Would this solve the efficiency issue?

Regarding the elliptic curve hierarchy... The situation is different. As I noted, we have several options how the BaseField of the context can be related to the elliptic curve point type. Depending on the field choice, the implementation of the EC operations will be different. So, a multi-parametric approach is justified (and it is very much needed in the IVC, where we want to use all those options).

[TurtlePU]

So, ideally, there should be only one choice of Eq and Conditional for x.

This would be of course ideal, but, for Conditional, this is not really optimal -- for instance Conditional (Vector a) we have the following dilemma:

• if we keep only one instance, then this should be an instance which builds new vector componentwise, as done in the PR. This is suboptimal in pure Haskell context; and we would still need instance for pure Haskell if we want to write down language-agnostic generalized algorithms, which is the point of @echatav's refactoring.

• if we need more instances, then we need a multiparam class or something of the sort.

Actually, I think the current multiparam class definition is fine, it's the instances that have to be changed to:

class BoolType b => Conditional b a where
  ifThenElse :: b -> a -> a -> a

instance Conditional Haskell.Bool a where
  ifThenElse condition thenBranch elseBranch =
    if condition then thenBranch else elseBranch

instance SymbolicData a => Conditional (Bool (Context a)) a where
  ifThenElse (Bool c) t e = unPar1 $ interpolate [(zero, e), (one, t)] c

Where interpolate is a member of SymbolicData with the following type:

class ... => SymbolicData a where
  ...
  interpolate :: (Context a ~ c, Representable f) => [(BaseField c, a)] -> c f -> f a

(For now, interpolate can be defined only on lists of size 2 for simplicity of implementation)

The reasoning behind interpolate is such that once we have sum types in Symbolic, we will need to define an eliminator for them. For Bool, this is Conditional; to avoid defining a separate class for each sum type, I think it's better to include the common functionality in the base SymbolicData class and call into it.

In addition, this would allow to get rid of deriving for Conditional.

[TurtlePU]

return to the design of having Conditional and Eq being multiparameter typeclasses

Agreed about Conditional being multiparam, but I think Eq should still have an associated type, like this:

class Conditional (BooleanOf a) a => Eq a where
  type BooleanOf a :: Type
  (==) :: a -> a -> BooleanOf a
  (/=) :: a -> a -> BooleanOf a

My arguments are:

• Runtime performance doesn't differ much between Haskell.Eq and this Eq, even in pure context
• This makes sense because while Conditional is like an eliminator for a boolean datatype, Eq a is a property of a that its equality relation is decidable (well, what "decidable" means in Symbolic is an interesting question, but still).
• On the topic of type inference. In the case of Conditional, having it multiparam is fine because all the types can be inferred from the inputs. Output of Eq, on the other hand, cannot be inferred from the inputs directly so we have to provide some help to inference algorithm in form of either fundeps or associated types.
• From the UX standpoint, in this solution users wouldn't have to write down Conditional instances at all, and Eq instance deriving would be just instance Symbolic c => Eq (... symbolic datatype ...) with no reference to Bool c whatsoever, which is as close to usual Haskell as possible
• If you still need to get Bool c as a result of x == y where x, y :: a and Haskell.Eq a, you can just use FromConstant Haskell.Bool (Bool c). Or a Conditional Haskell.Bool (Bool c). This can be given a general definition like this:

(?==) :: (Eq a, FromConstant (BooleanOf a) b) => a -> a -> b
x ?== y = fromConstant (x == y)

[echatav]

^ Yes, I agree that having its boolean be inferable from a type makes more sense for Eq than Conditional.

[TurtlePU]

Additional reasoning on why BoolType, Conditional and Eq have to be defined in different modules -- they mean completely different, although related concepts:

• BoolType a states that a is a boolean algebra
• Conditional b a states that a belongs to the universe where b can be eliminated like a boolean
• Eq a states that a has decidable equality relative to BooleanOf a