Ethereum, Libra and a Unified Type System

Libra, with its new language Move, was recently announced and some of its features are interesting. Here, we will only be covering those related to its type system, comparing it to Ethereum/Solidity and dType and then presenting some interesting conclusions, suggestions, and some demos at the end.

For additional Ethereum-Libra feature comparisons, check out: https://github.com/pipeos-one/chaincompare and feel free to correct and contribute.

Type-related Features

EVM & Solidity

Solidity is a statically typed language with support for elementary types (booleans, integers, address, byte arrays, strings, enums, functions etc.) and complex types (mappings, fixed-size & dynamic-size arrays, structs). Developers can create their own named types with struct.

These custom types and helper functions can be reused by others if they are defined in libraries, or by inheritance if they are defined in a contract. The former is more elegant, as it separates type definition and helper functions from data storage.

Therefore, you can define reusable types like this:

// MarketProductLib.sol
library MarketProductLib {
  struct MarketProduct {
    bytes32 id;
    uint64 amount;
    uint64 price;
  }
  function productFunction (MarketProduct product) public {}
}
// OriginatedMarketProductLib.sol
import 'MarketProductLib.sol';
library OriginatedMarketProductLib {
  struct OriginatedMarketProduct {
    MarketProductLib.MarketProduct product;
    address creator;
  }
  function originatedProductFunction (OriginatedMarketProduct product) public {}
}

This is the basis of how dType types are defined, but we will go into more details below.

Libra & Move

Both Move and Move VM are typed, currently supporting a small number of native types and values: booleans, unsigned 64-bit integers, 256-bit addresses, fixed-size byte arrays, structs (including resources), and references.

A key feature is its modularity, through separating custom type definitions (resources or unrestricted structs) and static functions from actual data, stored in each account. Modules, which contain the actual code, have no state. Modules can define resource types (nominal types, similar to Solidity structs) and procedures. They are kept in the global scope, meaning types can be reused from any defined module, as long as you know the module address, name, and resource name (e.g. 0x56.Currency.TCoin). Modules have an acyclic dependency relation.

The key feature of Move is the ability to define custom resource types … the Move type system provides special safety guarantees for resources. A resource can never be copied, only moved. These guarantees are enforced statically by the Move VM.

The bytecode verifier checks properties like type-safety, reference-safety, and resource-safety (i.e., resources are not duplicated, reused, or inadvertently destroyed). The rules for mutating, deleting, and publishing a resource are encoded in the module that created the resource and declared its type.

The state is stored in account resources. For example, the number of TCoins held by an account 0x12.., is found at a unique access path determined by account address, module address, and name, resource name: 0x12/resources/0x56.Currency.TCoin.

Procedures are uniquely identified by its module identifier and signature and module dependencies are acyclic. This ensures that all procedure calls in Move are statically determined.

These features, along with no dynamic dispatch and limited mutability offer a more deterministic environment for doing static verification of computations.

Additionally, the design supports parallel execution of transactions if there are no state conflicts. Memory cells are found at a unique access path (e.g. 0x12/resources/0x56.Currency.TCoin), therefore conflicts are easier to find.

Let us write our initial type definition example in Move IR:

module MarketProductModule {
  resource MarketProduct {
    id: bytearray,
    amount: u64,
    price: u64,
  }
}
module OriginatedMarketProductModule {
  import 0x3.MarketProductModule;
  resource OriginatedMarketProduct {
    creator: address,
    product: R#MarketProductModule.MarketProduct,
  }
}

Type Registry on-chain (Global Scope)

The advantage of having a type system is that bugs stemming from incorrect type assumptions (wrong input types given to a function, applying operators on variable types that should not be compatible) are caught at compile or run time. In our case, with both Solidity and Move, we are talking about static type checking at compile time. There are other advantages — enabling compiler optimizations, type documentation for free, customizing and extending type rules, etc.

However, there is one advantage that has become clear with the emergence of global operating systems, like Ethereum: we can have a global type system through which the system’s parts can interoperate. Projects should agree on standardizing types and a type registry, continuously working on improving them.

Currently, neither Ethereum nor Libra are using such a system, but it is just a matter of time. Libra Association is in a good position to control the types used for their platform and we do not know when they plan to open their testnet to external developers or whether external developers will have enough freedom on their platform.

For Ethereum, we have started dType, a decentralized typing system. For details, check out dType — Decentralized Type System & Functional Programming on Ethereum.

With dType, you define your types in libraries, along with helper functions, as in my first MarketProductLib and OriginatedMarketProductLib Ethereum example.

You can also define libraries for additional non-state changing helper functions. As in Libra’s case, these functions are easy to test for invariants and are deterministic. You can run your tests directly on Mainnet deployed libraries. Each of these functions has a unique identifier inside the registry, in the same way as Libra has a unique identifier for its procedures.

You can have an optional StorageContract for each type, if you want to centralized data storage for each type. Libra does the same thing — separates definitions and rules from data. However, in Libra, resource data is stored under each account. In Ethereum, this might be achievable with user-specific smart contracts, but a central storage contract has its benefits, even on the legal side: there is no one owner that is responsible. In a world where legal standards are not always congruent with moral standards, this can be useful.

Now, each type is registered in the dType registry contract. We even have a nice UI for this:

This is the actual type structure that gets stored on-chain:

