Michelson is a smart contract language from the Tezos community. Akin to Forth, Michelson contract is described by a sequence of instructions operating on a typed stack. Each instruction assumes a stack of a certain type as input and produces an output stack of determined type. For example, the `PAIR`

instruction presumes a stack of the type `a : b : s`

and produces a stack of the type `pair a b : s`

for any stack tail `s`

. You can read more about Michelson instructions and typing in the official documentation.

In January 2019, in collaboration with Tocqueville Group, Serokell started the Morley project. One of its goals was to implement a comprehensive framework for testing arbitrary Michelson contracts that would support simple unit testing as well as more complex property-based testing. Being more precise, we wanted to take a contract and feed with various sets of input and output values and see if it behaved as expected.

A small remark before we go forward. In this article, we cover only a small subset of the Michelson’s instructions and consider only the core of the Michelson’s type system without taking annotations into account. Clearing up all these details was a complicated task we performed during our work on the Morley framework, and we welcome everybody to go and check the repository to see the implementation of a type check and interpretation with all underlying details.

It was decided to use Haskell for the Morley implementation, and firstly we developed the Michelson language as a very simple AST data type:

```
data T =
Tint
| Tnat
| Toption T
| Tlist T
data UVal =
UInt Integer
| USome UVal
| UNone
| UList [UVal]
data UInstr =
UNOP
| UDROP
| UDUP
| USWAP
| UPUSH T UVal
| UPAIR
| UCAR
| UCDR
| UADD
| UCONS
| UNIL T
| UIF_CONS
```

Soon we understood this simple AST suffered from certain limitations. First of all, it was untrivial to generate arbitrary loosely-typed values. In our AST, list was merely a constructor `UList [UVal]`

and we couldn’t write an `Arbitrary`

instance that would generate an arbitrary list of integers or strings depending on the type context.

The answer to this problem was obvious: create an AST with stronger types. Expression then becomes annotated with a type, which is easy to implement thanks to awesome `GADTs`

and `DataKinds`

extensions. This immediately solves the problem of arbitrary value generation. And moreover, it becomes possible for the interpreter to stop unpredictably failing with runtime type errors.

```
data Val t where
VInt :: Int -> Val 'TInt
VNat :: Word -> Val 'TNat
VList :: [Val t] -> Val ('TList t)
VPair :: Val p -> Val q -> Val ('TPair p q)
```

But after introducing this type, we quickly found ourselves at a challenge. It was very easy to parse textual code representation to a simple AST but was obscure how to do the same for a typed representation of Michelson. To simplify things, instead of parsing, we considered a task of conversion from a simple AST to a typed AST.

The first problem with conversion from a simple AST to a typed representation was that conversion of a parent branch in an AST depended on the types of children. A useful trick for solving this issue can be found in the blog post from 2009. In short, we create an existential type holding value along with its type and return this existential type from our type check function:

```
data Sing (t :: T) where
STInt :: Sing 'TInt
STNat :: Sing 'TNat
STList :: Sing t -> Sing ('TList t)
STPair :: Sing p -> Sing q -> Sing ('TPair p q)
data SomeVal1 where
SomeVal1 :: Val t -> Sing t -> SomeVal1
typeCheckVal1 :: UVal -> Maybe SomeVal1
typeCheckVal1 (UInt i) = Just $ SomeVal1 (VInt i) STInt
typeCheckVal1 (UPair p q) = do
SomeVal1 pv pt <- typeCheckVal1 p
SomeVal1 qv qt <- typeCheckVal1 q
pure $ SomeVal1 (VPair pv qv) (STPair pt qt)
typeCheckVal1 (UList _) = error "not implemented"
```

The `Sing`

data type can be derived automatically with the use of the singletons library. That library provides the `Sing`

data family and useful helper functions and classes for work with singletons. Throughout this article, we’ll stick to handwritten `Sing`

and conversion functions.

There are two major problems with this construction. First, a reader may have noticed that neither `STNat`

nor `VNat`

constructors were ever used. Indeed, the `UInt`

constructor from a simple AST was meant to represent both signed and unsigned integers because they have roughly the same representation. We can not really distinguish between `TInt`

and `TNat`

literals during parsing.

A similar issue appears in the case of a list constructor with an empty list wrapped in it. When given a list constructor, we have no idea what type of values this list contains. In the case of an empty list, we must return the `forall t. TList t`

type, but our type representation does not support such a construction.

The second problem with this snippet is similar. In case of a non-empty list, we can take `t`

as a type of the first element and figure out if other elements in the list have the same type by comparing them. But to compare a `t1`

type of the first list element with a `t2`

type of the second list element, we need constraints `Typeable t1`

and `Typeable t2`

to hold.

It’s relatively easy to address the second problem. We introduce a `SomeVal`

data type with `Typeable`

constraint put in the scope of the constructor:

```
data SomeVal where
SomeVal :: Typeable t => Val t -> Sing t -> SomeVal
```

The first problem requires a switch to a different approach for type checking. One way to solve the problem is to introduce some sort of constrained `forall`

