Open in app

Sign in

Write

Sign in

The Love Smart Contract Language: Introduction & Key Features — Part I

David Declerck
Dune Network
Published in
7 min readFeb 1, 2020

By De Oliveira Steven & David Declerck

What Is Love?

Love is a new native smart contract language for the Dune Network, meant to coexist alongside with Michelson. Also designed with formal verification in mind, Love offers new exclusive features to improve smart contracts design and implementation, among which:

  • direct read-only access to another contract’s storage
  • library contracts that can be either statically or dynamically referenced
  • easy-to-read target language for higher-level languages
  • high-level enough so that contracts can also be directly written in Love.

In this first article, we will introduce the basics of the language. The next article, Part 2, will introduce the module system, used to easily compose smart contracts.

Why Love?

The former smart contract language on the Dune Network, Michelson — inherited from Tezos — has been designed with its implementation using GADTs in mind. GADTs are a powerful feature of the OCaml type-system, but they come with many drawbacks: they make the language limited, constrained and hard to change. As a result, anyone who tried to write a (non-trivial) smart contract in Michelson knows how tedious it can be: it has a very restricted set of instructions, is rather hard to read for the uninitiated (and not straightforward for the initiated), making contract auditing an almost impossible task, and its stack is tricky to deal with. In particular, accessing variables requires to constantly remember their position in the stack and the current stack height, which is error-prone. This also makes it harder to use Michelson as a target language for compilation.

With this in mind, and notwithstanding the qualities of the Michelson language, we wanted to offer a more general-purpose alternative language, hence Love, also amenable for formal verification.

Basic Contract Structure

Love is a functional language, and borrows its syntax both from Liquidity and OCaml. As Love is a target language, developers are not supposed to write directly in Love. In this article, we will still write some contracts in Love, to better understand how it works.

Before entering the details of the language, let’s start with a simple smart contract that counts how many times it was called and how many DUNs it received:

#lovetype storage = {
  total : dun;
  calls : nat;
}val%init storage (_ : unit) = {
  total = 0.0dn;
  calls = 0p;
}val%entry main (s : storage) (amount : dun) (_ : unit) =
  let total = s.total +$ amount in
  let calls = s.calls ++ 1p in
  [][:operation], { total; calls }

All Love smart contracts share the same basic structure. The very first line must begin with a #love directive, to distinguish them from the Michelson smart contracts (which should now start with a #mic directive, although if missing, the language will default to Michelson).

Then follows one or more type declarations, one of them being the mandatory storage type declaration, which specifies the layout of the contract data. As in Liquidity and OCaml, these can be either record types, sum types, tuples, or just aliases to other types. In the above example, the storage type is a record containing two fields, total of type dun (the type of amounts) and calls of type nat (natural numbers). Many different types exist, such as bool, int, string, bytes, keyhash, address… You may refer to the Love documentation for a complete list of types.

After this, a storage initializer should be specified. It is a unique function named storage, introduced with val%init and having a single argument, used to produce the initial storage of the contract when it is originated. If a storage initializer is not specified, then the programmer will have to manually build an initial storage in order to originate the contract. In our example, the storage initializer does not use its argument, so it is given a type unit and no name. It sets the field total to 0 DUN and the field calls to 0. Notice how these constants are written: an amount in DUN ends with dn, and a natural number ends with p (whereas an integer would have no suffix). Check the documentation for how to write constants in Love.

Finally, a contract defines one or more entrypoints, which are functions introduced with the val%entry keyword and which take three arguments: the contract storage, the transaction amount, and a parameter. The type of the two first argument is fixed, thus it is not mandatory to specify them. Also, entrypoints return a pair of values: a (possibly empty) list of operations (transactions or originations), and the new value of the storage. The returned operations are performed after the contract has finished its execution. In our example, the entrypoint main adds the amount of duns received to the total amount of DUN memorized in the storage s, increments the number of calls by one, builds a new storage with these values, and returns a pair composed of an empty list of operations and this new storage.

