What is an appropriate type for smart contracts?

I'm wondering what is the best way to express smart contracts in typed languages such as Haskell or Idris (so you could, for example, compile it to run on the Ethereum network). My main concern is: what is the type that captures everything that a contract could do?

Naive solution: EthIO

A naive solution would be to define a contract as a member of an EthIO type. Such type would be like Haskell's IO, but instead of enabling system calls, it would include blockchain calls, i.e., it would enable reading from and writing to the blockchain's state, calling other contracts, getting block data and so on.

-- incrementer.contract

main: EthIO
main = do
   x <- SREAD 0x123456789ABCDEF
   SSTORE (x + 1) 0x123456789ABCDEF

This is clearly sufficient to implement any contract, but:

1. Would be too powerful.

2. Would be very coupled to the Ethereum blockchain specifically.

Conservative solution: event sourcing pattern

Under that idea, a contract would be defined as fold over a list of actions:

type Contract action state = {
    act  : UserID -> action -> state -> state,
    init : state
}

So, a program would look like:

incrementer.contract

main : Contract
main = {
    act _ _ state = state + 1,
    init          = 0
}

That is, you define an initial state, a type of action, and how that state changes when a user submits an action. That would allow one to define any arbitrary contract that doesn't involve sending/receiving money. Most blockchains have some kind of currency and most useful contracts involve money somehow, so that type would be way too restrictive.

Less conservative solution: events + currency

We can make the type above aware of currencies by hardcoding a currency logic into the type above. We'd, thus, get something like:

type Contract action state = {
    act        : UserID -> action -> state -> state,
    init       : state,
    deposit    : UserID -> Amount -> state -> state,
    withdrawal : UserID -> Amount -> state -> Maybe state
}

I.e., the contract developer would need to explicitly define how to deal with monetary deposits and withdrawals. That type would be enough to define any self-contained contract which can interact with the host blockchain's currency. Sadly, such a contract wouldn't be able to interact with other contracts. In practice, contracts often interact with each other. An Exchange, for example, needs to communicate with its exchanged Token contracts to query balances and so on.

Generalization: global state?

So, let's take a step back and rewrite the conservative solution as this:

type Contract = {
    act  : UserID -> Action -> Map ContractID State -> State,
    init : State
}

Under this definition, the act function would have access not only to the contract's own state but the state of every other contract on the same blockchain. Since every contract can read each other's state, one could easily implement a communication protocol on top of this, and, thus, such type is sufficient to implement arbitrarily interacting contracts. Also, if the blockchain's currency was itself implemented as a contract (possibly using a wrapper), then that type would also be sufficient to deal with money, despite not having it hardcoded on the type. But that solution has 2 problems:

1. Peeking at the other contract's state looks like a very "hacky" way to enable communication;

2. A contract defined this way wouldn't be able to interact with existing contracts which aren't aware of that solution.

What now?

Now I'm in the dark. I know I'm not in the right abstraction for this problem, but I'm not sure what it would be. It looks like the root of the problem is that I'm not able to capture the phenomenon of cross-contract communications properly. What concrete type would be more suitable to define arbitrary smart-contracts?

Before I answer the main question, I'm going to try to define a bit more precisely what it would mean to write code in Haskell or Idris and compile it to run on an Ethereum-like blockchain. Idris is probably a better fit for this, but I'm going to use Haskell because that's what I'm familiar with.

Programming model

Broadly, I can envision two ways of using Haskell code to produce bytecode for a blockchain virtual machine:

• A library that builds up EVM bytecode as Haskell data

• A GHC backend that generates bytecode from Haskell code

With the library approach, constructors would be declared for each of the EVM bytecodes, and library code layered on top of that to create programmer-friendly constructs. This could probably be built up into monadic structures that would give a programming-like feel for defining these bytecodes. Then a function would be provided to compile this datatype into proper EVM bytecode, to be deployed to the blockchain proper.

The advantage of this approach is that no added infrastructure is needed - write Haskell code, compile it with stock GHC, and run it to produce bytecode.

The big drawback is, it is not easily possible to reuse existing Haskell code from libraries. All code would have to be written from scratch targeted against the EVM library.

That's where a GHC backend becomes relevant. A compiler plugin (at present it would probably have to be a GHC fork, like GHCJS is) would compile Haskell into EVM bytecode. This would hide individual opcodes from the programmer, as they are indeed too powerful for direct use, relegating them instead to being emitted by the compiler based on code-level constructs. You could think of the EVM as being the impure, unsafe, stateful platform, analoguous to the CPU, which the language's job is to abstract away. You would instead write against this using regular Haskell functional style, and within the restrictions of the backend and your custom-written runtime, existing Haskell libraries would compile and be usable.

There is also the possibility of hybrid approaches, some of which I will discuss at the end of this post.

For the remainder of this post, I will use the GHC backend approach, which I think is the most interesting and relevant. I'm sure the core ideas will carry over, perhaps with some modification, to the library approach.

Programming pattern

You will then need to decide how programs are to be written against the EVM. Of course, regular, pure code can be written and will compile and compute, but there is also a need to interact with the blockchain. The EVM is a stateful, imperative platform, so a monad would be an appropriate choice.

We'll call this foundation monad Eth (although it doesn't strictly have to be Ethereum-specific) and equip it with an appropriate set of primitives to utilize the full power of the underlying VM in a safe and functional style.

We'll discuss what primitive operations will be needed in a moment, but for now, there are two ways to define this monad:

