Previous | Contents | Next

NOTE: This tutorial describes an old version of Idris. For an up to date tutorial, see here.

Do notation and Idioms

Edwin Brady

Do notation | Idioms

This part of the tutorial describes some higher level syntactic sugar, for writing programs involving sequencing (do notation) and application (idioms) of data types.

Do notation

Recall that when we write I/O programs we use do notation to sequence the side-effecting operations:

greet : IO ();
greet = do { putStr "What is your name? ";
             name <- getStr;
             putStrLn ("Hello " ++ name);
           };

In fact do notation is merely syntactic sugar, which expands to applications of the following bind function, which executes an action then feeds the output to the next action:

bind : IO a -> (a -> IO b) -> IO b;

The above greet function could also be written with bind explicitly:

greet : IO ();
greet =      bind (putStr "What is your name? ")
      (\x => bind  getStr
   (\name =>       putStrLn ("Hello " ++ name)));

Clearly, the do notation is much easier to read, and it is much clearer what is going on! Conveniently, therefore, do notation can be rebound to work with types other than IO - any type T for which there can be bind and return operations, with the following types:

T_bind   : T a -> (a -> T b) -> T b;
T_return : a -> T a;

For example, we can write a bind operation for Maybe as follows:

maybeBind : Maybe a -> (a -> Maybe b) -> Maybe b;
maybeBind Nothing  mf = Nothing;
maybeBind (Just xmf = mf x;

For the return operation, we can use Just. We can use these inside a do block by a do using declaration, which takes the bind and return operations as parameters. For example, a function which adds two Maybe Ints:

do using (maybeBindJust) {
   m_add : Maybe Int -> Maybe Int -> Maybe Int;
   m_add x y = do { x' <- x-- Extract value from x
                    y' <- y-- Extract value from y
                    return (x' + y'); -- Add them 
                  };
}

This function will extract the values from x and y, if they are available, or return Nothing if they are not. Managing the Nothing cases is achieved by maybeBind, hidden by the do notation.

Idrism_add (Just 20) (Just 22)
Just 42 : Maybe Int

Idrism_add (Just 20) Nothing
Nothing : Maybe Int

Haskell programmers will probably have wanted this section to include the word 'monad', so there it was. Any others may feel free not to worry :-).

Idioms

While do notation gives an alternative meaning to sequencing, idioms give an alternative meaning to application. The notation and larger example in this section is inspired by Conor McBride and Ross Paterson's paper "Applicative Programming with Effects".

First, let us revisit m_add above. All it's really doing is applying an operator to two values extracted from Maybe Ints. We could abstract out the application:

m_app : Maybe (a->b) -> Maybe a -> Maybe b;
m_app (Just f) (Just a) = Just (f a);
m_app _        _        = Nothing;

Using this, we can write an alternative m_add which uses this alternative notion of function application, with explicit calls to m_app:

m_add' : Maybe Int -> Maybe Int -> Maybe Int;
m_add' x y = m_app (m_app (Just (+)) xy;

Rather than having to insert m_app everywhere there is an application, we can use idiom brackets to do the job for us. The idiom keyword takes two parameters, the first explaining what to do with pure values, the second being the application function.

idiom (Justm_app) {
  m_add' : Maybe Int -> Maybe Int -> Maybe Int;
  m_add' x y = [| x + y |];
}

Any type T can be used in this way, given pure and apply functions with types of the following form:

T_pure : a -> T a;
T_apply : T (a->b) -> T a -> T b;

An error-handling interpreter

Idiom notation is commonly useful when defining evaluators. McBride and Paterson describe such an evaluator, for a language similar to the following:

data Expr = Var String      -- variables
          | Val Int         -- values
          | Add Expr Expr;  -- addition

Expressions in this language are evaluated with respect to an environment, mapping Strings to Int values. We can use a list of pairs for this, and write a fetch function to retrieve the value. This may fail, so it returns a Maybe Int:

fetch : String -> List (String & Int) -> Maybe Int;
fetch x (Cons (v,valxswith strEq x v {
    | True = Just val;
    | False = fetch x xs;
}
fetch x Nil = Nothing;

It is convenient to define a type synonym for environments. Type synonyms are just functions:

Env = List (String & Int);

Now we'd like to evaluate things which might fail, which carry an environment, without the noise usually associated with this. Enter the idiom brackets... We'll take our idiom to be Env -> Maybe a.

First, we need to know how to inject pure values into this idiom:

pure : a -> Env -> Maybe a;
pure x e = Just x;

Then we need to know how to apply things which carry an environment and might fail:

ap : (Env -> Maybe (a -> b)) -> (Env -> Maybe a) -> (Env -> Maybe b);
ap f g x with (f xg x) {
   | (Just fxJust gx) = Just (fx gx);
   | _ = Nothing;
}

Finally, we write the evaluator which can use idiom brackets to evaluate things clearly in this idiom:

idiom (pureap) {
      eval : Expr -> Env -> Maybe Int;
      eval (Var x)   = fetch x;
      eval (Val x)   = [| x |];
      eval (Add x y) = [| eval x + eval y |];
}

We'll set up a simple environment to test the evaluator, and try a couple of expressions. testExpr1 will succeed, but testExpr2 will fail due to using an undefined variable:

testEnv = Cons ("x", 42) (Cons ("y", 6) Nil);

testExpr1 = Add (Var "x") (Var "y");
testExpr2 = Add (Var "x") (Var "z");


Idriseval testExpr1 testEnv
Just 48 : Maybe Int
Idriseval testExpr2 testEnv
Nothing : Maybe Int

And without the idiom brackets...?

To properly appreciate the value of idiom brackets, it's worth seeing what the definition would have looked like without them. The most obvious way uses with to extract the values from the intermediate evaluations:

eval : Expr -> Env -> Maybe Int;
eval (Var x)   g = fetch x g;
eval (Val x)   g = Just x;
eval (Add x yg with (eval x geval y g) {
   | (Just x'Just y') = Just (x'+y');
   | _ = Nothing;

The situation improves slightly with do notation:

do using (maybeBindJust) {
   eval : Expr -> Env -> Maybe Int;
   eval (Var x)   g = fetch x g;
   eval (Val x)   g = return x;
   eval (Add x yg = do { x' <- eval x g;
                           y' <- eval y g;
                           return (x'+y'); };
}


Source for this chapter

Previous | Contents | Next