REPL – interactive shell for Sophia!

Hi all!
I am glad to announce that the first version of Sophia REPL has been released: check it out on github!

What is it

REPL is an acronym for “read-eval-print loop”. As it says, it is a program that reads an expression or a query, evaluates it, prints out the result… and so on. For instance, if you type python or erl in your system console you will see the REPLs of respectively Python and Erlang.

REPLs are extremely useful for quick checking of some properties of the programs, language features, the syntax, types and many other things. They are very good mates for people that are learning new language and want to quickly try out the basic concepts.
Btw, do you remember the order of arguments of Oracle.register or are you sure about how does Func.recur combinator work? I don’t. But with this awesome tool we can vanish our doubts in a while!

More detailed overview / tutorial

How does it work

The setup instructions and full usage documentation are in the README on github.

After the successful build you need to start the service by provided aerepl_server start executable and from this point you can connect to it using aerepl script. Voilà!

    ____
   / __ | ,             _     _
  / / |_|  )           | |   (_)
 ( (_____,-` ___  _ __ | |__  _  __ _
  \______ \ / _ \| '_ \| '_ \| |/ _` |
  ,-`    ) ) (_) ) |_) ) | | | | (_| |
 (  ____/ / \___/| .__/|_| |_|_|\__,_|
  `(_____/       | |
                 |_|  interactive

The REPL works nicely as a calculator, try some expressions:

AESO> 2 + 2 * 2
6
AESO> String.concat("hello", " Sophia!")
"hello Sophia!"
AESO> (2 + 3)^2 == 2^2 + 3^2
false

You can type multiline queries as well. This requires surrounding the expression with :{ and :} braces, just like in GHCi:

AESO> :{
| let x = 2 + 2
| if(x > 0) 10
| elif(x < 0) 12
| else 11
| :}
10

Variables and functions

You can define and save your own values and functions:

AESO> let x = 2 + 2
AESO> let y = x + x
AESO> function f(z) = z + x + y
AESO> x
4
AESO> y
8
AESO> f(16)
28

You remember that in Sophia values are immutable, right? That means there is no possibility to change in-place any variables (beside the state). This rule applies to the REPL as well. Each successive redefinition of a name fill shadow the previous ones, but all of the already existing definitions will not see the change. Check out the example:

AESO> let x = 2
AESO> function f() = x
AESO> let x = x + 1
AESO> function g() = x
AESO> f()
2
AESO> g()
3

See? At first x = 2 and the f function is said to return it. After that we define the new x with value x + 1 which is a completely different object (note that this definition uses the previous x, it is not recursive). Now, while g returns the “new” x that has value of 3, the f still sees only the “old” x. Why is that? Imagine following scenario:

AESO> let x = 2
AESO> function f(y) = x + y
AESO> f(10)
12
AESO> let x = "Adam Malysz"
AESO> f(10)
...?

If f was following the trends and used the “new” x it would clearly become ill-typed. Indeed, what is "Adam Malysz" + 10? This behavior is called “static variable binding” – meaning that functions use the context from the place they were defined. The opposite, “dynamic binding” would make functions use variables from where they were called instead.

Typechecking

So, what was the order of arguments for Oracle.register? Just use the :type query, or simply :t:

AESO> :t Oracle.register
(signature : bytes(64), address, int, Chain.ttl) =>
  oracle('a, 'b)

Now we see that it takes a named argument signature, some address (probably of the oracle? ((actually this is true))), some int (a fee), and ttl (which obviously defines the lifetime of the registered oracle).
Type information is an extremely useful feedback – it can not only describe the domain of an expression, but also gives some suggestions on what is the function doing. More visualizing example:

AESO> include "Triple.aes"
Registered include Triple.aes
AESO> :t Triple.rotr
(('a * 'b * 'c)) => ('c * 'a * 'b)

This gives us a clear image of what is the purpose of Triple.rotr. It stands for “rotate right a 3-tuple” which comes pretty obviously from the type. In this simple case we don’t need to test the runtime at all to understand what is this function supposed to do.

Playing with state

The REPL can track its own state, just like real contracts! The default is unit, which can be ensured by :type query:

AESO> :t state
unit

Note that state expression will not print anything, as the () is not displayed by default. This behavior can be changed by setting display-unit option to true.

To set the state you should use :set state command along with the desired initial value (not a type!). The type will be automatically guessed. Note that queries like datatype state = Yes | No will not affect the in-REPL state. Example:

AESO> :set state 0
AESO> :t state
int
AESO> state
0
AESO> function f() = put(state + 1)
ERROR
1:16:Cannot reference stateful function put (at line 1, column 16)
in the definition of non-stateful function f.

AESO> stateful function f() = put(state + 1)
AESO> f()
AESO> state
1

Yeah, don’t forget about stateful annotation. The regular query can alter the state of course:

AESO> put(10)
AESO> state
10

This is the exceptional case where f cannot use the “old” state value like it does with the let definitions – we want f to stay updated with the state, just like it takes place in smart contracts. Because of this if you try to redefine the state (especially giving it a different type) the f would become ill-typed. Therefore, the REPL will try to remove it and ask you if you are okay with it.

AESO> stateful function f() = put(state + 1)
AESO> :set state true
This will require removing following entities: f. Proceed? [y]n
? y
AESO> f()
ERROR
1:1:Unbound variable f at line 1, column 1

Traps of custom types

You can define your own datatypes and records, along with type aliases in the REPL. To keep the integrity of the defined values during type shadowing there is a mechanism that covers custom types under TYPEDEF_x namespaces. This is used to prevent situations where some variable has a type of d and after that the d becomes redefined to be incompatible with the value. Also, it prevents unwanted comparisons between types that seem to share constructors:

AESO> datatype d = D
AESO> let x = D
AESO> datatype d = D | E 
AESO> x
D
AESO> D
D
AESO> x == D
ERROR
REPL:0:0:Cannot unify TYPEDEF_5.d
         and TYPEDEF_7.d
...
AESO> :t x
TYPEDEF_5.d
AESO> :t D
TYPEDEF_7.d

Tracking contracts and virtual deploy

The REPL is actually keeping its own blockchain behind the scenes, so nothing stops you from deploying your contracts there! This can be done via :deploy command which takes a file with the contract and optionally a name of the deployed instance (if not provided it will infer it from the name of the declaration).

// File c.aes
contract C =                         
  type state = int                   
  entrypoint init() = 0              
  entrypoint get() = state           
  stateful entrypoint inc() =        
    put(state + 1)
AESO> :deploy c.aes
c : C was successfully deployed
AESO> :deploy c.aes as con
con : C was successfully deployed
AESO> c.get()
0
AESO> con.inc()
AESO> con.inc()
AESO> con.get()
2

The token flow requires a bit of tweaking, but should work as well. Remember about the gas costs.

// file d.aes
payable contract D =                 
  payable entrypoint pay() = ()      
  stateful entrypoint take() =       
    Chain.spend( Call.caller         
               , Contract.balance    
               )
AESO> :d d.aes
d : D was successfully deployed
AESO> :set call-value 1000
AESO> d.pay(value = 500)
AESO> :set call-value 0
AESO> Chain.balance(d.address)
500
AESO> d.take()
AESO> Chain.balance(d.address)
0

I would be glad for any suggestions, bug reports, comments (both positive and negative) and I will happily answer all questions. I hope this tool will help you with the smart contract development and will make the learning process much more fun :slight_smile:

If you enjoy the project, remember to star it on github!

9 Likes