# Resources as purely functional objects

**URL:** <https://forum.anoma.net/t/resources-as-purely-functional-objects/1455>\
**Category:** RM\
**Created:** [April 27, 2025, 2:23am UTC](https://forum.anoma.net/t/resources-as-purely-functional-objects/1455 "2025-04-27T02:23:29Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![jonathan](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/jonathan/32/1395_2.png) [@jonathan](https://forum.anoma.net/u/jonathan)\
**Post date:** [April 27, 2025, 2:23am UTC](https://forum.anoma.net/t/resources-as-purely-functional-objects/1455/1 "2025-04-27T02:23:29Z")

</div>

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

> [@Looking at the OO Resource Machine Experiment](https://forum.anoma.net/t/looking-at-the-oo-resource-machine-experiment/1384):
>
> Table of Contents [Preliminary Results from the first OO-RM](#org727d1ad)[Preamble](#org1ba680b)[Goals Non Goals and Motivation](#org5fb6859)[The Programming Model](#org9da2259)[Base Level Mapping](#org964369c)[Protocols](#org9a9c466)[Object↔Resource Transformation](#org64c3f11)[The Three Predicates and It’s Precursor](#org438fd8d)[Delete/Consumption and Introduction](#orgad36065)[Meta Environment Protocols](#org743773c)[Verification](#org5919127)[Transact](#orgfe3b840)[How does it work in practice](#orge8faaee)[Ownership](#org1b380e9)[Unique](#orgd3ee0c8)[Fixed-Supply](#orgf963400)[Spacebucks](#org868a4b5)[Imagining a Logtalk Implementation](#orgfca1148)[Intent Transactions](#org263ccd1)[Vulnerability](#orgdc086bd)[The Meta Language Requirements](#org9ed2f67)Conclusion …

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](https://specs.anoma.net/pr-359/arch/system/state/resource_machine/data_structures/resource/index.html)

> 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 of `valueRef` - 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:

```ml
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](https://specs.anoma.net/pr-359/arch/system/state/resource_machine/data_structures/resource/index.html),  
we can define the representation of the state of a resource as:

```ml
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.

```ml
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

```ml
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,

```ml
ResourceR := {
  ...
  , #accessCount: Nat
};

```

and the methods could be:

```ml
ResourceM := λ (R : *) . {
  ...
  , accessCount : R → Nat
};

```

## Resource as a functional object

We can now formally define a resource:

```ml
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:

1. Takes a subtype `R` of the resource state representation
2. Takes a self-reference function that allows access to the object’s methods
3. Returns a function that, when given a unit value, produces a record of  
methods that operate on resources of type `R`

This structure enables proper method dispatch and self-reference while  
maintaining type safety.

```ml
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.

```ml
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:

```ml
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.

```ml
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`.

```ml
> getCommitment [ResourceM] r : Commitment

```

Okay, another example of defining a function.

```ml
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](https://www.cis.upenn.edu/~bcpierce/tapl/index.html).

Another encoding of the RM is possible using row-value polymorphism. Something  
like,

```ml
Resource := {
  ...
  , p
};

where `p` is a row variable that can be instantiated to a polymorphic type.
```

---

<div class="post-metadata">

**Author:** ![cwgoes](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/cwgoes/32/22_2.png) [@cwgoes](https://forum.anoma.net/u/cwgoes)\
**Post date:** [April 29, 2025, 8:13am UTC](https://forum.anoma.net/t/resources-as-purely-functional-objects/1455/2 "2025-04-29T08:13:10Z")

</div>

Thanks for the write-up. I’ll leave some thoughts on the question of the relationship between the resource-abstraction and the object-abstraction for later, but for now I just wanted to note one complexity that I think we’d need to think about in this kind of effort: for different resource objects with potentially different method implementations to be used _together_ in the context of a single “resource machine” in a way which preserves the desired high-level properties, their method implementations must stand in certain relationships to each other, both at a per-resource level and across resources – for example, delta should bind to kind and quantity (per-resource), and commitments and nullifiers of unequal resources should always be unequal (across-resources).

If we allow arbitrary implementations of these methods, the system can be trivially broken: for example, I could create a new resource which intentionally has the same nullifier as a previously created one, and nullify this new resource to prevent the previously created one from being spent. I’m not sure exactly what this would require in terms of type-systems or descriptions to capture precisely, but I think that we’ll need to address this challenge if we want to really capture the resource machine in an OO model.