Currently, the story of deriving Symbolic typeclasses is as follows:
SymbolicData provides some instances for tuples, which are then used via newtype deriving.
pros: dead simple
cons: forces all user-defined datatypes to be tuples
Conditional has a single instance for all SymbolicData
pros: no need to write instance by hand
cons: introduces unnecessary coupling of circuits in a datatype via pieces, while e.g. separate fields of a record can be kept separate in an appropriate instance implementation:
instance (Conditional b a, Conditional b c) => Conditional b (a, c) where
bool (xf, yf) (xt, yt) b = (bool xf xt b, bool yf yt b)
Eq
pros: deriving via a Structural instance which is good enough for most builtin datatypes
cons: such deriving is not compositional and is not effective if, e.g., someone uses Structural on a datatype which contains Bool c
Ord: same as with Eq, deriving via Lexicographical has very limited use because it breaks compositionality, so it actually better not be used even with datatypes which contain UInt.
We can do better. Using Generic as described on this wiki page, we can do the following:
[x] Default overridable SymbolicData implementation via Generic: #299
[x] #372
class (Support a ~ (), Representable (Layout a)) => SymbolicInput a where
isValid :: a -> Bool (Context a)
default isValid :: (Generic a, GSymbolicInput (Rep a)) => a -> Bool (Context a)
-- checks if components are valid and folds the results.
-- deserves its own name if a user wants to both check the components
-- AND provide their own invariant.
[ ] Make Conditional a part of SymbolicData: #296
[ ] #385
class Eq b a where
(==) :: a -> a -> b
default (==) :: (Generic a, GEq b (Rep a)) => a -> a -> b
-- compares values component-wise and folds the results
[ ] Default overridable implementation of Ord via Generic:
class Ord b a where
(<) :: a -> a -> b
default (<) :: (Generic a, GOrd b (Rep a)) => a -> a -> b
-- compares values component-wise and folds the results??
-- this is actually harder than it looks to do efficiently, needs investigation
I would like to provide instances for SymbolicData and Conditional instead of default implementations because I do not expect them to have any other instances other than the ones we can generate via Generic. On the other hand, the rest of the typeclasses can have custom (or more performant) instances for user-defined datatypes; in addition, for SymbolicInput this can serve as an additional sanity-check if the datatype defined by the user is indeed qualified to be an input to the smart contract.
If there are any other suggestions, please comment.
Currently, the story of deriving
Symbolic
typeclasses is as follows:SymbolicData
provides some instances for tuples, which are then used via newtype deriving.Conditional
has a single instance for allSymbolicData
pieces
, while e.g. separate fields of a record can be kept separate in an appropriate instance implementation:Eq
Structural
instance which is good enough for most builtin datatypesStructural
on a datatype which containsBool c
Ord
: same as withEq
, deriving viaLexicographical
has very limited use because it breaks compositionality, so it actually better not be used even with datatypes which containUInt
.We can do better. Using
Generic
as described on this wiki page, we can do the following:SymbolicData
implementation viaGeneric
: #299Conditional
a part ofSymbolicData
: #296Ord
viaGeneric
:I would like to provide instances for
SymbolicData
andConditional
instead of default implementations because I do not expect them to have any other instances other than the ones we can generate viaGeneric
. On the other hand, the rest of the typeclasses can have custom (or more performant) instances for user-defined datatypes; in addition, forSymbolicInput
this can serve as an additional sanity-check if the datatype defined by the user is indeed qualified to be an input to the smart contract.If there are any other suggestions, please comment.