A Toy Model/Specification for Superfluid Money Concepts

- A
**new payment paradigm**:- where money can be
**instantly**or**continuously**moved from**1-to-1**or**1-to-N en-mass**.

- where money can be
- How a
**Haskell toy model/reference implementation/specification**for it is written:*Haskell*- A pure, strongly-typed, syntactically terse language best suited for domain modeling.- "A domain model is a conceptual model of the domain that incorporates both behavior and data."
- Also similar to what Conal Elliot advocated for: a denotational design of software.

- A teaser of new perspectives on money,
- Let's search for some categories related to money.
- Real time finance, a new area for innovations.

Bob requests to send €42 to Alice *now*.

Bob requests to send a constant flow of money at €420 per 30 day to Alice *now*.

Microsoft requests to send $0.42 per share to all its share holders *on the next ex-dividend date*.

Elon Musk requests to send a constant flow of money at €4.2B per 360 days to all its share holders with individual flow
rates proportional to their number of share units, *from 20st April*.

- Financial Market Utilities (FMUs): SEPA, TARGET2, Fedwire, CHIPS, SWIFT, etc.
^{1} - Public Blockchains and their token standards: Bitcoin, Ethereum, Ethereum ERC-20 tokens, etc.

FMUs | Public blockchain | |
---|---|---|

Instant | Yes, fast within the system, poor interoperability | Yes, with scalability issue |

Streaming | Micro transactions | Micro transactions, but can be costly on some system |

en mass | NOPE | Some system may have ad-hoc implementations. |

**FORMAL SPECIFICATION**- A foundation designed using denotational semantics approach. (Conal Elliott/Lambda Jam 2015)
- Built with compositionality in mind. (Simon Peyton Jones/Microsoft research, "Composing contracts")

**EFFICIENT**- A system that interprets the DSL and performs the operations with as little as possible information waste.
- Use micro payments to simulate flow of money?
**NOPE** - Send dividens payment one by one to all share holders?
**NOPE** - They are all too noisy.

- Use micro payments to simulate flow of money?

- A system that interprets the DSL and performs the operations with as little as possible information waste.

- Design an
**denotational semantics**for new payment requests. - An
**expressive and composable DSL**for the semantics. - A
**new payment rail**that natively interprets and execute the DSL.

How money is represented in the system?

```
class (Integral v, Default v) => Value v
```

- But there are no further "types" of value.
- Let us call these values
*unaccounted for*.

- We give value a tag, so that it can be
*accounted for*by sub systems. - We will see what are sub systems later…

```
-- | Typed value is an otherwise unaccounted value ~v~ with an associated ~vtag~.
class ( TypedValueTag vtag
, Value v
) => TypedValue tv vtag v | tv -> v, tv -> vtag where
untypeValue :: tv -> v
default untypeValue :: Coercible tv v => tv -> v
untypeValue = coerce
-- | Tag for typed value type class using ~Typeable~ runtime information.
class Typeable vtag => TypedValueTag vtag where
tappedValueTag :: Proxy vtag -> String
```

- There are two sub classes of typed values:
*Untapped typed value*doesn't have a designated sub system. Hence any sub system can add or remove amount of this type.- Any
*tapped typed value*on the other hand is designed to a specific sub system. Hence only that sub system can add or remove amount of this type. - An example is that, in your personal account, untapped typed value is what you can still use, while tapped typed value is what is reserved by the bank for a future transaction.

Code

`-- | Untapped value type. It can be freely accessed by any sub systems. newtype UntappedValue v = UntappedValue instance Value v => TypedValue (UntappedValue v) UntappedValueTag v -- | Tapped value tag. It must only be accessed by its designated sub system. class TypedValueTag tvtag => TappedValueTag tvtag instance (Value v, TypedValueTag vtag) => TypedValue (TappedValue vtag v) vtag v`

- Let's call a
*functorful*of these typed value`RealTimeBalance`

. - Or simply view it is a list of typed values
`[untapped value, tapped value 1, tapped value 2, ...]`

.