• As a builtin primitive datatype with a set of operations

  -- Not really a declaration but a compiler builtin
  -- data Eth = ...
  

• Since much of the EVM resembles an ordinary computer, mainly its memory model, a sneakier way would be to just alias it to IO:

  type Eth = IO
  

  With appropriate support from the compiler and runtime, this would allow existing IO-based functionality, such as IORefs, to run unmodified. Of course much IO functionality, such as filesystem interaction, would not be supported, and a custom base package would have to be supplied without those functions, to ensure code that uses them won't compile.

Primitives

Some builtin values will need to be defined to support blockchain programming:

-- | Information about arbitrary accounts
balance  :: Address -> Eth Wei
contract :: Address -> Eth (Maybe [Word8])
codeHash :: Address -> Eth Hash

-- | Manipulate memory; subsumed by 'IORef' if the 'IO' monad is used
newEthVar   :: a -> Eth (EthVar a)
readEthVar  :: EthVar a -> Eth a
writeEthVar :: EthVar -> a -> Eth ()

-- | Transfer Wei to a regular account
transfer :: Address -> Wei -> Eth ()

selfDestruct :: Eth ()

gasAvailable :: Eth Gas

Other basic functionality, including function calling, including deciding whether a call is a regular (internal) function call, a message call, or a delegate message call, will be handled by the compiler and runtime.

Type for smart contracts

We're now up to answering the original question: What is the appropriate type for a smart contract?

type Contract = ???

A contract needs to:

• Execute code on the EVM - return an action in the Eth monad
• Call other contracts. We will define an Eth action to do this in a moment.
• Take and return values, of type in and out
• access information about its environment, including:
  • amount transferred in current transaction
  • current, sending, and originating accounts
  • information about the block

Therefore, an appropriate type may be:

newtype Contract in out = Contract (Wei -> Env -> in -> Eth out)

The Wei parameter is informational only; the actual transfer occurs when the contract is called, and cannot be modified by the contract.

Regarding enviromental information, it is a bit of a judgement call to decide what should be passed as a parameter and what should be made available as primitive Eth actions.

Contracts can be called using a contract call primitive:

call :: Contract in out -> Wei -> in -> Eth out

Of course this is a simplification; for example, it does not curry the input type. presumably, the compiler will generate unique actions for each visible contract, similar to Solidity. It may not even be appropriate to make this primitive available.

One additional detail: EVM supports constructors, EVM code that will be executed at time of contract creation, to allow enviromental information to be used. Thus, the type of a contract, as written by a programmer, would be:

main :: Eth (Contract in out)
main = return . Contract $ \wei env a -> do
  ...

Conclusion

I've omitted many details, such as error handling, logging/events, Solidity interop/FFI and deployment. Nontheless, I hope I have given a useful overview of programming models for functional languages against blockchain smart contract environment.

These ideas are not stricly Ethereum-specific; however, do be aware that Ethereum uses an account-based model, while both Bitcoin and Cardano use a Unspent Transaction Output (UTxO) model, so many details will differ. Bitcoin doesn't really have a usable smart contract platform, while Cardano (whose smart contract functionality is in late tesing stages at time of writing) is programmed entirely in Plutus, which is a Haskell variant.

Rather than a strict library-based or backend approach to generating EVM bytecode, other more user-friendly approaches could be devised. Plutus, the Cardano blockchain language, uses a Template Haskell splice to embed on-chain Haskell code in ordinary Haskell, which is executed off-chain. This code is then processed by a GHC plugin.

Another intruiging idea would be to use Conal Eliot's compiling to categories to extract and compile Haskell code for the blockchain. This also uses a compiler plugin, but the neccesary plugin already exists. All that is neccessary to define instances of relevant category-theorwtic typeclasses, and you get -Haskell-to-arbitrary-backend compilation for free.

Further reading

While writing this post, I referred heavily to the following references:

• Ethereum Yellow Paper, The specificatiom of the Ethereum Virtual Machine
• Solidity ABI
• Solidity builtins

Other interesting resources:

• Safer smart contracts through type-driven development

  A paper describing a much fuller scheme for specifying smart contracts in Idris, leveraging dependent programming features to enforce important invariants

• Marlowe: financial contracts on blockchain

  A paper describing using functional languages for specifying blockchain smart contracts, a forerunner of the Cardano Plutus technologies

• fp-ethereum

  A list of references and gitter community for those interested in both functional programming and Ethereum smart contracts.

Two suggested solutions:

type Contract action state = {
    act  : UserID -> action -> state -> (state, Map ContractID State)
}

The map is used to keep track of the states of other contracts on the same blockchain. This solution has two advantages: it's very simple and doesn't require any special language features, and it can interact with existing contracts which don't know about this solution. Or just:

type Contract action state = {
    act  : UserID -> action -> state -> (state, List State)
}

Either way use a type that is not aware of the blockchain's currency. This type captures all possible actions that can be performed by a contract and how it changes its own state as well as the states of other contracts on the same blockchain. It also captures what happens when an action is submitted by a user. This last part is crucial for implementing communication protocols between smart-contracts. For example, if we want to implement an Exchange contract, then we'd need to know what happens when one exchange submits an order and another exchange accepts it or rejects it. That information needs to be communicated back from the second contract to the first one so that they both agree on their respective states after such submission/acceptance/rejection event has taken place. So, this type would capture all necessary information about cross-contract communications in addition to being able to define any arbitrary smart-contract logic without having hardcoded anything specific about Ethereum's currency into it (or even knowing whether there was some currency at all).