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?

In Kindelia, a contract is just a function that returns an IO, performing side-effective actions on the network, including saving/loading persistent state, getting the caller name and block height, and calling other IOs. As such, contracts are simply invoked by calling them with their inputs, and they can then do whatever they need, like a normal program. 5 years later and I don't think there must be a different or fancy way to treat contracts. Below is a "Counter" example:

// Creates a Counter function with 2 actions:
ctr {Inc} // action that increments the counter
ctr {Get} // action that returns the counter
fun (Counter action) {

  // increments the counter
  (Counter {Inc}) =
    !take x        // loads the state and assigns it to 'x'
    !save (+ x #1) // overwrites the state as 'x + 1'
    !done #0       // returns 0

  // returns the counter
  (Counter {Get}) =
    !load x // loads the state
    !done x // returns it

// initial state is 0
} with {
  #0
}

Its type, if written, would be Counter : CounterAction -> IO<U128>. Note that contracts must necessarily have dependent types, since the type they return may depend on the value of the action the caller is taking.

Of course, different networks might have wildly different types with more or less restrictions, but they must, at the very least, satisfy two fundamental needs: persisting state, and communicating with other contracts.