quantifier into our simplistic type system, similar to what we have in Haskell. For the empty list case, we can write something like `SomeVal (VList []) (forall n. Num n => n)`

. This approach is more universal but far heavier to implement and maintain.

Luckily for us, a lighter approach is possible for type checking Michelson programs. Although all Michelson instructions are polymorphic, Michelson programs are always given in the context of a contract. A contract defines an input stack type, and each instruction modifies a stack type in an unambiguous way. Hence, there is no actual need to implement a type checking algorithm that derives a type (with some `forall`

quantifiers)
for an arbitrary sequence of Michelson instructions. We are going to start with the input stack type and iterate through instructions. This way, we’ll be able to stick to the type system represented by the `T`

data type.

In this example, we considered only the type checking of values. Following the rule defined above, we’ll implement the `typeCheckVal`

function with the first argument being a type of an expression we’re trying to parse. There are only two instructions that introduce new value to the stack (namely, `UPUSH`

and `UNIL`

) and both of them explicitly have type representation included.

```
typeCheckVal :: Sing t -> UVal -> Maybe (Val t)
typeCheckVal STInt (UInt i) = Just (VInt i)
typeCheckVal STNat (UInt i) = do
guard (i >= 0)
pure (VNat $ fromIntegral i)
typeCheckVal (STPair pt qt) (UPair p q) = do
pv <- typeCheckVal pt p
qv <- typeCheckVal qt q
pure $ VPair pv qv
typeCheckVal (STList t) (UList l) =
VList <$> mapM (typeCheckVal t) l
typeCheckVal _ _ = Nothing
```

We do not actually need to wrap `Val t`

into `SomeVal`

here because the first argument nicely defines the output of the function. It’s important to emphasise the role of singletons in the construction above. What we do is pattern-matching on the type of value that should be parsed. Pattern-matching on type in the code of term-level functions is not common in Haskell, and singletons are perhaps the most straightforward way.

Now, let’s implement a conversion for instructions. First, we’ll have to modify our `Sing`

data type slightly and provide some required helper functions:

```
data Sing (t :: T) where
STInt :: Sing 'TInt
STNat :: Sing 'TNat
STList :: Typeable t => Sing t -> Sing ('TList t)
STPair :: (Typeable p, Typeable q)
=> Sing p -> Sing q -> Sing ('TPair p q)
fromSing :: Sing t -> T
fromSing = ...
data SomeSing where
SomeSing :: Typeable t => Sing t -> SomeSing
withSomeSing
:: SomeSing
-> (forall t . Typeable t => Sing t -> a)
-> a
withSomeSing (SomeSing a) f = f a
toSing :: T -> SomeSing
toSing = ...
```

Similarly to values, we’ll define a typed representation of an instruction. The `Instr`

data type is parametrized by type parameters `inp`

and `out`

of kind `[T]`

which state for input and output stack types corresponding to an instruction. This Michelson instructions representation is very elegant as it perfectly mimics the notation given in Michelson’s documentation.

```
data Instr (inp :: [T]) (out :: [T]) where
Seq :: Instr a b -> Instr b c -> Instr a c
Nop :: Instr s s
DROP :: Instr (a ': s) s
DUP :: Instr (a ': s) (a ': a ': s)
SWAP :: Instr (a ': b ': s) (b ': a ': s)
PUSH :: Val t -> Instr s (t ': s)
PAIR :: Instr (a ': b ': s) ('TPair a b ': s)
CAR :: Instr ('TPair a b ': s) (a ': s)
CDR :: Instr ('TPair a b ': s) (b ': s)
NIL :: Instr s ('TList t ': s)
CONS :: Instr (t ': 'TList t ': s) ('TList t ': s)
ADDii :: Instr ('TInt ': 'TInt ': s) ('TInt ': s)
ADDnn :: Instr ('TNat ': 'TNat ': s) ('TNat ': s)
ADDin :: Instr ('TInt ': 'TNat ': s) ('TInt ': s)
ADDni :: Instr ('TNat ': 'TInt ': s) ('TInt ': s)
IF_CONS :: Instr (a ': 'TList a ': s) s'
-> Instr s s'
-> Instr ('TList a ': s) s'
```

The representation of the `ADD`

instruction is not very nice but can be improved with the use of a type class. We may create a type class `AddOp`

which takes two type arguments (for two operands of the `ADD`

instruction). It will contain one function for type checking, one function for interpretation and a type family for the result type. For simplicity, this is not implemented in the article’s code.

Our function `typeCheckI`

will take an input stack type and an untyped instruction and should return an output stack type along with a typed instruction. Hence, we introduce `Stack`

and `SomeInstr`

data types. The `Stack`

data type is similar to `Rec`

from the vinyl package. The only difference is that we impose the `Typeable`

constraint on the first argument of `:&`

.

```
data Stack inp where
SNil :: Stack '[]
(::&) :: (Typeable s, Typeable a)
=> Sing a -> Stack s -> Stack (a ': s)
infixr 7 ::&
data SomeInstr inp where
(:::) :: Typeable out
=> Instr inp out -> Stack out -> SomeInstr inp
infixr 5 :::
```

