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

Support Plutarch #107

Closed bladyjoker closed 10 months ago

bladyjoker commented 11 months ago

TODO:

bladyjoker commented 10 months ago

This is going to be a tricky one!

Will write down some of my thoughts.

Given a Foo .lbf module:

module Foo

import Plutus

sum FooSum a b = Bar a (Maybe Address) | Baz b (Maybe AssetClass)
derive Eq (FooSum a b)
derive Json (FooSum a b)
derive PlutusData (FooSum a b)

prod FooProd a b = a (Maybe Address) b (Maybe AssetClass)
derive Eq (FooProd a b)
derive Json (FooProd a b)
derive PlutusData (FooProd a b)

prod FooRec a b = {
  bar : a (Maybe Address),
  baz: b (Maybe AssetClass)
  }
derive Eq (FooRec a b)
derive Json (FooRec a b)
derive PlutusData (FooRec a b)

How do we map type definitions and implementations.

Type definition mapping

module LambdaBuffers.Plutarch.Foo where

data FooSum (a :: PType) (b :: PType) (s :: S) = FooSum'Bar (Term s a) (Term s (PMaybe PAddress))
   | FooSum'Baz (Term s b) (Term s (PMaybe PAssetClass))

data FooProd (a :: PType) (b :: PType) (s :: S) = FooProd (Term s a) (Term s (PMaybe PAddress)) (Term s b) (Term s (PMaybe PAssetClass))

data FooRec (a :: PType) (b :: PType) (s :: S) = FooRec {
   bar :: (Term s a) (Term s (PMaybe PAddress)),
   baz :: (Term s b) (Term s (PMaybe PAssetClass))
   }

Questions:

  1. Do we need to use PDataRecord or is native product good enough?
  2. bar and baz field accessors, I guess they are useless, and I must implement some of the Field tcs?

Implementation deriving

module LambdaBuffers.Plutarch.Foo where

instance Plutarch.PlutusType FooSum a b where
   pcon = ...
   pmatch = ...

instance Plutarch.PlutusType FooProd a b where
   pcon = ...
   pmatch = ...

instance Plutarch.PlutusType FooRec a b where
   pcon = ...
   pmatch = ...

instance Plutarch.Eq FooSum a b where
  (#==) = plam (\l r -> )

instance Plutarch.Eq FooProd a b where
  (#==) = plam (\l r -> )

instance Plutarch.Eq FooRec a b where
  (#==) = plam (\l r -> )

Questions

  1. Is PlutusType central to this whole story?
  2. What should type vars be constrained on in PlutusType instances (PIsData? Or PlutusType?)?
  3. Equality in Plutarch is generally delegated to their Data encoding, which I believe implicitly assumes that values of PTypes have a single valid Data representation.
    • Is that generally true? What happens to hypothetical PSet such that [x,y] and [y,x] Data representations could be considered valid. I think it needs to be stressed out that PTypes have a canonical and unique value representations.
bladyjoker commented 10 months ago

I need a bit more clairification on PlutusType and PIsData relationship...

I'm implementing my pcon' for my type, and I have to call pdata on its constituents? This is suprising to me:

  1. Why not further call pcon' on constituent types?

    • Because! These are already pcond values, ie. constructed values, and now you need access to their Data form (fundamentally it's already in this form, we just have to massage the types with pdata)
  2. Is default PIsData implementation doing the above in some way?

    • I think so? It just does a pto which gives you the PData of your PType (that's what PInner is for).
  3. Why would PIsData implementations, pfromDataImpl and pdataImpl, ever be anything but 'take the underlying PData and pass that along'

    • Not sure about that? Anyone?
  4. I might be forgetting that we have ScottEncoded variants on everything so perhaps that is why?

  5. What's the deal with PTryFrom?

    • Eventually, I need to get from PData into my Term s Smtn, is PTryFrom also doing pmatch in the background (as the default impl)?
  6. PEq is interesting

    • Because values of PTypes are PData, equality is deferred to PData equality. Is this fundamentally solid? As in; is there 2 different PData representation of the same 'value' that would break this assumption? Can't think of anything.