Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

logic hierarchy #421

Draft
wants to merge 9 commits into
base: main
Choose a base branch
from
Draft

logic hierarchy #421

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
340ba59
logic hierarchy
echatav Dec 24, 2024
0a884fd
stylish-haskell auto-commit
echatav Dec 24, 2024
acc0d5f
Update Logical.hs
echatav Dec 24, 2024
83f8d23
split it
echatav Dec 24, 2024
a04e9a0
stylish-haskell auto-commit
echatav Dec 24, 2024
5fa59a5
Merge branch 'main' into eitan-logic-hierarchy
echatav Dec 24, 2024
6e4576c
Update Eq.hs
echatav Dec 24, 2024
e069604
Merge branch 'eitan-logic-hierarchy' of https://github.com/zkFold/zkf…
echatav Dec 24, 2024
a644bf5
Update Eq.hs
echatav Dec 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 34 additions & 0 deletions symbolic-base/src/ZkFold/Base/Data/Boolean.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
module ZkFold.Base.Data.Boolean
( Boolean (..)
, all, any, and, or
) where

import Control.Category
import qualified Data.Bool as H
import Data.Foldable hiding (all, and, any, elem, or)
import qualified Prelude as H

class Boolean b where
true, false :: b
not :: b -> b
(&&), (||), xor :: b -> b -> b

instance Boolean H.Bool where
true = H.True
false = H.False
not = H.not
(&&) = (H.&&)
(||) = (H.||)
xor = (H./=)

all :: (Boolean b, Foldable t) => (x -> b) -> t x -> b
all f = foldr ((&&) . f) true

any :: (Boolean b, Foldable t) => (x -> b) -> t x -> b
any f = foldr ((||) . f) false

and :: (Boolean b, Foldable t) => t b -> b
and = all id

or :: (Boolean b, Foldable t) => t b -> b
or = any id
100 changes: 100 additions & 0 deletions symbolic-base/src/ZkFold/Base/Data/Conditional.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Data.Conditional
( Conditional (..)
, GConditional (..)
) where

import qualified Data.Bool as H
import Data.Functor.Identity
import qualified Data.Functor.Rep as R
import Data.Kind
import qualified GHC.Generics as G
import Prelude (type (~))

import ZkFold.Base.Algebra.Basic.Number
import ZkFold.Base.Data.Boolean
import ZkFold.Base.Data.Vector

class Boolean (BooleanOf a) => Conditional a where

type BooleanOf a :: Type
type BooleanOf a = GBooleanOf (G.Rep a)

ifThenElse :: BooleanOf a -> a -> a -> a
default ifThenElse ::
( G.Generic a
, GConditional (G.Rep a)
, BooleanOf a ~ GBooleanOf (G.Rep a)
) => BooleanOf a -> a -> a -> a
ifThenElse b t f = G.to (gifThenElse b (G.from t) (G.from f))

instance
( Conditional x0
, Conditional x1
, BooleanOf x0 ~ BooleanOf x1
) => Conditional (x0,x1)

instance
( Conditional x0
, Conditional x1
, Conditional x2
, BooleanOf x0 ~ BooleanOf x1
, BooleanOf x1 ~ BooleanOf x2
) => Conditional (x0,x1,x2)

instance
( Conditional x0
, Conditional x1
, Conditional x2
, Conditional x3
, BooleanOf x0 ~ BooleanOf x1
, BooleanOf x1 ~ BooleanOf x2
, BooleanOf x2 ~ BooleanOf x3
) => Conditional (x0,x1,x2,x3)

instance (R.Representable v, Conditional x)
=> Conditional (G.Generically1 v x) where
type BooleanOf (G.Generically1 v x) = BooleanOf x
ifThenElse b (G.Generically1 vt) (G.Generically1 vf) =
G.Generically1 (R.mzipWithRep (ifThenElse b) vt vf)

deriving via G.Generically1 (Vector n) x
instance (KnownNat n, Conditional x) => Conditional (Vector n x)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)$

Copy link
Contributor

@TurtlePU TurtlePU Dec 24, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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@

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(Terminology borrowed from here as this looks familiar)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

@echatav echatav Dec 26, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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...

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Contributor

@TurtlePU TurtlePU Dec 30, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@TurtlePU TurtlePU Dec 30, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


deriving via G.Generically1 ((->) x) y
instance Conditional y => Conditional (x -> y)

instance Conditional (Identity x) where
type BooleanOf (Identity x) = H.Bool
ifThenElse b t f = if b then t else f

class Boolean (GBooleanOf f) => GConditional f where
type GBooleanOf f :: Type
gifThenElse :: GBooleanOf f -> f a -> f a -> f a

instance
( GConditional u
, GConditional v
, Boolean (GBooleanOf u)
, GBooleanOf u ~ GBooleanOf v
) => GConditional (u G.:*: v) where
type GBooleanOf (u G.:*: v) = GBooleanOf u
gifThenElse b (t0 G.:*: t1) (f0 G.:*: f1) =
gifThenElse b t0 f0 G.:*: gifThenElse b t1 f1

