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.

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

EC symbolic #396

Merged
merged 13 commits into from
Dec 13, 2024
Merged

EC symbolic #396

merged 13 commits into from
Dec 13, 2024

Conversation

echatav
Copy link
Contributor

@echatav echatav commented Dec 10, 2024

Change the Point type and friends so that they may support Symbolic computation.

Resolves #400

@echatav echatav marked this pull request as ready for review December 11, 2024 03:04
@echatav echatav added the ready for review needs review before merge label Dec 11, 2024
@vlasin vlasin requested review from TurtlePU and vks4git December 11, 2024 20:30
Copy link
Contributor

@vks4git vks4git left a comment

Choose a reason for hiding this comment

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

Awesome! RebindableSyntax is such a nice touch

@echatav echatav merged commit 573af1a into main Dec 13, 2024
1 check passed
@echatav echatav deleted the eitan-ec-symbolic branch December 13, 2024 00:08
@@ -65,8 +64,6 @@ deriving instance Show (c Par1) => Show (Bool c)
instance {-# OVERLAPPING #-} (Eq a, MultiplicativeMonoid a) => Show (Bool (Interpreter a)) where
show (fromBool -> x) = if x == one then "True" else "False"

deriving newtype instance Symbolic c => SymbolicData (Bool c)
Copy link
Contributor

Choose a reason for hiding this comment

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

Why did this instance have to be moved?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Hmmm, it might not have to have been. I had a cycle at one point but not sure if this in fact solved it or something else.

@TurtlePU
Copy link
Contributor

Really like the way elliptic curve API changed! So clean and polymorphic now

Hope we will sort the stuff with Conditional/Eq/Ord out so that modules in Base do not depend on Symbolic, just rubs me the wrong way...

@echatav
Copy link
Contributor Author

echatav commented Dec 13, 2024

Hope we will sort the stuff with Conditional/Eq/Ord out so that modules in Base do not depend on Symbolic, just rubs me the wrong way...

I agree. Conceptually the BoolType/Conditional/Eq/Ord hierarchy I believe belong in Base since they are "polymorphic" across Haskell & Symbolic. I don't know if all dependencies can be cut (it may be possible) but at least organizationally, it makes sense to move/reorganize these modules.

@TurtlePU
Copy link
Contributor

TurtlePU commented Dec 13, 2024

(Though I still believe that we should have Symbolic-specific versions of Eq and Ord classes for a cleaner API for Symbolic users who are not involved in language-polymorphic stuff)

@echatav
Copy link
Contributor Author

echatav commented Dec 13, 2024

^ I think this is best handled by re-exporting and properly documenting in friendly ways these terms and others in a Symbolic.Prelude. The logical classes are similar to the algebraic classes in that users of Symbolic should be able to use them seamlessly whether they know they also work in Haskell too.

@TurtlePU
Copy link
Contributor

TurtlePU commented Dec 13, 2024

Well, I'm only concerned about Symbolic functions which are polymorphic in datatypes. Take an example like this:

find :: a -> Vector n a -> Maybe c (UInt k r c)

What should the constraints look like?

With language-agnostic Eq

find :: (Symbolic c, SymbolicData a, Context a ~ c, Support a ~ Proxy c, Eq a, BooleanOf a ~ Bool c) => a -> Vector n a -> Maybe c (UInt k r c)

With Symbolic-specific Eq

class SymbolicData a => Eq a where
  (==) :: a -> a -> Bool (Context a)

find :: (Eq a, Context a ~ c) => a -> Vector n a -> Maybe c (UInt k r c)

P.S. We can introduce type aliases however we want, sure, but the real interface the user is going to interact with are compiler errors, and usually type aliases are not present there

P.P.S. Also good point about similarity to algebraic classes, though I think algebraic classes have advantage of behaving pretty much the same as usual Haskell, and BooleanOf a is not usual Haskell

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready for review needs review before merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Refactor EllipticCurve to make it Symbolic-friendly
3 participants