Two important aspects of the Love language are displayed in this simple contract:

  • First, unlike in Liquidity (and many other languages), we used different addition operators: we used +$ to add duns and ++ to add naturals (and we would just have used + on integers). Indeed, there is no operator overloading in Love, so each operator works on specific types. All these operators and their naming scheme are detailed in the documentation.
  • Secondly, to build the empty list of operations, we wrote [][:operation]: indeed, the empty list constructor [] is polymorphic, i.e. it allows to construct a list of anything, so the type of elements contained in the list must be specified. This mechanism is ubiquitous in Love, and should be understood properly to use Love at its best. It is further described in the next section.

Functions, Recursion and Polymorphic Functions

Functions

Similarly to how entrypoints are defined, one may also define functions. A function is introduced by the val keyword, followed by its name, the list and type of its arguments, and its return type. For instance:

val add_and_sub (x : int) (y : int) : int * int =
  (x + y, x - y)

This defines a function add_and_sub that takes two integers as argument and returns a pair of integers. This function will be visible from the outside, so other smart contracts may call it. This can be prevented by declaring the function with val%private instead of val.

User-defined functions can then be used as any other Love built-in function. For instance, to use the add_and_sub function defined above, we may write:

  let (sum, diff) = add_and_sub 42 14 in
  ...

It is also possible to declare functions locally, in another function or entrypoint. In this case, the function is introduced with a let ... in construct, and its return type does not need to be specified:

val%entry main storage amount (_ : unit) =
  let double (x : int) = x * 2 in
  [][:operation], double storage

Here, the function double is local to the entrypoint main.

Recursive Functions

Love also supports recursive functions, useful for simulating loops and iterating over collections. Such functions are introduced with val rec or let rec ... in , and their return type must always be specified (even when defined locally). For instance:

val%entry main storage amount (_ : unit) =
  let rec mul_pow_2 (x : int) (t : nat) : int =
    if t = [:nat] 0p then x
    else mul_pow_2 (x * 2) (t -+ 1p)
  in
  [][:operation], mul_pow_2 storage 3p

This defines a (local) recursive function mul_pow_2, that (inefficiently) computes x * 2 ^ t, and uses it on the contract’s storage.

Polymorphism

Many Love primitives are designed to work with values of different types: they are said to be polymorphic. This is the case for primitives on collections (for instance lists, sets and maps, that may contain either integers, strings, records…), as well as comparison operators.

To use these primitives and operators, one has to explicitly specify the type of its argument, by performing what we call a type application. This is achieved by passing one or more arguments of the form [:type] to the primitive or operator. For instance, in the previous example, we applied the type nat to the = operator by writing = [:nat]. Note that in this particular case, the type could be omitted and inferred automatically, since one of the operands is a constant.

Love also allows the programmer to define his own polymorphic functions. This is achieved by adding type variables as arguments to the function, and then using these to specify the types of actual arguments. Type variables are introduced using a ' symbol. Here is an example of a user-defined polymorphic function:

val make_triple 'a 'b 'c (x : 'a) (y : 'b) (z : 'c) : 'a * 'b * 'c =
  (x, y, z)

Calling such a function simply requires passing the types as arguments, as we would do with polymorphic primitives:

let t = make_triple [:int] [:string] [:bool] 42 "Hello" true in ...

Note that type arguments do not specifically have to be placed first in a function declaration. For instance, one could write:

val make_triple 'a (x : 'a) 'b (y : 'b) 'c (z : 'c) : 'a * 'b * 'c =
  (x, y, z)

This function would then be called as follows:

let t = make_triple [:int] 42 [:string] "Hello" [:bool] true in ...

The interested reader may refer to literature about System-F for the theoretical background.

Closing Words

This concludes Part 1 of our technical introduction to Love. In the next part, we’ll see how to better structure a smart contract through the use of modules, and discuss how to implement contract interactions, i.e. how a contract can create or call another contract and read its storage through views. Meanwhile, don’t hesitate to follow the Love tutorial and to read the documentation.

EDITED: check our next article on Love: The Love Smart Contract Language: Introduction & Key Features — Part II

These are some of the resources you might find interesting in building your own smart contracts:

And other resources on the Dune Network:

Smart Contracts
Blockchain
Technical
Dune Network
Love

--

--

David Declerck
Dune Network

Written by David Declerck

10 Followers
Editor for

Help

Status

About

Careers

Press

Blog

Privacy

Terms

Text to speech

Teams