instance (R.Representable v, GConditional u)
=> GConditional (v G.:.: u) where
type GBooleanOf (v G.:.: u) = GBooleanOf u
gifThenElse b (G.Comp1 vt) (G.Comp1 vf) =
G.Comp1 (R.mzipWithRep (gifThenElse b) vt vf)

instance GConditional v => GConditional (G.M1 i c v) where
type GBooleanOf (G.M1 i c v) = GBooleanOf v
gifThenElse b (G.M1 t) (G.M1 f) = G.M1 (gifThenElse b t f)

instance Conditional x => GConditional (G.K1 i x) where
type GBooleanOf (G.K1 i x) = BooleanOf x
gifThenElse b (G.K1 t) (G.K1 f) = G.K1 (ifThenElse b t f)
101 changes: 101 additions & 0 deletions symbolic-base/src/ZkFold/Base/Data/Eq.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE TypeOperators #-}

module ZkFold.Base.Data.Eq
( Eq (..)
, elem
, GEq (..)
) where

import Data.Foldable hiding (all, and, any, elem, or)
import Data.Functor.Identity
import qualified Data.Functor.Rep as R
import qualified GHC.Generics as G
import Prelude (type (~))
import qualified Prelude as H

import ZkFold.Base.Algebra.Basic.Number
import ZkFold.Base.Data.Boolean
import ZkFold.Base.Data.Conditional
import ZkFold.Base.Data.Vector

class Conditional a => Eq a where

(==) :: a -> a -> BooleanOf a
default (==) ::
( G.Generic a
, GEq (G.Rep a)
, BooleanOf a ~ GBooleanOf (G.Rep a)
) => a -> a -> BooleanOf a
x == y = geq (G.from x) (G.from y)

(/=) :: a -> a -> BooleanOf a
TurtlePU marked this conversation as resolved.
Show resolved Hide resolved
default (/=) ::
( G.Generic a
, GEq (G.Rep a)
, BooleanOf a ~ GBooleanOf (G.Rep a)
) => a -> a -> BooleanOf a
x /= y = gneq (G.from x) (G.from y)

instance
( Eq x0, Eq x1
, BooleanOf x0 ~ BooleanOf x1
) => Eq (x0,x1)

instance
( Eq x0
, Eq x1
, Eq x2
, BooleanOf x0 ~ BooleanOf x1
, BooleanOf x1 ~ BooleanOf x2
) => Eq (x0,x1,x2)

instance
( Eq x0
, Eq x1
, Eq x2
, Eq x3
, BooleanOf x0 ~ BooleanOf x1
, BooleanOf x1 ~ BooleanOf x2
, BooleanOf x2 ~ BooleanOf x3
) => Eq (x0,x1,x2,x3)

instance (Foldable v, R.Representable v, Eq x)
=> Eq (G.Generically1 v x) where
G.Generically1 vx == G.Generically1 vy =
and (R.mzipWithRep (==) vx vy)
G.Generically1 vx /= G.Generically1 vy =
or (R.mzipWithRep (/=) vx vy)

deriving via G.Generically1 (Vector n) x
instance (KnownNat n, Eq x) => Eq (Vector n x)

instance H.Eq x => Eq (Identity x) where
(==) = (H.==)
(/=) = (H./=)

elem :: (Eq a, Foldable t) => a -> t a -> BooleanOf a
elem x = any (== x)

class GConditional f => GEq f where
geq :: f a -> f a -> GBooleanOf f
gneq :: f a -> f a -> GBooleanOf f

instance
( GEq u, GEq v
, GBooleanOf u ~ GBooleanOf v
) => GEq (u G.:*: v) where
geq (x0 G.:*: x1) (y0 G.:*: y1) = geq x0 y0 && geq x1 y1
gneq (x0 G.:*: x1) (y0 G.:*: y1) = gneq x0 y0 || gneq x1 y1

instance (Foldable v, R.Representable v, GEq u) => GEq (v G.:.: u) where
geq (G.Comp1 vx) (G.Comp1 vy) = and (R.mzipWithRep geq vx vy)
gneq (G.Comp1 vx) (G.Comp1 vy) = or (R.mzipWithRep gneq vx vy)

instance GEq v => GEq (G.M1 i c v) where
geq (G.M1 x) (G.M1 y) = geq x y
gneq (G.M1 x) (G.M1 y) = gneq x y

instance Eq x => GEq (G.K1 i x) where
geq (G.K1 x) (G.K1 y) = x == y
gneq (G.K1 x) (G.K1 y) = x /= y
3 changes: 3 additions & 0 deletions symbolic-base/symbolic-base.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,10 @@ library
ZkFold.Base.Algebra.Polynomials.Multivariate.Substitution
ZkFold.Base.Algebra.Polynomials.Univariate
ZkFold.Base.Control.HApplicative
ZkFold.Base.Data.Boolean
ZkFold.Base.Data.ByteString
ZkFold.Base.Data.Conditional
ZkFold.Base.Data.Eq
ZkFold.Base.Data.Functor.Rep
ZkFold.Base.Data.HFunctor
ZkFold.Base.Data.List.Infinite
Expand Down
Loading