This week, among other things, I should have jumped into the ongoing
formalisation of the current presentation of the RM in Lean4 by @graphomath and @ArtemG,
that is, using dependent types. However, I decided to detour a bit and explore
encoding the concept of resources, just resources!, as a concept akin to
object-oriented programming (OOP). Let me share this experiment below. It’s
worth mentioning that this is also inspired by internal discussions and forum
posts
by @mariari, because it may be simpler than the post described. Also, if you
find any typos and issues in the code snippet below, feel free to reach out to
me, and I’ll fix them. I also wrapped the text with a max of 80 for me, my
editor did it, hope it’s not disturbing.
While OOP combines data and behaviour in mutable objects, and you change their
behaviour and state by “sending messages”, functional programming requires a
different approach due to immutability. The literature on the subject is quite
rich, so it’s not trivial. I will focus on how to represent resources as purely
functional objects via existential types, and other features such as subtyping
under the hood.
Motivation
In the Anoma specs, we have the following paragraph at the end of the definition
of a resource, and I wanted to rephrase it so it’s precise. Hopefully, after
this post, I might be able to.
- Latest work on this definition:
PR-359
REF1 To distinguish between the resource data structure consisting of the
resource components and a resource as a unit of state identified by just one
(or some) of the resource computed fields, we sometimes refer to the former as
a resource object. Data which is referenced by the resource object such as the
preimage ofvalueRef- we refer to as resource-linked data
As I see it, the Anoma resource system specs as they stand involve three
distinct concepts:
- Resource object, the complete data structure with all resource-defining
fields - Resource identifiers, computed fields derived from the resource object that
uniquely identify resources - Resource-linked data, external data referenced by the resource object (like
preimages of hashes), This, I’m going to ignore in this note.
Functional object representation
In functional programming with a type system that has features such as
subtyping, higher-order operators, and other advanced capabilities, we can
define the type of objects as follows:
Object := λ (M : * → *) .
{ ∃X
, { state : X
, methods : M X
}
};
> Object : ((* → *) → *)
That is, Object is a type operator that takes a type constructor M (for
methods) and returns an existential type, where the type variable X is bound
and hidden, and where the body of the type is a record with the state of
type X and the methods of type M X. Here, X represents the
representation of the object’s state, while M X represents the object’s
methods. The type X is hidden from external view. I won’t delve deeply into
existential types here, but you can think of them as a way to bind a type
variable to a type and hide it from the outside. This concept differs from sigma
types but is related to n-type truncation in Homotopy Type Theory (HoTT).
The key insight about using existential types is that an object essentially
functions as a black box. We don’t know its internal representation, but we can
interact with it solely through its methods.
For the resource type, we need to declare both the representation of the state
and its methods. Importantly, declaring the methods (the interface type) does
not depend on the specific representation of the state.
The representation of the state of a resource
From ARM specs
PR-359,
we can define the representation of the state of a resource as:
ResourceR := {
logicRef: LogicVKCompact,
labelRef: LabelHash,
valueRef: ValueHash,
quantity: Quantity,
isEphemeral: Bool,
nonce: Nonce,
nullifierKeyCommitment: NullifierKeyCommitment,
randSeed: RandSeed,
#consumed: Bool
};
The # prefix denotes fields that can be updated. You can skip this detail in a
first reading, but this is the same notation used by Pierce when supporting
polymorphic record updates. Only fields marked as updatable are allowed to be
modified, and this constraint is enforced at compile time.
The methods of a resource
The interface type ResourceM defines the available methods for a resource.
ResourceM := λ (R : *) . {
commitment : R → Commitment,
nullifier : R → NullifierKey → NullifierHash,
kind : R → KindHash,
quantity : R → Quantity,
delta : R → Option DeltaExtraInput → DeltaHash,
isConsumed : R → Bool,
tag : R → Bool → Tag,
};
where Tag is
Tag := Commitment | Nullifier
and the rest of types such as Commitment, Nullifier, NullifierKey,
NullifierHash, KindHash, Quantity, DeltaExtraInput, and DeltaHash are
taken as given.
Above, ResourceM is a type operator that takes any type R and returns a record of methods operating on that type. Of course, we expect that the type R is the representation of the
state of the resource, or a subtype of it, which we’ll denote as A <: B when
A is a subtype of B. However, we don’t need to make this explicit.
For example, from the type signature of isConsumed, we can see that it takes a
value of type R as input and returns a boolean. If R were a resource, it
would return the consumed field of the resource.
An important point is that the presentation here assumes a type system that
supports subtyping and polymorphic record updates. This is quite a strong
assumption and powerful features. With it, we could define different, more
specialised interface types for “subclasses” of resources. For instance, we
might create a class with a representation that extends the base resource to
count the number of times a resource is accessed for validation purposes. We
would then define a subclass of resources and a subclass of resource methods
with an instance variable that counts access frequency, and propagate this logic
to all methods that need to know the access count. For example,
ResourceR := {
...
, #accessCount: Nat
};
and the methods could be:
ResourceM := λ (R : *) . {
...
, accessCount : R → Nat
};
Resource as a functional object
We can now formally define a resource:
Resource := Object ResourceM;
This definition means that a resource is an object whose methods conform to the
ResourceM interface. We structure it this way to separate cleanly:
- The varying part: the method interface (
ResourceM), which supports
subtyping. - The fixed skeleton: the existential packaging of state and methods, which
remains stable and simplifies repackaging.
Resource class implementation
Now we can implement the resource class. A class is a type operator that:
- Takes a subtype
Rof the resource state representation - Takes a self-reference function that allows access to the object’s methods
- Returns a function that, when given a unit value, produces a record of
methods that operate on resources of typeR
This structure enables proper method dispatch and self-reference while
maintaining type safety.
resourceClass :=
λ (R <: ResourceR) .
λ (self : Unit → ResourceM R) .
λ (_ : Unit) .
{ commitment = λ (r : R) . commitmentHash(r)
, nullifier = λ (r : R) . λ (nk : NullifierKey) . nullifierHash(nk, r)
, kind = λ (r : R) . kindHash(r.labelRef, r.logicRef)
, quantity = λ (r : R) . r.quantity
, delta = λ (r : R) . λ (ei : Option DeltaExtraInput) .
let knd := (self unit).kind r in
let qty := (self unit).quantity r in
deltaHash(knd, qty, ei)
, isConsumed = λ (r : R) . r.consumed,
, tag = λ (r : R) . λ (isConsumed : Bool) .
if isConsumed then (
let nk := r.nullifierKeyCommitment in
(self unit).nullifier r nk
)
else (self unit).commitment r
}
as ResourceM R;
And one could actually define “sub-classes” of resources. For example, a “sub”
class of resources that are ephemeral. Instead of baking in the isEphemeral
field in the representation of the state.
Resource creation
To be useful, a resource of type Resource must inhabit the existential type
Object ResourceM. This means it needs to be an object that implements methods
conforming to the ResourceM interface. So, we can define the function
createResource that takes the resource components and returns a resource object.
createResource := λ (cmpts : ResourceR) .
{* ResourceR,
{ state := {
logicRef := cmpts.logicRef,
labelRef := cmpts.labelRef,
valueRef := cmpts.valueRef,
quantity := cmpts.quantity,
isEphemeral := cmpts.isEphemeral,
nonce := generateNonce(),
nullifierKeyCommitment := cmpts.nullifierKeyCommitment,
randSeed := cmpts.randSeed,
consumed := false
},
methods := fix (resourceClass [ResourceR]) unit
}
}
as Resource;
Notation: {* R, B } is the notation for the term of the existential type ∃R. X, where R is the type variable and B is the body of the existential type
of type X. The fix operator creates the recursive binding for
self-reference. Think of it as a way to enable recursion in the type system.
Then, a resource could be “created” as:
r := createResource {
logicRef = ...
labelRef = ...
valueRef = ...
quantity = ...
isEphemeral = ...
}
> r : Resource
Resource operations
One example of a function that may be useful in this context is how to get the
commitment of a resource object. Here is how.
getCommitment := λ (M <: ResourceM) . λ (r : Object M) .
let {_, b} := r in
b.methods.commitment(b.state);
> getCommitment : ∀ (M <: ResourceM) . Object M → Commitment
Let’s read this in a more verbose way. getCommitment takes a subtype M of
the type of resource methods, and an object with that interface, which is a
resource. It then returns the resource’s commitments. We unpack the object
and, using the body (which is a record), we call the function commitment to
get the commitment of the resource by passing in the resource’s state. Remember
that this state has the type that represents the state of the resource,
ResourceR.
> getCommitment [ResourceM] r : Commitment
Okay, another example of defining a function.
getQuantity := λ (M <: ResourceM) . λ (r : Object M) .
let {_, b} = r in
b.methods.quantity(b.state);
At this point, it should be clear that we have defined interface types for our
objects. To use “getters” and “setters” on these objects, we need to define
functions that take the interface type as a type parameter and an object of that
type as an argument, then return the value of the desired field or compute.
Conclusion
Whether you adopt OOP directly or not, OOP core ideas can be encoded in a purely
functional style —and the RM stands to benefit. This note only scratches the
surface of representing RM concepts as functional objects. I missed many other
concepts, like inheritance in the OOP topic but for the RM, resources linked
data, and more central concepts, like the resource machine itself, and the
concept of transactions, and more. I, personally, see this encoding compelling
for a model of the RM that is both simple and powerful, and that can be
understood by both OOP-like people and functional programmers.
BTW, under the hood we rely on a variant of Pierce’s System F<:^ω, existential
types and polymorphic record updates. We must have parametric polymorphism,
bounded quantification, higher-order type operators, subtyping, existential
types, record types, of course, and polymorphic record updates. Not to mention
fix for recursive types. You can probably get similar power in Haskell (with
the right extensions) or OCaml. The main reference for this note is Pierce’s
chapter 32, on Purely Functional
Objects.
Another encoding of the RM is possible using row-value polymorphism. Something
like,
Resource := {
...
, p
};
where `p` is a row variable that can be instantiated to a polymorphic type.