Imperative statements¶

This chapter will introduce the imperative statements that Indigo supports.

Remember: for a full list of the available operators and construct, please refer to reference page.

Getting control (statements)¶

Just as any other imperative language Indigo has common control statements, namely:

• if/then/else
• while
• forEach

but it also has less common ones, like:

• ifSome
• case_
• and more...

Let's take a look at the example file included in this chapter: Control.hs and its controlContract:

module Indigo.Tutorial.Statements.Control
  ( controlContract
  ) where

import Indigo

data IncrementIf
  = IsZero Integer
  | HasDigitOne Natural
  deriving stock (Generic, Show)
  deriving anyclass (IsoValue)

instance ParameterHasEntrypoints IncrementIf where
  type ParameterEntrypointsDerivation IncrementIf = EpdPlain

controlContract :: IndigoContract IncrementIf Natural
controlContract param = defContract do
  base <- new$ 10 nat
  result <- case_ param $
    ( #cIsZero #= \val -> do
        return (val == 0 int)
    , #cHasDigitOne #= \val -> do
        checkRes <- new$ False
        while (val > base && not checkRes) do
          val =: val / base
          remainder <- new$ val % base
          checkRes =: remainder == 1 nat
        return checkRes
    )
  if not result
    then storage =: 0 nat
    else storage += 1 nat

storage :: HasStorage Natural => Var Natural
storage = storageVar

This contract is fairly more complicated than the previous examples, but we can slowly take it apart and we'll come to understand it.

First of all we have a new data type IncrementIf:

data IncrementIf
  = IsZero Integer
  | HasDigitOne Natural
  deriving stock (Generic, Show)
  deriving anyclass (IsoValue)

instance ParameterHasEntrypoints IncrementIf where
  type ParameterEntrypointsDerivation IncrementIf = EpdPlain

We can see that our contract takes an IncrementIf as parameter, and since this is a valid type to use case_ with, we can use pattern-matching on it. Except for declaring a base variable, this is exactly what the contract code starts with: case_ takes param as argument and then defines a list of possible patter-matches, in this case #cIsZero and #cHasDigitOne, for its constructors IsZero and HasDigitOne, respectively.

controlContract :: IndigoContract IncrementIf Natural
controlContract param = defContract do
  base <- new$ 10 nat
  result <- case_ param $
    ( #cIsZero #= \val -> do
        return (val == 0 int)
    , #cHasDigitOne #= \val -> do
        checkRes <- new$ False
        while (val > base && not checkRes) do
          val =: val / base
          remainder <- new$ val % base
          checkRes =: remainder == 1 nat
        return checkRes
    )

We can also see that here case_ is used to create a new variable result by the use of the arrow <-. This is not necessary to case_, we could have avoided this and have each branch return nothing (aka ()), but in this case we want to perform a check based on param and have its result returned.

Let's look at the definition for the first branch, which is to say what follows the #= for #cIsZero:

    ( #cIsZero #= \val -> do
        return (val == 0 int)

Here we take the Integer parameter of IsZero, call it val, and start a code block with do that just returns True if val is 0 and False otherwise. This is indeed so simple it could have been defined without the code-block (and so the do) in a single line as:

\val -> return (val == 0 int)

Let's look instead at the isolated code for the second branch, the one for #cHasDigitOne:

    , #cHasDigitOne #= \val -> do
        checkRes <- new$ False
        while (val > base && not checkRes) do
          val =: val / base
          remainder <- new$ val % base
          checkRes =: remainder == 1 nat
        return checkRes

Here we take the Natural parameter of HasDigitOne and we call it val, then we start the code-block. This branch check that val has at least a digit equal to 1 in base 10, how this logic is implemented should be fairly simple to understand. In it we can see the usage of while that acts on a Boolean expression and has its own code-block.

An important thing to notice here is the scoping:

• we don't have any problem calling the input to this branch val even tho it has a different type and source than the val for the previous branch
• we can access base because it is part of the outer-scope
• outside of the branch we cannot access anything declared in it, like checkRes, because it gets destroyed as soon as we leave the branch
• the code-block of while has an even inner scope, it can access both the outermost (e.g. base) and the branch's (e.g. val/checkRes) scope, but its declarations (e.g. remainder) cannot be accessed outside of it

Indigo has automatic scope management and behind the scene will DROP the values associated with a scope as soon as this is no longer available.

Going back to the contract as a whole for just a second we can see, after result is calculated, an example of the if/then/else syntax:

  if not result
    then storage =: 0 nat
    else storage += 1 nat

This contract is a bit bigger than usual and not much readable as-is, moreover, the situation would get worse if we kept adding to it, especially if there are repeated blocks of code.

For this reason Indigo supports functions and procedures, which are the argument of the next chapter.

Technical details: Imperative statements and scopes¶

The icing on the cake of Indigo are the imperative statements like if, while, case_ and others that can be used in its code.

Let's just take if_ from the Indigo.Backend.Conditional module and explain its semantic. if_ has the following type:

if_ :: forall inp xs ys a b exc .
      ( IfConstraint a b
      , exc :~> Bool
      )
  => exc
  -> IndigoState inp xs a
  -> IndigoState inp ys b
  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)