[
 {
   “name”: “MarketProduct”,
   “types”: [
     {“name”: “bytes32”, “label”: “id”, “relation”: 0, “dimensions”:[]},
     {“name”: “uint64”, “label”: “amount”, “relation”: 0, “dimensions”:[]}, 
     {“name”: “uint64”, “label”: “price”, “relation”: 0, “dimensions”:[]}
 ],
   “optionals”: [],
   “outputs”: [],
   “lang”: 0,
   “typeChoice”: 0,
   “contractAddress”: “0x0000000000000000000000000000000000000000”,
   “source”: “0x0000000000000000000000000000000000000000000000000000000000000000”
 },
 {
   “name”: “OriginatedMarketProduct”,
   “types”: [
     {“name”: “MarketProduct”, “label”: “product”, “relation”: 0, “dimensions”:[]},
     {“name”: “address”, “label”: “creator”, “relation”: 0, “dimensions”:[]}
   ],
   “optionals”: [],
   “outputs”: [],
   “lang”: 0,
   “typeChoice”: 0,
   “contractAddress”: “0x0000000000000000000000000000000000000000”,
   “source”: “0x0000000000000000000000000000000000000000000000000000000000000000”
 },
]

Having a global type registry allows you to automate processes even between projects from unrelated entities.

Imagine a decentralized marketplace that looks at the OriginatedMarketProduct type and has access to all stored data, being able to choose the product based on the information it finds. Any vendor is free to add his information under that type. Transparently, without any interoperability issues, without asking.

Currently, using dType implies having to deal either with lower level assembly or some boilerplate code, for interfacing with the types.

There are solutions to make this as easy as in Libra:

• (best) EVM opcodes for supporting a dType-like system.
• (second best) (extra-)typed language, a superset of Solidity, that supports dType and transpiles to Solidity or Yul/bytecode.

New Ethereum Opcodes

The EIP is in work and it will be based on a previous dType EIP: https://github.com/ethereum/EIPs/pull/1900, but for now, we will explain some high-level concepts.

Ethereum 2.0. discussions mention support for multiple Execution Environments. This is the future: upgrading or switching blockchain mechanisms through smart contracts. This is how Libra also sets its decentralized versioned database rules. And this is how a system like dType will also become available to be easily used.

DTYPEID opcode: The opcode will receive a dType type identifier, defined as:

uint language = 0;  // Solidity language code is 0
string type_name = 'MarketProduct';
bytes32 identifier = keccak256(abi.encode(language, type_name);

In this case, language = 0 is for the EVM. The EVM will know the address of the dType registry contract and will be able to retrieve the type information, along with the type rules if they are defined. Libra’s bytecode verifier might be implementable for Ethereum in this manner, at compile time.

The new smart contract bytecode will, therefore, contain the type identifier. This can be added in contract events and in the ABI interfaces. Blockchain explorers would benefit, being able to actually analyze and label data without relying on off-chain centralized services to provide ABIs.

UPDATE: in-work document.

Move vs. Solidity + dType

Move VM was designed with types and determinism at the core or the system. Ethereum can implement a global type system on top of the current protocols and achieve even more than what the Libra Association/Facebook has announced.

Future data bridges between Ethereum and Libra

Data bridges between Ethereum and Libra will be easier if they have common data types.

Ideally, Ethereum should lead the work in defining a global type system and projects like Libra should use these definitions. Otherwise, Ethereum should be prepared to include future Libra types in its registry.

Bridging to other languages

When we talk about a global type registry, we are not only talking about a type registry for Ethereum. We are talking about a type registry that can offer type definitions for any language.

We plan to use dType to produce type definitions for TypeScript, Python, and Rust.

// TypeScript
// interfaces for basic types will be defined from the start; an example after which this can be done for Uint64 is https://github.com/DefinitelyTyped/DefinitelyTyped/blob/244bca7f3c37cb9651193337c3fd4b5c059fb0ea/types/cuint/index.d.ts
interface MarketProduct {
    id: bytes32;
    amount: Uint64;
    price: Uint64;
}
interface OriginatedMarketProduct {
  product: MarketProduct;
  creator: Address;
}
# Python
class MarketProduct:
  def __init__(self, id: Bytes32, amount: Uint64, price: Uint64):
    self.id = id
    self.amount = amount
    self.price = price
class OriginatedMarketProduct:
  def __init__(self, product: MarketProduct, creator: Address):
    self.product = product
    self.creator = creator

The definition snapshots will be stored on a decentralized storage system, such as Swarm, for ease of use.

Conclusion

Ethereum is a global operating system. So is Libra, even if the computing power is currently capped at 100 validators. The advantage that a global operating system brings to a type system is type reuse and interoperability between projects.

Developers can collaborate on types and upgrade them as time passes. Projects can have compatible APIs and your project is part of a bigger system.

Libra has already started to put types/resources as first-class. At the moment, developers are not allowed to publish their own types and there is no estimation of when they will be able to do so. Libra core developers will probably release their own types first, before they open the system to outside developers, to ease use. And there is a chance that they will end up controlling what types are predominantly used (if not entirely) on their network. This means they would be intermediaries and external projects will collaborate with them instead of with each other.

Ethereum can still make the first move if it starts adopting a type system. It might influence the Libra type definitions or at least it will be prepared to include them into its type system, to ensure compatibility.

Dear Ethereum people, if we do not want to lead today, we will be forced to follow tomorrow.

dType Demo — Decentralized Type System on Ethereum & Functional Programming (dApp)

File System with Semantic Search on dType, Ethereum

Example of what can be built on top of dType and how dTypes can have their own UI components that can be reused in dApps.