```
class ( Value v
, Foldable rtbF
, Monoid (rtbF v)
) => RealTimeBalance rtbF v | v -> rtbF where
-- | Convert a single monetary value to a RTB value.
valueToRTB :: v -> rtbF v
-- | Net monetary value of a RTB value.
netValueOfRTB :: rtbF v -> v
netValueOfRTB = foldr (+) def
-- | Convert typed values to a RTB value.
typedValuesToRTB :: UntappedValue v -> [AnyTappedValue v] -> rtbF v
-- | Get typed values from a RTB value.
typedValuesFromRTB :: rtbF v -> (UntappedValue v, [AnyTappedValue v])
```

```
-- monoid laws
monoid_right_identity x = (x <> mempty) `sameAs` x
monoid_left_identity x = (mempty <> x) `sameAs` x
monoid_associativity a b c = ((a <> b) <> c) `sameAs` (a <> (b <> c))
-- in addition to monoid laws, it also has some other nice properties:
monoid_mappend_commutativity a b =
(a <> b) `sameAs` (b <> a)
rtb_identity_from_and_to_typed_values x = -- type of x is a RealTimeBalance
(uncurry typedValuesToRTB . typedValuesFromRTB) x `sameAs` x
rtb_conservation_of_net_value x = -- type of x is a Value
(netValueOfRTB . valueToRTB) x == x
```

- U is the set of
*monetary units.* - ν : U → N is the
*value function.* - β : U → B is the
*bearer function.* - Monetary unit examples: coins, bank notes, bank account, crypto wallet, etc.

Cit. buldas2021unifying - A Unifying Theory of Electronic Money and Payment Systems

- ν needs an additional input ctx, known as the
*context*. - ctx should be some value that's "shared" globally in nature.
- For example, it could be
*timestamp*. - Further more, ν returns a RTB instead of the unaccounted value type.

How money should be moved in the system?

- Let us define another concept "agreement", to represent on-going relationships between monetary units.
- It has two parts:
- Agreement Monetary Unit Data.
- Agreement Operation.

- It provides part of the real time balance for the monetary unit.

```
class ( SuperfluidTypes sft
, Monoid amud -- !! A MONOID, so that system may scale
) => AgreementMonetaryUnitData amud sft | amud -> sft where
-- | π function -
-- balance provided (hear: π) by the agreement monetary unit data.
balanceProvidedByAgreement
:: amud -- amud
-> SFT_TS sft -- t !! THIS IS WHAT MAKES THINGS REAL TIME
-> SFT_RTB sft -- rtb
-- | Calculate the real time balance of an monetary unit at a given time.
balanceOfAt :: (SuperfluidTypes sft, MonetaryUnit mu sft)
=> mu -> SFT_TS sft -> SFT_RTB sft
balanceOfAt mu t = foldr -- !! THIS IS THE: ν(u, t)
-- !! providedBalanceByAnyAgreement is the balanceProvidedByAgreement for the existential type
-- returned from agreementsOf.
((<>) . (flip (providedBalanceByAnyAgreement mu) t))
mempty
(agreementsOf mu)
```

- They are the little engines that make values move.

```
class ( SuperfluidTypes sft
, AgreementMonetaryUnitData (AgreementMonetaryUnitDataInOperation ao) sft
) => AgreementOperation ao sft | ao -> sft where
-- ... for brevity, removed some type definitions here...
-- | ω function - apply agreement operation ~ao~ (hear: ω) onto the agreement
-- operation data ~aod~ to get a tuple of:
--
-- 1. An updated ~aod'~.
-- 2. A functorful delta of agreement monetary unit data ~aorΔ~, which then
-- can be monoid-appended to existing ~amud~. This is what can make an
-- agreement scalable.
applyAgreementOperation
:: amud ~ (AgreementMonetaryUnitDataInOperation ao)
=> ao -- ao
-> AgreementOperationData ao -- aod
-> SFT_TS sft -- t
-> ( AgreementOperationData ao
, AgreementOperationResultF ao amud) -- (aod', aorΔ)
```

Semantic: Party A sends an X amount of money instantly to party B.

- Built from lenses.
- TLDR: Lens' is a data structure of a pair of getter and setter.

```
class (Default amuLs, SuperfluidTypes sft)
=> MonetaryUnitLenses amuLs sft | amuLs -> sft where
untappedValue :: Lens' amuLs (UntappedValue (SFT_MVAL sft))
```

