plutonomicon/plutarch-core

Plutarch 2.0

P L U T O N O M I C O N

Introduction

The Plutonomicon is a developer-driven guide to the Plutus smart contract language in practice.

Since this ecosystem is moving at a breakneck speed, we ask that ANY information posted that is not confirmed to work on chain be labelled as 🔧 work in progress.

Available resources

We currently provide the following resources, broadly organized by topic.

Fundamentals and explanations

• The Fundamentals of Plutus, which gives a brief introduction to the Plutus language.
• Plutus from a Transaction Perspective, which gives another perspective to the environment Plutus runs in.
• Plutus Numeric Hierarchy, which gives an overview of the Plutus numerical type class stack, as well as the extensions to it provided by plutus-numeric.
• User guide to plutus-numeric, which gives a more 'example-driven' explanation for how to do certain common tasks using plutus-numeric.
• How Stake Validators Actually Work, which gives an explanation of 'Stake Validators'.

Design patterns

• Forward Minting Policy. Also described in another writeup. Some caution is required, as you may not wish to directly reference a script to obtain a hash used to identify the two scripts, as this method details.
• Come and Go Proof Tokens
• State Thread Token Pattern
• DistributedMap, describing an on-chain implementation of key-value mappings. This is naive, and mostly designed for conceptual illustration.
• Consistency of a Distributed Map, which explains some ways of operating on a distributed map.
• Stick Breaking Set, describing an on-chain method of proving presence or absence in a set.
• On-Chain Association List With Constant Time Insert-Removal, describing a pattern that can be used to replicate account-style maps without breaking transaction size limits. This is the optimized version of the naive version of that data structure.
• Transaction Tokens provide an method of deferring validation to minting policies for the purpose of validating entire transactions rather than the unlocking of individual UTxOs.
  • The Transaction Token Pattern document introduces the pattern.
  • The Transaction Token Protocol Architecture document introduces a conceptual and practical framework leveraging the pattern for specifying and implementing protocols.
  • The Protocol Category Sketch document sketches a formalism to establish a formalism that places protocols described according the the Architecture into the language of symmetric monoidal categories, and works through some examples of how wiring diagrams and aid specification and implementation.

Testing and optimization

• Staying In Bounds, which describes the testing interface for Plutus on-chain size provided by plutus-size-check.

Script Optimization Techniques:

• Reducing Plutus Script Sizes
• Optimizations to reduce CPU and Mem consumption
• Shrinker (shrinker is currently unmaintained)

Plutus Vulnerabilities:

• Common Plutus Vulnerabilities

Discussion

To discuss the projects and the content under the Plutonomicon umbrella, join our Discord: https://discord.gg/722KnTC8jF

Running the website

If you'd like to run a live version of the website locally:

nix run

As you edit¹ and save the Markdown files, the browser view should update instantly without requiring a manual refresh. Run nix build to build the statically generated website. See Emanote guide for further information.

Please note the Markdown writing conventions:

