Learning from CL

[jhbertra]

Yesterday @yveshauser gave a very interesting presentation on Contract Language (CL). I thought it would be a good idea to open a discussion about lessons we could learn or things we might want to consider adapting to Marlowe.

[yveshauser]

Thanks for opening the discussion. Just as a reference, CL and the extraction of CL to a payoff language is defined in the following publications:

• https://github.com/HIPERFIT/contracts/blob/master/doc/icfp2015.pdf
• https://dannenkov.me/papers/annenkov-elsman-ppdp18.pdf

[jhbertra]

There are a lot of things I like about CL. Some would be relatively easy for us to integrate, some less so. Three clear candidates from my perspective are:

• The typed expression sublanguage
• A relative time model
• Parallel composition

Typed Expression Sublanguage

Marlowe and CL both support boolean and numeric expressions. Marlowe represents these with two mutually recursive data types: Observation represents boolean expressions, and Value represents numeric expressions. Conversely, CL represents both with a generalized algebraic data type that carries the expression's type in a parameter (see here for details).

The advantage of the expression sublanguage approach is that it allows polymorphic language constructs. In particular, let bindings and Cond (if) expressions can be generalized to any expression type, not just numeric values.

Relative Time Model

There are two differences in how Marlowe and CL represent time: relativity and unit. Marlowe uses milliseconds as the unit, whereas CL uses days. Marlowe's time values are absolute, or more precisely, they are all relative to a fixed point (the UNIX epoch). In contrast, CL's time values are relative to the contract's start date. Both offer advantages, but actual financial contracts almost always use relative times, not absolute ones. Additionally, relative times make contracts more reusable, as one can change the schedule of a contract without changing the contract definition (by changing the effective start date). Finally, relative times ensure sensible temporal ordering of sub-contracts, as one schedule date cannot occur before a previous one (assuming the language only allows schedule times to be advanced forward and not backward).

Parallel composition

CL supports contract conjunction via its & combinator. The case studies in the paper all use this combinator extensively, and we regularly feel the need for it when writing realistic contracts. We have previously investigated implementing a Both combinator which does the same thing.

[yveshauser]

Denotational semantics

CL defines denotational semantics, as well as reduction semantics, where Marlowe has just reduction semantics. Denotational semantics allows to simplify contracts to a normalized form (section 2.4: Contract Equivalences), i.e. by adding denotational semantics to Marlowe we could accomplish optimizations of Marlowe contracts

[yveshauser]

Payoff language

CL considers pricing a particular use-case for a contract language. In addition to CL they defined the CL payoff language, which is designed to be well suited for integration with Monte Carlo simulation techniques for pricing.
Should pricing of contracts also be explored for Marlowe contracts?