```
newtype Operation sft = Transfer (SFT_MVAL sft)
instance SuperfluidTypes sft => AgreementOperation (Operation sft) sft where
data AgreementOperationResultF (Operation sft) elem = OperationPartiesF
{ transferFrom :: elem
, transferTo :: elem
} deriving stock (Functor, Foldable, Traversable)
applyAgreementOperation (Transfer amount) acd _ = let
acd' = acd
aorΔ = fmap ITMUD.MkMonetaryUnitData (OperationPartiesF
(def & set ITMUD.untappedValue (coerce (- amount)))
(def & set ITMUD.untappedValue (coerce amount)))
in (acd', aorΔ)
```

- monoid

```
instance MonetaryUnitLenses amuLs sft
=> Semigroup (MonetaryUnitData amuLs sft) where
(<>) (MkMonetaryUnitData a) (MkMonetaryUnitData b) =
let c = a & over untappedValue (+ b^.untappedValue)
in MkMonetaryUnitData c
instance MonetaryUnitLenses amuLs sft
=> Monoid (MonetaryUnitData amuLs sft) where
mempty = MkMonetaryUnitData def
```

- π function

```
instance MonetaryUnitLenses amuLs sft
=> AgreementMonetaryUnitData (MonetaryUnitData amuLs sft) sft where
balanceProvidedByAgreement (MkMonetaryUnitData a) _ =
typedValuesToRTB (a^.untappedValue) []
```

`SF.transfer`

uses the`ITA.Operation`

defined above, this is how its semantic looks like:

```
runToken token $ SF.transfer (ITA.OperationPartiesF bob alice) (USD 42)
```

Well, we just redefined 1to1 instant payment using this new semantic… big deal, what's next?

Semantic: Party A sends a flow of money at a constant rate `X`

to party B.

- How can it work in a nut shell?
- A and B shares the same context "time", when time advances A & B's balances move at the same rate but opposite direction for both of them, for one single CFA agreement.
- Any party can have as many such CFA agreements on going as needed, its all in one single value: net flow rate for the party. Thanks to the monoid structure, it is very scalable.

```
class (Default amuLs, SuperfluidTypes sft)
=> MonetaryUnitLenses amuLs sft | amuLs -> sft where
settledAt :: Lens' amuLs (SFT_TS sft)
settledUntappedValue :: Lens' amuLs (UntappedValue (SFT_MVAL sft))
netFlowRate :: Lens' amuLs (SFT_MVAL sft)
instance MonetaryUnitLenses amuLs sft
=> Semigroup (MonetaryUnitData amuLs sft) where
(<>) (MkMonetaryUnitData a) (MkMonetaryUnitData b) =
let c = a & set settledAt ( b^.settledAt)
& over settledUntappedValue (+ b^.settledUntappedValue)
& over netFlowRate (+ b^.netFlowRate)
in MkMonetaryUnitData c
```

```
instance MonetaryUnitLenses amuLs sft
=> AgreementMonetaryUnitData (MonetaryUnitData amuLs sft) sft where
balanceProvidedByAgreement (MkMonetaryUnitData a) t = typedValuesToRTB
( UntappedValue $ uval_s + fr * fromIntegral (t - t_s) ) []
where t_s = a^.settledAt
UntappedValue uval_s = a^.settledUntappedValue
fr = a^.netFlowRate
```

```
-- ... some defintions are omitted for brevity ...
applyAgreementOperation (UpdateFlow newFlowRate) acd t' = let
acd' = ContractData { flow_last_updated_at = t'
, flow_rate = newFlowRate
}
aorΔ = OperationPartiesF
(def & set CFMUD.settledAt t'
& set CFMUD.netFlowRate (-flowRateΔ)
& set CFMUD.settledUntappedValue (UntappedValue $ -settledΔ)
)
(def & set CFMUD.settledAt t'
& set CFMUD.netFlowRate flowRateΔ
& set CFMUD.settledUntappedValue (UntappedValue settledΔ)
)
in (acd', fmap CFMUD.MkMonetaryUnitData aorΔ)
where t = flow_last_updated_at acd
fr = flow_rate acd
settledΔ = fr * fromIntegral (t' - t) -- !! KEY equition
flowRateΔ = newFlowRate - fr
```

