mlabs-haskell / lambda-buffers

LambdaBuffers toolkit for sharing types and their semantics between different languages
https://mlabs-haskell.github.io/lambda-buffers/
Apache License 2.0
29 stars 0 forks source link

Discuss: PlutusTx Eq instance generation should delegate to BuiltinData equality #236

Open bladyjoker opened 6 days ago

bladyjoker commented 6 days ago

In Plutarch the general consensus is that we perform Eq by simply delegating to the underling PlutusData representation.

instance PEq FooTrivial where
  (#==) = \l r -> pdata l #== pdata r

PlutusData equality operation is a builtin which is naturally much more performant then doing the obvious field by field comparisons (which is done in PlutusTx PLA types and is generally a practice adopted https://github.com/IntersectMBO/plutus/blob/b34d6ca2c4bbe54c324337eb813a5f6a522b475c/plutus-ledger-api/src/PlutusLedgerApi/V2/Tx.hs#L84).

However, we do assume that there's a single canonical PlutusData representation for all types, which might not be the case for semantically richer types like Set or Map (for example, the underlying AssocMap PlutusData representation can use ascending or descending ordering etc). This is solved by agreeing on a well defined PlutusData representation for any type that might be ambiguous in that regard.

cc @peter-mlabs

bladyjoker commented 6 days ago

PTryFrom in Plutarch is parsing data and yielding a type (it just yields a proof that it is of proper encoding). So it's about going from PlutusData -> a (which can fail).

However, what's the deal with PlutusTx ToData/toData? In Plutarch this is a pdata noop that just forgets the type, but in PlutusTx this is not a noop and it actually traverses the value structures while converting to BuiltinData

I ask because if I wanted to implement PlutusTx.Eq such that it delegates to underlying BuiltinData equality check I'm not sure how I would do a pdata PlutusTx equivalent on it. And ToData instances seems to be going through each constituents and calling toData which is not efficient and sounds redundant (unless I'm missing smtn)

To be more concrete if I

instance PlutusTx.Eq Foo where
  l == r = toData l == toData r

I wouldn't necessarily gain anything, as I still traverse the value structures of l and r and construct BuiltinData from it. Right?

bladyjoker commented 6 days ago

Relevant Plutarch pieces

PEq (PAsData a) -> https://github.com/Plutonomicon/plutarch-plutus/blob/780d350f1985e89e3294861118f721d4141b2a6a/Plutarch/Builtin.hs#L471

pdata :: PIsData a => Term s a -> Term s (PAsData a) https://github.com/Plutonomicon/plutarch-plutus/blob/780d350f1985e89e3294861118f721d4141b2a6a/Plutarch/Builtin.hs#L367

punsafeBuiltin https://github.com/Plutonomicon/plutarch-plutus/blob/780d350f1985e89e3294861118f721d4141b2a6a/Plutarch/Internal.hs#L369