What is an appropriate type for smart contracts?

Question

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.