Semantic: Party A sends a flow of money at a decaying rate `Λ`

to party B with a distribution limit of `X`

.

- For recipient looks like receiving money over a decaying curve (with a half-life determined by Λ):

```
balanceProvidedByAgreement (MkMonetaryUnitData a) t = typedValuesToRTB
( UntappedValue $ ceiling $ α * exp (-λ * t_Δ) + ε ) []
where t_s = a^.settledAt
α = a^.αVal
ε = a^.εVal
λ = a^.decayingFactor
t_Δ = fromIntegral (t - t_s)
```

- Similar to CFA it is scalable, but only for the same
`Λ`

value.

Challenge: How to augment previously mentioned semantics with 1 to N proportional distribution semantic?

- Lenses come to the rescue.
- Indexes are where the actual lenses are provided.
A reminder, lenses for the

`ConstantFlow`

:`class (Default amuLs, SuperfluidTypes sft) => MonetaryUnitLenses amuLs sft | amuLs -> sft where settledAt :: Lens' amuLs (SFT_TS sft) settledUntappedValue :: Lens' amuLs (UntappedValue (SFT_MVAL sft)) netFlowRate :: Lens' amuLs (SFT_MVAL sft)`

- For all (∀, universal) monetary unit data there exists one and only one set of universal lenses.
- As a result, combining
`ConstantFlow`

and universal indexed lenses gives you the 1to1 semantic agreements:- Instant Transfer Agreement (ITA)
- Constant Flow Agreement (CFA)
- Decaying Flow Agreement (DFA)
- etc.

```
data UniversalData sft = UniversalData -- UniversalMonetaryUnitData
{ -- ...
, cfa_settled_at :: SFT_TS sft
-- ...
-- | Monetary unit lenses for the universal index.
instance SuperfluidTypes sft => CFMUD.MonetaryUnitLenses (UniversalData sft) sft where
settledAt = $(field 'cfa_settled_at)
settledUntappedValue = $(field 'cfa_settled_untapped_value)
netFlowRate = $(field 'cfa_net_flow_rate)
```

- A publisher owns a distribution.
- Each distribution can have any number of subscribers.
- Each subscriber owns a number of units in the distribution.
- Subscribers can receive money distributions from the publisher proportionally per their number of units.

Constant Flow Distribution Agreement.

Sub systems created through "agreement framework" have:

*π function*- providing a portion of real time balance to the monetary unit data value function, with time also part of its input.*ω function*- transforming data or create agreement monetary unit data delta monoids that affect the inputs to the π function.*Lens abstraction*- A optional technique to compose smaller building blocks for`1to1`

and`1toN proportional distribution`

semantics.

- Instant Transfer Agreement (payment as we are familiar with)
- Constant Flow Agreement (1to1 constant money flows)
- Decaying Flow Agreement (1to1 decaying money flow with a distribution limit and a half-life of flow rate)
- Instant Distribution Agreement (1toN instant transfer)
- Constant Flow Distribution Agreement (1toN constant money flows)

How to have compositionality and add context to the system?

DISCLAIMER: Not everything mentioned here is implemented in the spec yet, but we will show the working Haskell code that demonstrates the main idea.

```
-- simplified for brevity
class AgreementOperationWithData a where
runAgreement :: a -> IO ()
data PaperAgreement = MkPaperAgreement String
instance AgreementOperationWithData PaperAgreement where
runAgreement (MkPaperAgreement s) = putStrLn s
-- | A contract executable within the IO monad context.
data Contract = Contract
{ contractPreCond :: IO Bool
, contractExecs :: [AnyAgreementOperationWithData]
, contractAttachedCond :: (IO Bool, AnyAgreementOperationWithData)
}
-- Define an existential type to avoid an explicit sum type...
data AnyAgreementOperationWithData = forall a.
AgreementOperationWithData a => MkAnyAOD a
instance AgreementOperationWithData AnyAgreementOperationWithData where
runAgreement (MkAnyAOD a) = runAgreement a
```