Now we’re able to finally implement the `typeCheck`

function:

```
typeCheckI
:: Typeable inp => Stack inp -> UInstr -> Maybe (SomeInstr inp)
typeCheckI s UNOP = pure (Nop ::: s)
typeCheckI (_ ::& s) UDROP = pure (DROP ::: s)
typeCheckI (a ::& s) UDUP = pure (DUP ::: a ::& a ::& s)
typeCheckI (a ::& b ::& s) USWAP = pure (SWAP ::: b ::& a ::& s)
typeCheckI s (UPUSH t v) = withSomeSing (toSing t) $ \t' -> do
val <- typeCheckVal t' v
pure (PUSH val ::: t' ::& s)
typeCheckI (a ::& b ::& s) UPAIR = pure (PAIR ::: STPair a b ::& s)
typeCheckI (STPair a _ ::& s) UCAR = pure (CAR ::: a ::& s)
typeCheckI (STPair _ b ::& s) UCDR = pure (CDR ::: b ::& s)
typeCheckI (STInt ::& STInt ::& s) UADD = pure (ADDii ::: STInt ::& s)
typeCheckI (STNat ::& STNat ::& s) UADD = pure (ADDnn ::: STNat ::& s)
typeCheckI (STInt ::& STNat ::& s) UADD = pure (ADDin ::: STInt ::& s)
typeCheckI (STNat ::& STInt ::& s) UADD = pure (ADDni ::: STInt ::& s)
typeCheckI s (UNIL t) = withSomeSing (toSing t) $ \t' ->
pure (NIL ::: STList t' ::& s)
typeCheckI ((_ :: Sing a) ::& STList (e :: Sing b) ::& s) UCONS = do
Refl <- eqT @a @b
pure (CONS ::: STList e ::& s)
typeCheckI (STList a ::& s) (UIF_CONS consCase nilCase) = do
nc ::: (s' :: Stack out1) <- typeCheck s nilCase
cc ::: (_ :: Stack out2) <- typeCheck (a ::& STList a ::& s) consCase
Refl <- eqT @out1 @out2
pure (IF_CONS cc nc ::: s')
typeCheckI _ _ = Nothing
typeCheck
:: Typeable inp => Stack inp -> [UInstr] -> Maybe (SomeInstr inp)
typeCheck s [] = pure (Nop ::: s)
typeCheck s (i : []) = typeCheckI s i
typeCheck s (i : is) = do
a ::: s' <- typeCheckI s i
b ::: s'' <- typeCheck s' is
pure (a `Seq` b ::: s'')
```

In `typeCheckI`

, we pattern-match on an input stack type and an untyped instruction. In the case of `CONS`

, we need to additionally check the equality of first element of the stack and an subtype of the list at the second element of the stack. In the case of `IF_CONS`

, a recursive call to `typeCheck`

is used to check both continuations.

Now, when we have finally settled down how to type check a sequence of Michelson instructions, let’s see how our eDSL can be interpreted.

```
interpret
:: Rec Val inp -> Instr inp out -> Rec Val out
interpret s Nop = s
interpret s (Seq a b) = interpret (interpret s a) b
interpret (_ :& s) DROP = s
interpret (a :& s) DUP = a :& a :& s
interpret (a :& b :& s) SWAP = b :& a :& s
interpret (a :& b :& s) PAIR = VPair a b :& s
interpret s (PUSH v) = v :& s
interpret (VPair a _ :& s) CAR = a :& s
interpret (VPair _ b :& s) CDR = b :& s
interpret (VInt a :& VInt b :& s) ADDii = VInt (a + b) :& s
interpret (VInt a :& VNat b :& s) ADDin = VInt (a + fromIntegral b) :& s
interpret (VNat a :& VInt b :& s) ADDni = VInt (fromIntegral a + b) :& s
interpret (VNat a :& VNat b :& s) ADDnn = VNat (a + b) :& s
interpret s NIL = VList [] :& s
interpret (a :& VList l :& s) CONS = VList (a : l) :& s
interpret (VList [] :& s) (IF_CONS _ nilCase) = interpret s nilCase
interpret (VList (a : l) :& s) (IF_CONS consCase _) =
interpret (a :& VList l :& s) consCase
```

Interestingly, the `interpret`

function is total, which is a definite benefit of advanced type representation. The `Val`

data type contains enough information for a type checker to consider all possible cases of an input stack and instruction, and there’s no need to perform additional checks in runtime, which is an error-prone practice. In short, if the program type checks, it won’t produce an error in runtime.

To sum up, in this article we’ve seen how to apply some advanced typing techniques of Haskell to type-check simple strictly-typed stack-based language. We took a simple representation of language AST (which can be easily obtained from a text using any technique for parsing) and converted it to a strictly-typed representation of the same language. The strictly-typed representation is in 1:1 correspondence to the type system of defined language, and by having a term in strictly-typed representation, we are assured that it’s well-typed. The approach described is heavily dependent on the fact that the type system doesn’t define abstract types and all types are concrete, i.e. only built-in constructions are polymorphic. This restriction applies to a wide variety of languages, hence we see our approach as highly reusable.