• There must be zero or one level 1 heading (# A heading) as the first line.
  • If a level 1 heading is not specified, title will be derived from the filename.
• All other headings must be level 2 or greater.

Footnotes

1. Try Obsidian or VSCode with vscode-memo for editing. ↩

plutarch-core's Issues

Add type family `T`

type family T :: forall (edsl :: EDSLKind).  EType -> Type
type family T a where
  T @edsl a = Term edsl a

This is useful for annotating types inside terms

Implement effects in Nix backend

The Compile type needs to be changed to take an effect that returns a term.
The concrete implementation would likely be something similar to (M (m NixAST), a).
Sequencing two effects would essentially seq the contained terms.
TermCont and PEffect should be renamed and should be different instantiations of another type, e.g. PE purity a. Then plet etc. can abstract over that, same for pmatch/pcase.

GHC improvements

Definite improvement:
[ ] https://gitlab.haskell.org/ghc/ghc/-/issues/21702 (useful for deriving)
[ ] Warnings for OVERLAPPING and OVERLAPS.
[ ] Warnings for incoherent usage of OVERLAPPABLE instances.
[ ] Warnings for orphan flexible instances.
[ ] https://gitlab.haskell.org/ghc/ghc/-/issues/21782
[ ] Quantified constraints that work with type families
[ ] Generalised singletons (no proposal written-up)
[ ] Expand metavar x :: a when kind allows only one constructor, needed to replace ConstructNPFromVars stuff that also really fucks up compile-time performance
[x] Monadic viewpatterns replaced by https://github.com/JakobBruenker/monadic-bang
[ ] More powerful generics

Prefix everything with `p` again, instead of `e`

An informal internal poll at MLabs was performed.

Fix type inference on `compile`

https://gitlab.haskell.org/ghc/ghc/-/issues/22224

Relevant paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf

`DataKinds`-like theory in eDSL

This is probably not easy.

data EBool ef = EFalse | ETrue
  deriving stock Generic
  deriving anyclass EIsNewtype

-- takes `edsl` twice..
data ESBool (b :: Term edsl EBool) ef
  = ESFalse (Eq @? b (econ? EFalse))
  | ESTrue (Eq @? b (econ? ETrue))

Encode co{,ntra}variance and su{b,per}typing

To allow zero-cost coercions

Optics

Syntactical plugin to improve ergonomics

\x -> y -> maybePLam \x -> y
A x y z -> maybePCon $ A x y z
case x of { ... } -> maybePMatch x \case { ... }
Similarly for pattern guards, and other built-in syntax that can't be overloaded.

# Class-based solution
class MaybePLam x y out | out -> x y where
  maybePLam :: (x -> y) -> out

instance PLC e => MaybePLam (Term e a) (Term e b) (Term e (a #-> b)) where
  maybePLam = plam
  
instance {-# OVERLAPPABLE #-} PLC e => MaybePLam a b (a -> b) where
  maybePLam = id
  
# Type-family-based solution
type family F1 (x :: Type) :: Type where
  F1 (Term e (a #-> b)) = Term e a
  F1 (a -> b) = a

type family F2 (x :: Type) :: Type where
  F2 (Term e (a #-> b)) = Term e b
  F2 (a -> b) = b

type family IsTermFunc (x :: Type) :: Bool where
  F2 (Term e (_ #-> _)) = 'True
  F2 (a -> b) = 'False

maybePLam :: KnownBool (IsTermFunc out) => (F1 out -> F2 out) -> out
maybePLam = ...

General repo setup

CI, formatting, etc.

GHC Core backend

We want a backend that outputs GHC Core or something equivalent to it.

Outputting Haskell directly is another alternative but harder.

Allow splitting languages

Figure out how to make foralls more ergonomic

Clean up implementation of Plutarch.Internal.Utilities

The proofs can in hindsight be made much more elegant.
Performance also needs to be considered, everything that can be represented as an integer
should be an integer.
Many GADTs should be made into fully erased data families too.

Clean up implementation such that unused proofs terms are not carried around

Certain types are morally in Prop. We can rewrite the code such that they don't exist at run-time.

Embedded classes/constraints

Needs 9.4 to make it work well, but pre-9.4 can be made to work with plugin

Subinterpreting example

Make example for how to make something like the following:

f :: (EA edsl, EA edsl', EB edsl', IsEType edsl a, IsEType edsl b) => Term edsl a -> Term edsl' a

The idea is that we can implement EB in terms of EA. This might require changes to the core.

This is also important for emulating effects.

Equality type

This is useful for embedding GADTs

Example/Simple.hs doesn't compile

I first had to remove -Werror from plutarch-core.cabal in order to get past this unrelated error:

$ cabal repl
[...]
*** Exception: The following packages were specified via -package or -package-id flags,
but were not needed for compilation:
  - generics-sop-0.5.1.2-06250a69f3fc2d522ae418e9289393f2a0f8235347abce6b0b8887d14a0234a9
  - data-fix-0.3.2-b9f47d59a8d3a40a6cab9330e980f581afb5026ee9bb16169dc8c0f5e15586f4
  - base-4.16.0.0

Then I got an unbound identifier when loading the example:

$ cabal repl
λ> :load Examples/Simple.hs 
[...]
Examples/Simple.hs:17:80: error:
    Not in scope: type constructor or class ‘UnEf’
   |
17 | newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (UnEf ef)) f))
   |                                                                                ^^^^

Looking at the history, looks like the UnEf type family was renamed to EfC in 8975df7.

After performing the rename, I get a kind error instead:

Examples/Simple.hs:17:80: error:
    • Couldn't match kind ‘ETypeF -> Type’ with ‘ETypeRepr’
      Expected kind ‘EDSLKind’,
        but ‘EfC ef’ has kind ‘EType -> Constraint’
    • In the first argument of ‘IsEType’, namely ‘(EfC ef)’
      In the first argument of ‘EForall’, namely ‘(IsEType (EfC ef))’
      In the second argument of ‘Ef’, namely
        ‘(EForall (IsEType (EfC ef)) f)’
   |
17 | newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (EfC ef)) f))
   |                                                                                ^^^^^^

Looking at the kinds involved, I can fix the kind error by replacing IsEType (EfC ef) with EfC ef, but I don't yet have any idea if that makes any sense semantically.

With that "fix", I next encounter a type error:

Examples/Simple.hs:38:10: error:
    • Couldn't match type: EUnit f0
                     with: Term edsl EUnit
      Expected: Ef (Plutarch.Core.Helper edsl) U0
        Actual: EUnit f0
    • In the pattern: EUnit
      In the pattern: ERight EUnit
      In a case alternative: ERight EUnit -> econ EUnit
    • Relevant bindings include
        x :: Term edsl U1 (bound at Examples/Simple.hs:37:3)
        f :: Term edsl U1 -> Term edsl U0
          (bound at Examples/Simple.hs:37:1)
   |
38 |   ERight EUnit -> econ EUnit

That is, ERight's parameter is already a Term edsl EUnit, which is what we need on the right-hand-side, so the code can be simplified to:

f x = ematch x \case
  ERight eUnit -> eUnit
  ELeft eUnit -> eUnit 

With this second fix, Example/Simple.hs finally typechecks! However, the simplified code is not quite equivalent to the previous code, because we are no longer pattern-matching on EUnit. I get the impression that when the example was written, it was possible to write nested patterns with ematch, but that since then, ematch has been simplified so that only the outermost constructor is concretized. Thus, if we also want to match on the EUnit inside the ERight, we need a second ematch call:

f x = ematch x \case
  ERight eUnit -> ematch eUnit \case
    EUnit -> econ EUnit
  ELeft eUnit -> ematch eUnit \case
    EUnit -> econ EUnit

Some kind of dependently typed backend

This will be a good exercise in showing how to embed more powerful type theories.

Allow attaching metadata to datatype definitions

Haskell already allows us to attach a small amount of metadata in the form of strictness-annotations and similar, however, it seems useful to distinguish between Haskell metadata and embedded metadata. The Haskell constructor taking a lazy argument doesn't necessarily mean the embedded constructor should, or vice versa.

There are two main ideas, the first one is adding a fake constructor with metadata:

newtype PMetadata metadata = PMetadata Void#

data PMyType ef = PMyType (ef /$ PInteger) (ef /$ PInteger)
  | PMyTypeMeta (PMetadata '[PScottEncoded])
  deriving stock (Generic)
  deriving anyclass (PHasRepr)

This essentially means the constructor doesn't exist, since you don't have to worry about it when matching,
and you can't construct it either.

The other trick is attaching metadata to individual fields like so:

data PMyType ef = PMyType (ef /$ PInteger) (PStrictField ef /$ PInteger)
  deriving stock (Generic)
  deriving anyclass (PHasRepr)

This doesn't affect PHs, nor how users interact with the type, but it allows backends to see that it should be strict.

Type class and backend for Lua

Making a type class that expresses Lua's syntax and semantics will require novel techniques.
Since the language is mutable, and statements can't be put into expressions, the type class has to represent that, in addition to typing mutability somehow. This will look like an effect system, but be a bit different.
https://richarde.dev/papers/2021/linear-constraints/linear-constraints.pdf is a good resource for some ideas.

Optimisations to do

• Case of known constructors
  • Let-bind if term is used more than once
  • Otherwise inline
• η-reduction (for all types)
• Merging matches on same thing (choose the top-most one)
• User-defined rewrite rules (not through RULES pragma) (hard)
• Common Expression Elimination (not subexpression elimination) / hoisting
• Detect partial updating with pcon and pmatch/pcase

Support _generating_ type class instances

This is much harder than it sounds.
Given a target language that supports type classes, we want to be able to make use of that feature.
This is useful if you're interacting with libraries in that ecosystem that use type classes.
This will be of heavy importance in a future PureScript or Rust backend.

Support embedded linearity

Important for doing safe memory operations

How does interpreting and linearity of languages interact?

Especially important in the context of #42 .

Singletons / Dependent types

Using singleton trick described before, needs GHC plugin