```
data Contract = Contract
{ contractPreCond :: IO Bool
, contractExecs :: [AnyAgreementOperationWithData]
, contractAttachedCond :: (IO Bool, AnyAgreementOperationWithData)
}
execContract :: Contract -> IO ()
execContract (Contract preCond execs _) = do
pred <- preCond
if pred then mapM_ runAgreement execs
else putStrLn "No bueno, amigo"
execCondContract :: Contract -> IO ()
execCondContract (Contract _ _ (cond, a)) = do
pred <- cond
if pred then runAgreement a
else putStrLn "No tan rápida, amigo"
```

```
main = do
brrr <- newIORef False
let sec_says_no = return False
let sec_says_yes = return True
let when_money_goes_brrr = readIORef brrr
let c0 = Contract
sec_says_no
[ MkAnyAOD $ (MkPaperAgreement "Elon Musk buys Twitter") ]
(return False, MkAnyAOD $ MkPaperAgreement "Not possible")
let c1 = Contract
sec_says_yes
[ MkAnyAOD $ MkPaperAgreement "Bob sends Alice $42 dollar"
, MkAnyAOD $ MkPaperAgreement "Alice sends Carol $4.2 dollar"
]
( when_money_goes_brrr,
MkAnyAOD $ MkPaperAgreement "Alice pays Bob back $420 dollars" )
```

```
putStrLn "# Contract 0"
execContract c0
putStrLn "# Contract 1"
execContract c1
execCondContract c1
putStrLn "Money goes brrr..."
writeIORef brrr True
execCondContract c1
```

```
# Contract 0
No bueno, amigo
# Contract 1
Bob sends Alice $42 dollar
Alice sends Carol $4.2 dollar
No tan rápida, amigo
Money goes brrr...
Alice pays Bob back $420 dollars
```

"How to write a financial contract" by Simon Peyton Jones & Microsoft Research.

European option: at a particular date you may choose to acquire an “underlying” contract, or to decline

```
or :: Contract -> Contract -> Contract
-- Acquire either c1 or c2 immediately
zero :: Contract
-- A worthless contract
european :: Date -> Contract -> Contract
european t u = at t (u `or` zero)
```

Money at dynamic level has "potential to update its context".

- Let side effects make money useful!
- We already see the toy example using IO monad, in real implementation these are needed side effects:
- Load data from storage.
- Read context such as time.
- Authentication (Blockchain digital signature).
- Authorization (Who can update whose agreement?).
- Atomic transaction, for composed contract.
- …

```
class ( Monad tk
, SuperfluidTypes sft
, Account acc sft
) => Token tk acc sft | tk -> acc, tk -> sft where
balanceOfAccount :: ACC_ADDR acc -> tk (SFT_RTB sft)
transfer :: CONTRACT_ACC_ADDR acc (ITA.Operation sft) -> SFT_MVAL sft -> tk ()
updateFlow :: CONTRACT_ACC_ADDR acc (CFA.Operation sft) -> CFA.FlowRate sft -> tk ()
-- ...
distributeProportionally
:: ACC_ADDR acc -- publisher
-> ProportionalDistributionIndexID -- indexId
-> SFT_MVAL sft -- amount
-> tk ()
-- ...
```

- Token is like a bank, and it manages accounts.
- But note can be modeled similarly too as an monad!
- Choose effect systems: mtl,
*transformers*, free monads, polysemy.

- Early Superfluid Protocol idea is implemented for EVM blockchains in Solidity language.
- Not all the denotational semantics have been implemented.
- Live in production: Polygon, Gnosis Chain, Optimism, Arbitrum, Avalanche, BSC.
- Achieved stats: >= 30K addresses, >= $10M streamed a month.

- Still work in progress, but already functional.
- Plan to fully support and prototype new denotational semantics for payment.
- Plan to also work on financial contract combinators, inspired by Simon Peyton Jones' "Composing contracts"
paper
^{2}.

- Bartosz Milewski

- Ken Scambler

- Victor Frankl
~~Victor Frankl~~/jk

- Philip Wadler

Limit / Colimit.

- Real Time Payment - A money distribution where the value of each monetary unit in it is also a function of
*time*. - Compositionaility - The morphism of the money distribution are composed financial contracts.
- Real Time Accounting - Natural transformations between different accounting domains (RTB of Account, Balance Sheet, Income Statement, Cashflow Statement, etc.)

- Superfluid monorepo: https://github.com/superfluid-finance/protocol-monorepo/
- Presentation source: