zkFold / zkfold-base

ZkFold's Base library
https://zkfold.io
MIT License
16 stars 6 forks source link

Add `SymbolicRep` associated type to `SymbolicData` #277

Closed echatav closed 1 month ago

echatav commented 1 month ago

Add an associated SymbolicRep type to SymbolicData in preparation for Generic deriving, see #221 .

class SymbolicData x where
    type Context x :: (Type -> Type) -> Type
    type Support x :: Type
    type TypeSize x :: Natural
+  type SymbolicRep x :: Type -> Type
+  type SymbolicRep x = Vector (TypeSize x) -- default for now
+  -- type SymbolicRep x = GHC.Generic.Rep x -- default for generics later?

    -- | Returns the circuit that makes up `x`.
-    pieces :: x -> Support x -> Context x (Vector (TypeSize x))
+    pieces :: x -> Support x -> Context x (SymbolicRep x)

    -- | Restores `x` from the circuit's outputs.
-    restore :: (Support x -> Context x (Vector (TypeSize x))) -> x
+    restore :: (Support x -> Context x (SymbolicRep x)) -> x
echatav commented 1 month ago

I'm not sure this will work. When I did generic symbolic data before in a PoC, I took advantage of the fact that the datatypes were not just parametrized by their BaseField but that it was literally the last parameter of the datatype so I could use GHC.Generic.Rep1 instead of GHC.Generic.Rep. But it feels like it should work.

TurtlePU commented 1 month ago

We need this, yeah! Was going to call it Layout though, but SymbolicRep is also ok, I guess

Is there a problem with removing the TypeSize parameter altogether and migrating to Type -> Type immediately right now?

TurtlePU commented 1 month ago

I'm not sure this will work. When I did generic symbolic data before in a PoC, I took advantage of the fact that the datatypes were not just parametrized by their BaseField but that it was literally the last parameter of the datatype so I could use GHC.Generic.Rep1 instead of GHC.Generic.Rep. But it feels like it should work.

Just Rep from Generics, I'm afraid, is not going to work, because it wouldn't propagate the type parameters to built-in types correctly. But our default type family over Rep should work just fine.

echatav commented 1 month ago

Is there a problem with removing the TypeSize parameter altogether and migrating to Type -> Type immediately right now?

Not in theory, but, it's potentially an optimization for any call to typeSize to make use of a compile time calculation like TypeSize instead of having to use something like Foldable.length (pureRep ()) and it's convenient to have. As long as the compile time computations are not slowing us down as devs too much! I'd say keep it and have sensible laws when you have (KnownNat TypeSize, Representable Layout, Foldable Layout).

echatav commented 1 month ago

I feel like Support is like InputSpace and Layout is like OutputSpace.

TurtlePU commented 1 month ago

Not in theory, but, it's potentially an optimization for any call to typeSize to make use of a compile time calculation like TypeSize

After this migration, I doubt that we'd need typeSize at all! Other than that, I see your point

(Although we could still compute TypeSize from Layout with a type family)

TurtlePU commented 1 month ago

I feel like Support is like InputSpace and Layout is like OutputSpace.

Yeah, they're related, it's only that Support is Type while InputSpace was Type -> Type.

(And I'd prefer the support argument to keep being Type to keep the logic of adding input constraints separate from restore)