First of all it takes three arguments: a boolean expression and Indigo code for the true and false branch. Let's take a closer look at the branches' code and the resulting one. Branches can end up with different stack types, but we have to unify them somehow to fit in the same output stack type.

This unification is obvious and comes from imperative languages, where there is the notion of scopes. If the execution leaves a scope all variables defined within it are destroyed. The same thing happens here and this is why, as explained before, we defined GenCode to also contain the Lorentz code able to return to the input stack.

This way constructs like if_ can remove the variables and types pushed by a branch, but there is still a feature missing. As you can see by the return type this is defined by RetOutStack and RetVars, these (supported by the IfConstraint) allow for the ability to return something from that scope, without it getting destroyed. You can find this defined in the Indigo.Backend.Scope module.

While what we described above is true for other statements as well, if_ specifically has one last bonus feature: replacing Haskell if/then/else syntax, thanks once again to RebindableSyntax.

Technical details: IndigoM freer monad¶

It's time to complete the full picture of Indigo machinery. Previously, IndigoState was explained, and theoretically, you could write Indigo code in the bare IndigoState monad, using >>= operator with RebindableSyntax, and you would get all the benefits of automatic stack management. However, one small drawback of this would be the necessity to specify input and output stack types in type annotations in some tricky usages of IndigoState. A more serious problem is that the fixed stack types in the annotations take away the possibility to do arbitrary logic-preserving transformations to the stack from the Indigo optimizer. So, in order to hide these parameters from the Indigo programmer, we introduce the IndigoM monad.

First of all, let's define

data Program instr a where
  Done :: a -> Program instr a
  Bind :: Program instr a -> (a -> Program instr b) -> Program instr b
  Instr :: instr a -> Program instr a

This is what's called "operation style" freer monad. There is a package on Hackage. There are two things which may attract your attention: that Program resembles the Monad interface and the instr type parameter. Program is basically a monad but one that keeps the whole flow of execution as a datatype: every constructor either corresponds to return, bind or just an effect. The instr type parameter represents a range of possible effects.

Let's say we have the following oversimplified GADT, which represents all possible statements in Indigo code:

data StatementF a where
  NewVar :: Expr x -> StatementF (Var x)
  SetVar :: Var x -> Expr -> StatementF ()

According to this GADT, we can just create new variables and set values to existing ones.

Having Program StatementF we could write simple programs in this monad, the only thing which lacks for our convenience is a monad instance for Program, which actually can be straightforwardly defined, and then you can enjoy do syntax:

instance Monad (Program instr) where
  return = pure
  (>>=) = Bind

Now, let's introduce the if statement, which complicates the definition of StatementF a bit:

data StatementF (freer :: Type -> Type) a where
  NewVar :: Expr x -> StatementF freer (Var x)
  SetVar :: Var x -> Expr x -> StatementF freer ()
  If :: Expr Bool -> freer a -> freer a -> StatementF freer a

As you can see, a new freer type parameter is added. The if statement, unlike simple NewVar and SetVar statements, contains two branches: one for a case in which a guard expression is evaluated to true, and another branch for false, both of which are sequences of statements. However, for sequences of statements we already have Program monad, and that's it: we got mutually recursive construction, where StatementF is a building block of Program, representing all possible statements, and on the other hand, Program is used in StatementF in statements, which contain other subprograms.

You could wonder: why just not to use Program in StatementF directly? If you try to do so, you may experience difficulties with mutually recursive types, like

If
  :: Expr Bool
  -> Program (Statement (Program ...)) a
  -> Program (Statement (Program ...)) a
  -> StatementF a

To dispel your possible confusion, let's gather everything together, getting the resulting type:

newtype IndigoM a = IndigoM (Program (StatementF IndigoM) a)

which automatically derives its Monad instance from Program. As a result, we've just built a "better" version of IndigoState, which doesn't expose input and output stacks. The full version of StatementF can be found in the Indigo.Frontend.Internal.Statement module and of Program in the Indigo.Frontend.Program module.

Let's discuss a bit how IndigoM is connected with the rest of the machinery. IndigoM can be traversed and converted into the typed version of Indigo, that is to say, IndigoState.

You can take a look at the details of this conversion in the Indigo.Compilation module, that utilizes an additional datatype, SomeIndigoState, that basically hides the type of the output stack. The idea of this conversion is straightforward: by having the input stack type and structure of Program, we can reconstruct the output stack type, by sequentially gluing IndigoState statements corresponding to StatementF constructors.

The main reason why this possible is that every statement doesn't depend on a specific input stack type, and can be executed against any stack.

Basically, IndigoM monad is a frontend for the Indigo language exposed to the user, and this frontend representation is compiled to the internal, strictly typed, IndigoState monad.

This approach makes it possible to perform optimization behind the scene. The only thing that remains to be mentioned is that IndigoContract param storage is just a type synonym for Var param -> IndigoM ().