[#90] update Indigo README and add a tutorial

Problem: Indigo documentation is outdated and was written for internal
use only. It would be better to have a newcomers-frienly tutorial that
also introduces concepts for developers.

Solution: create a tutorial with examples that is easy to follow and
contains (updated) information from the old README.
Provide then a simpler README that refers to the tutorial.
Additionally, add printing and type synonyms that help Indigo usage.
parent 492e5b5f
Pipeline #127751790 passed with stages
in 8 minutes and 9 seconds
......@@ -95,6 +95,17 @@
- ingredients
- main
- package:
- name: indigo-tutorial
- section:
- name: library
- message:
- name: Redundant build-depends entry
- depends:
- base-noprelude
- indigo
- morley-prelude
- package:
- name: morley-ledgers
- section:
......
......@@ -4,6 +4,7 @@ with-compiler: ghc-8.6.5
packages:
code/indigo/
, code/indigo/tutorial/
, code/lorentz/
, code/morley/
, code/morley-client/
......
......@@ -18,6 +18,7 @@ rec {
# we need to know subdirectories to make weeder stuff work
local-packages = [
{ name = "indigo"; subdirectory = "code/indigo"; }
{ name = "indigo-tutorial"; subdirectory = "code/indigo/tutorial"; }
{ name = "lorentz"; subdirectory = "code/lorentz"; }
{ name = "morley"; subdirectory = "code/morley"; }
{ name = "morley-client"; subdirectory = "code/morley-client"; }
......
# Indigo eDSL
Indigo eDSL is a high level language over Lorentz.
The main feature of the language is that it supports variables
and that you are freed from the burden of manual stack management.
You can construct expression using variables and constants within them
and they will be compiled to Lorentz.
Indigo eDSL is a high level language for Michelson contract development.
It is meant first and foremost to free you from the burden of manual stack
management and supports common features of imperative languages.
Also the language supports all typical imperative statements like If, While, For, etc.
Variables are destroyed when you leave a scope, like in any other imperative languages.
It is built on top of `Lorentz`, which in turn is built on top of `Morley`, a
dialect that is a superset of vanilla Michelson.
If you are interested more in the relationships between these projects you can
start by taking a look at [Morley's README](../../README.md).
## Overall idea
The main motivation to create this eDSL was the burden of manual stack management in Lorentz.
When writing contracts code in Lorentz you have access to the typed stack
which is basically an Haskell heterogeneous list. The repetitive pattern during
this process is to store a bunch of values at the end of the stack and copy the
required ones on the top of the stack when you have to operate with them.
Sometimes a developer can leverage other tricks, but the described one seemed
to be most common to me.
Michelson contracts are stack-based and often follow the repetitive pattern of
copying the required values on top of the stack to apply an instruction to them.
Indigo can associate variables to values in the stack and it's able to refer to
them in order to handle this pattern automatically.
So, Indigo is just called up to handle this routine in a similar way, namely,
storing values at the top of the stack with ability to refer to them via variables.
Each variable has its own index and can be found in the stack using this index.
In addition to this it can override existing variables with new values, allowing
the manipulation of the stack to be automatic.
## IndigoM monad
The basic idea for Indigo is straightforward.
We just want to have a state monad that stores a list which corresponds
to the stack. Each element of the list is the index of a variable which
refers to this corresponding stack element.
Also, it would be nice to store the number of variables that have been already
allocated so far, to be able to assign to a following variable the next index
which hasn't been already used.
Leveraging this ability, it also supports features such as: imperative statements
(`if`, `while`, ...), expressions, operators (`+`, `||`, `==`, ...), scoped
functions definition and errors.
As we go with explanation, I can give some snippet of Haskell code.
Indigo uses Morley to map values from Michelson to Haskell and to compile to
Michelson code (or to any of the other projects in the chain mentioned above).
```haskell
newtype Var = Var Word
## Tutorial and documentation
data StkEl
= NoRef
| Ref Var
Indigo has a tutorial that you can find [here](tutorial/).
newtype IndigoM a = IndigoM (State ([StkEl], Word) a)
```
This code could probably work, but it has two main disadvantages:
* It's not strong typed. We have the strong typed Lorentz stack but this `IndigoM`
doesn't ensure any of these type level invariants which Lorentz provides.
* It is not connected to the real Lorentz code at all.
Strictly speaking we could return Lorentz code as result of an execution of this monad,
and then glue result of two sequent results, but again, it's very fragile
(from the perspective of types).
Let's bring more type safety here.
First of all, let's make `Var` typed:
```haskell
newtype Var a = Var Word
```
You can see that `Var` has a phantom type parameter which is the type
of the stack element where a variable refer to.
Then let's propagate this change to `StkEl`
```haskell
data StkEl a
= TypeValue a => NoRef
| TypeValue a => Ref (Var a)
```
(don't pay attention to the `TypeValue a` constraint at this stage,
it's a minor detail and will be explained in the next chapter).
Now let's define the heterogeneous list of `StkEl`
```haskell
type StackVars (stk :: [Kind.Type]) = Rec StkEl stk
```
So we got the following definition of `IndigoM`:
```haskell
newtype IndigoM stk a = IndigoM (State (StackVars stk, Word) a)
```
But now, if we try to connect two sequent expressions having `IndigoM` type via `>>=`,
we'll be obliged to provide an expression with the same `stk`, however, the second
one actually has a `stk` which depends on the result type of the first expression.
So, ideally, we would like to have such `IndigoM` which is akin to the `State` monad
described above that also has an input and an output stack types as its type parameters.
Something like this
```haskell
newtype IndigoM inp out a = ...
```
and then the bind operator would have a type like this:
```haskell
(>>=) :: IndigoM inp out a -> (a -> IndigoM out out1 b) -> IndigoM inp out1 b
```
so such bind operator would glue two expressions with matched types.
But the problem is that it's already not the bind for ordinary `State`,
also this bind doesn't match the bind from the `Monad` type class.
Fortunately, there is such thing called
[indexed monad](http://hackage.haskell.org/package/category-extras-0.53.1/docs/Control-Monad-Indexed-State.html#t:IxState).
Its definition looks like this:
```haskell
newtype IxState i j a = IxState { runIxState :: i -> (a, j) }
```
and it's basically a `State` monad that returns the state of a new type everytime.
Let's get closer to our case, and introduce substitute specific types to this
definition to build the final version of our `IndigoM` monad:
```haskell
newtype IndigoM inp out a = IndigoM { runIndigoM :: (StackVars inp, Word) -> (StackVars out, Word, inp :-> out) }
```
Although it may look scary it's basically a state monad that consumes
the references on the stack and the number of allocated variables and returns
new references, the increased number of allocated variables and the Lorentz code
generated in result of the execution.
You can get more details in this [module](src/Indigo/State.hs), where
`MetaData` is a consuming tuple and `GenCode` is a resulting one.
Also, in this module you can see the definition of the `>>=` operator which
together with the `RebindableSyntax` extension can be used in `do` syntax, what
makes the code really neat.
However, all this definitions are sligtly different, the reason will be explained
later on.
## Variables and expression evaluation
Now, when we got so solid strong typed construction let's try to examine it further
and describe some basic operations.
Let's try to come up with an assignment operator:
a function that would create a new variable from some expression.
An expression is as usual something that can go on the right hand of an assignment.
Let's define a simple `Expr` datatype with three basic constructors:
```haskell
data Expr a where
C :: a -> Expr a
V :: Var a -> Expr a
Add :: Expr Int -> Expr Int -> Expr Int
```
First of them creates an expression from a constant, the second from a variable
and the last one is for additions of two expressions of `Int` type.
Let's define a function that will compile `Expr` to Lorentz code, which computes
the value of the passed expression and leaves it on the top of the stack:
```haskell
compileExpr :: Expr a -> IndigoM inp (a & inp) ()
```
It'll have this type because in result of the execution we'll have
an expression of type `a` on the top of the stack.
Let's define it step by step, explaining the definition for each constructor:
```haskell
compileExpr (C a) = do
md <- iget
iput $ GenCode (pushNoRefMd md) (push a)
```
First of all, notice that we use the `do` syntax which comes from `RebindableSyntax`
extension for `IndigoM`.
In the first line of this function we just get current state (which has type `MetaData`),
in the second line we construct a `GenCode` datatype which is the resulting type.
`GenCode` consists of a `MetaData` and the generated Lorentz code.
The generated code will be just a Lorentz `push` instruction, `pushNoRefMd`
hasn't been defined yet.
However, it just push a `NoRef` of type `StkEl a` on the top of the stack
to satisfy the output type of the stack `a & inp`.
The next step is the `Add` constructor:
```haskell
compileExpr (Add e1 e2) = do
compileExpr e2
compileExpr e1
IndigoM $ \md -> ((), GenCode (pushNoRefMd $ popNoRefMd $ popNoRefMd md) add)
```
The first two lines are straightforward, we just call `compileExpr` recursively
for the operands of `Add`.
The last line looks a little bit trickier, but basically it drops two ints from
the top and adds one as a result.
And the last and hardest step, the implementation for a variable:
```haskell
compileExpr (V a) = do
md@(MetaData s _) <- iget
iput $ GenCode (pushNoRefMd md) (lookupVar a s)
```
Firstly, it's better to realise the logic behind this code.
As stated above, the main idea is that we assign each variable an index
and mark each element of the stack with an index of a variable which refers to this element.
Now it's time to bind things together.
To compute an expression that is just a variable we have to generate the Lorentz
code to `duup` the element corresponding to this variable.
This logic is implemented in this [module](src/Indigo/Lookup.hs), that exports
the function to copy the value associated to a `Var` to the top of the stack:
```haskell
varActionGet :: TypeValue a => Var a -> StackVars stk -> stk :-> a & stk
```
This function iterates over `StackVars` to find the depth of the `Var`, then
check all the required constraints (using the `TypeValue` typeclass) to use the
`duupX` Lorentz macro.
You can notice that the same module contains not only the getter
of a variable, but also the setter (code that assigns to the variable the value
on the top of the stack)
```haskell
varActionSet :: TypeValue a => Var a -> StackVars stk -> a & stk :-> stk
```
and an updater (code to update the variable using an instruction, the value at
the top of the stack and the current value of the variable itself)
```haskell
varActionUpdate
:: (TypeValue a, TypeValue b)
=> Var a
-> StackVars stk
-> '[b, a] :-> '[a]
-> (b ': stk) :-> stk
```
And the last step to write the assignment operator is to create a variable which
refers to the top of the stack where a computed expression takes place.
This can be done with a function having the type
```haskell
makeTopVar :: TypeValue x => IndigoM (x & inp) (x & inp) (Var x)
```
You can find its implementation in this [module](src/Indigo/State.hs).
In the module [Expr](src/Indigo/Expr.hs) you can also find more useful constructors
of `Expr` and their compilation to Lorentz.
## Imperative statements
The icing on the cake is the imperative statements like `if`, `while`, `assert`
and others which can be used in code in Indigo.
Let's just take `if_` from the [Language](src/Indigo/Language.hs) module and
explain its semantic.
`if_` has the following type:
```haskell
if_ :: forall inp xs ys .
=> Expr Bool
-> IndigoM inp xs ()
-> IndigoM inp ys ()
-> IndigoM inp inp ()
```
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 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 type.
This unification is obvious and comes from imperative languages, where there exist such notion
as "scope". If the execution leaves a scope all variables defined within it are destroyed.
The same thing happens here. To do so we redefine `GenCode` to also contain the
Lorentz code to return to the input stack:
```haskell
-- | Resulting state of IndigoM.
data GenCode inp out = GenCode
{ gcMeta :: ~(MetaData out)
-- ^ Interpreter meta data.
, gcCode :: inp :-> out
-- ^ Generated Lorentz code.
, gcClear :: out :-> inp
-- ^ Clearing Lorentz code.
}
```
This way, constructs like `if_` can remove the variables and types pushed by a
branch. You can see this version in the [State](src/Indigo/State.hs) module.
Pay attention to the fact that that branches return `()` as a protection from
accidentally returning a variable which refers to a non-existing stack elements
destroyed after the execution leaves the scope. It can be rewritten to return
`Expr a` if it's really needed.
Also, notice that even though the elements added to `inp` by the branches are
removed these can still directly operate with internals of `IndigoM`, spoiling
the stack and removing some references.
Such an even will cause an error when you try to evaluate a variable that refers
to a non-existing element.
Because of that it makes sense not to export functions that allow the modification
of `IndigoM`'s state directly.
## Functions and Procedures
The same concept of imperative scope is also useful when declaring indigo
functions to be called somewhere else by different Indigo code.
For this reason two type synonyms are defined in the [Language](src/Indigo/Language.hs)
module to easily identify such cases of `IndigoM`:
```haskell
type IndigoFunction s a = IndigoM s (a & s) (Var a)
type IndigoProcedure s = IndigoM s s ()
```
and to be able to create them from a generic `IndigoM` a function is defined for
each:
```haskell
defFunction :: (IsExpr ex a, TypeValue a) => IndigoM inp out ex -> IndigoFunction inp a
defProcedure :: IndigoM inp out a -> IndigoProcedure inp
```
These are simply implemented to make sure to remove the unwanted elements from
the stack after leaving the function/procedure scope (and in the case of a
function, to not keep the element associated with the returned `Expr`).
## Compilation to Lorentz
You can compile Indigo code to Lorentz one. There is a module `Indigo.Compilation`
which provides useful functionality to compile plain Indigo code to Lorentz, as well as contracts
(cleaning up all allocated variables during a contract execution).
## Examples
You can find some examples of Indigo code at this [module](test/Test/Examples.hs).
In addition, as for the other Morley projects, it has Haddock documentation.
......@@ -4,7 +4,7 @@ cabal-version: 2.2
--
-- see: https://github.com/sol/hpack
--
-- hash: 0e101be2d2109556f93099efa10e3a80cb002dfb75a8ef38760a8cc4e7b1c18f
-- hash: 72d882014eaf5bf5ae3d9898064909a43af9fe19ac9503055e572c106cdfc07d
name: indigo
version: 0.1.0.0
......@@ -41,6 +41,7 @@ library
Indigo.Lookup
Indigo.Lorentz
Indigo.Prelude
Indigo.Print
Indigo.Rebinded
Indigo.State
other-modules:
......
......@@ -10,5 +10,6 @@ import Indigo.Lib as Exports
import Indigo.Lookup as Exports
import Indigo.Lorentz as Exports
import Indigo.Prelude as Exports
import Indigo.Print as Exports
import Indigo.Rebinded as Exports
import Indigo.State as Exports
......@@ -3,6 +3,8 @@
module Indigo.Compilation
( compileIndigo
, IndigoContract
, IndigoContract'
, compileIndigoContract
, Ops
......@@ -73,6 +75,7 @@ assingVarIfOps [email protected](MetaData stk vRef) = case stk of
Just Refl -> MetaData (Ref (Var vRef) :& RNil) (vRef + 1)
-- | Compile Indigo code to Lorentz.
--
-- Note: it is necessary to specify the number of parameters (using the first
-- type variable) of the Indigo function. Also, these should be on the top of
-- the input stack in inverse order (see `IndigoWithParams`).
......@@ -92,13 +95,24 @@ type HasSideEffects = Given (Var Ops)
-- | Allows to get a variable with storage
type HasStorage st = Given (Var st)
-- | A utility type for a contract written in Indigo.
--
-- Note that is a more restrictive type than what is needed for compilation with
-- 'compileIndigoContract' and it's mainly intended to hide arbitrary outputs and
-- be similar to Lorentz's 'ContractCode'.
type IndigoContract param st = IndigoContract' param st '[param, st, Ops]
-- | Type of a contract that can be compiled to Lorentz with 'compileIndigoContract'.
type IndigoContract' param st out =
(HasStorage st, HasSideEffects) => Var param -> IndigoM '[param, st, Ops] out ()
-- | Compile Indigo code to Lorentz contract.
-- Drop elements from the stack to return only [Operation] and Storage.
compileIndigoContract
:: forall param st out .
( TypeValue param, TypeValue st
)
=> ((HasStorage st, HasSideEffects) => Var param -> IndigoM '[param, st, Ops] out ())
=> IndigoContract' param st out
-> ContractCode param st
compileIndigoContract code =
L.nil # L.swap # L.unpair #
......
......@@ -46,6 +46,7 @@ module Indigo.Language
, IndigoProcedure
, scope
, defFunction
, defContract
-- * Conversion from Lorentz
, fromLorentzFun1
......@@ -337,6 +338,13 @@ defFunction
-> IndigoFunction inp a
defFunction = scope
-- | A more specific version of 'defFunction' meant to more easily create
-- 'IndigoContract's.
defContract
:: ((HasStorage st, HasSideEffects) => IndigoM '[param, st, Ops] out ())
-> ((HasStorage st, HasSideEffects) => IndigoProcedure '[param, st, Ops])
defContract = scope
----------------------------------------------------------------------------
-- Conversion from Lorentz
----------------------------------------------------------------------------
......
-- | Module containing pretty-printing of Indigo contracts
module Indigo.Print
( printIndigoContract
, printAsMichelson
, saveAsMichelson
) where
import Indigo.Compilation
import Indigo.Lorentz
import Indigo.Prelude
import Indigo.State
-- | Pretty-print an Indigo contract into Michelson code.
printIndigoContract
:: ( TypeValue param, TypeValue st
, NiceParameterFull param, NiceStorage st
)
=> Bool -- ^ Force result to be single line
-> IndigoContract' param st out
-> LText
printIndigoContract forceSingleLine ctr = printLorentzContract forceSingleLine $
compileIndigoContract ctr
-- | Prints the pretty-printed Michelson code of an Indigo contract to
-- the standard output. This is intended to be easy to use for newcomers.
printAsMichelson
:: ( TypeValue param, TypeValue st
, NiceParameterFull param, NiceStorage st
, MonadIO m
)
=> IndigoContract' param st out
-> m ()
printAsMichelson contract = putStrLn (printIndigoContract False contract)
-- | Saves the pretty-printed Michelson code of an Indigo contract to
-- the given file. This is intended to be easy to use for newcomers.
saveAsMichelson
:: ( TypeValue param, TypeValue st
, NiceParameterFull param, NiceStorage st
, MonadIO m, MonadMask m
)
=> IndigoContract' param st out
-> FilePath
-> m ()
saveAsMichelson contract filePath =
withFile filePath WriteMode (`hPutStrLn` printIndigoContract False contract)
This diff is collapsed.
.PHONY: indigo-tutorial haddock haddock-no-deps clean
# Build target from the common utility Makefile
MAKEU = $(MAKE) -f ../make/Makefile
MAKE_PACKAGE = $(MAKEU) PACKAGE=indigo-tutorial
indigo-tutorial:
$(MAKE_PACKAGE) dev
haddock:
$(MAKE_PACKAGE) haddock
haddock-no-deps:
$(MAKE_PACKAGE) haddock-no-deps
clean:
$(MAKE_PACKAGE) clean
# Indigo Tutorial
This is a tutorial for [Indigo eDSL](../).
It aims to be accessible to as many people as possible, but also contains more
technical information for Haskell developers that are interested in learning more.
## Tutorial index
- [00 - Getting started](src/Indigo/Tutorial/00)
- [01 - Basics and Variables](src/Indigo/Tutorial/01)
- [02 - Expressions and operators](src/Indigo/Tutorial/02)
- [03 - Imperative statements](src/Indigo/Tutorial/03)
- [04 - Functions and Procedures](src/Indigo/Tutorial/04)
- [05 - Side Effects and Errors](src/Indigo/Tutorial/05)
- [Appendix A: types](src/Indigo/Tutorial/AA.md)
- [Appendix B: expressions](src/Indigo/Tutorial/AB.md)
cabal-version: 2.2
-- This file has been generated from package.yaml by hpack version 0.33.0.
--
-- see: https://github.com/sol/hpack
--
-- hash: 9d191454ebdf78b3a44fa68cc18f2237e285b9c28b5948feb83c9314ae26f4a7
name: indigo-tutorial
version: 0.1.0.0
synopsis: Tutorial for Indigo eDSL.
description: Tutorial for Indigo eDSL.
category: Language
homepage: https://gitlab.com/morley-framework/morley
bug-reports: https://gitlab.com/morley-framework/morley/issues
author: Serokell, Tocqueville Group
maintainer: Serokell <[email protected]>
copyright: 2019-2020 Tocqueville Group
license: AGPL-3.0-or-later
license-file: LICENSE
build-type: Simple
extra-source-files:
README.md
src/Indigo/Tutorial/00/index.md
src/Indigo/Tutorial/01/index.md
src/Indigo/Tutorial/02/index.md
src/Indigo/Tutorial/03/index.md
src/Indigo/Tutorial/04/index.md
src/Indigo/Tutorial/05/index.md
src/Indigo/Tutorial/AA.md
src/Indigo/Tutorial/AB.md
source-repository head
type: git
location: [email protected]:morley-framework/morley.git
library
other-modules:
Paths_indigo_tutorial
autogen-modules:
Paths_indigo_tutorial
hs-source-dirs:
src
default-extensions: ApplicativeDo AllowAmbiguousTypes BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MonadFailDesugaring MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances ViewPatterns DeriveAnyClass DerivingStrategies NoApplicativeDo RebindableSyntax
ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-unused-do-bind
build-depends:
base-noprelude >=4.7 && <5
, indigo
, morley-prelude
default-language: Haskell2010
<<: !include "../hpack/module.yaml"
<<: *meta
name: indigo-tutorial
version: 0.1.0.0
synopsis: Tutorial for Indigo eDSL.
author: Serokell, Tocqueville Group
copyright: 2019-2020 Tocqueville Group
description: Tutorial for Indigo eDSL.
category: Language
extra-source-files: