Jeremy W. Sherman

stay a while, and listen

An Idris metaprogramming "hello world"

Idris is a programming language with dependent types. Like any civilized language, it has metaprogramming support; its REPL even supports interactively crafting metaprograms by employing tactic functions.

Let’s walk through a small example that covers the bases of interactive metaprogramming.

This article is an elaboration of a gist I posted a few days ago.

A Simple Function

Here’s a simple program that take a list of strings and returns either the first string in the list or the empty string when the list is empty:

1
2
3
4
5
6
7
8
9
10
module Head

firstStringOrEmpty : List String -> String
firstStringOrEmpty strings =
    case strings of
        Nil =>
            ""

        string :: _ =>
            string

This function pattern matches on the strings argument to see if it is the empty list Nil or a list with at least one item:

  • In the Nil case, it evaluates to the empty string "".
  • In the non-Nil case, the first item is bound to the new name string. It ignores the rest of the list by binding it to the nameless name _. It then evaluates to that first item, string.

Here’s what it looks like in practice by firing up the REPL:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
> idris Head.idr
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.9.19
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
*Head> firstStringOrEmpty []
"" : String
*Head> firstStringOrEmpty ["a"]
"a" : String
*Head> firstStringOrEmpty ["a", "b", "c"]
"a" : String

(In future examples, I’ll be omitting the banner with --nobanner, but I figure it’s useful to see what version I was working with.)

Poking a Hole in It

Now that we know what we want the function to look like, let’s poke a hole in it!

Idris represents holes as names with a leading question mark, like ?hole. Let’s replace the Nil case with a hole:

1
2
3
4
5
6
7
8
9
10
module HoleyHead

firstStringOrEmpty : List String -> String
firstStringOrEmpty strings =
    case strings of
        Nil =>
            ?holeThatWasTheEmptyString

        string :: _ =>
            string

Now let’s see what the REPL has to say:

1
2
3
> idris --nobanner HoleyHead.idr
Type checking ./HoleyHead.idr
Holes: HoleyHead.holeThatWasTheEmptyString

Would you look at that! It found our hole.

Filling the Hole with Elaborator Reflection

We know what we want this to look like, since we started with a working program and then poked a hole in it, but let’s humor this example and pretend we need Idris’s help to figure out how to fill it in.

Import Elaboration Scripts

Start by pulling in the elaboration scripts provided by the system in the module Language.Reflection.Elab:

1
2
3
*HoleyHead> :module Language.Reflection.Elab
Holes: HoleyHead.holeThatWasTheEmptyString
*HoleyHead *Language/Reflection/Elab>

Notice how the prompt changed to reflect the added module.

Survey Your Tools

The good stuff in Language.Reflection.Elab lives in the Tactics module. Take a look at the fun stuff in there:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
*HoleyHead *Language/Reflection/Elab> :browse Language.Reflection.Elab.Tactics
Namespaces:

Names:
  addInstance : TTName -> TTName -> Elab ()
  apply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))
  attack : Elab ()
  check : Raw -> Elab (TT, TT)
  claim : TTName -> Raw -> Elab ()
… [list abbreviated to save you scrolling] …
  solve : Elab ()
  sourceLocation : Elab ()
  unfocus : TTName -> Elab ()
  whnf : TT -> Elab TT

These are the functions we’ll be using to fill the hole. Each of these has a docstring with more info about it. For example, here’s one we’ll use in a bit:

1
2
3
4
5
6
7
*HoleyHead *Language/Reflection/Elab> :doc intro'
Language.Reflection.Elab.Tactics.intro' : Elab ()
    Introduce a lambda binding around the current hole and focus on
    the body, using the name provided by the type of the hole.

    The function is Total
Holes: HoleyHead.holeThatWasTheEmptyString

Translated into plainer English, this says that intro' transforms a hole like ?hole into a function _ => ?newHole and points you at filling in the new hole.

(That line at the end of the docstring about “The function is Total” represents the judgment of Idris’s totality checker. A total function is one that terminates for all its inputs, which means it eventually returns a value for each and every one and cannot run forever.)

Gotcha

We’re taking a peek now, because unfortunately, we won’t be able to run :browse while we’re working on filling the hole, short of firing up a new REPL. We will be able to run :doc still, so we can just scroll back to this list as needed.

Enter the Elaborator Shell

Enter the interactive elaborator shell by issuing the :elab <HOLE> command:

1
2
3
4
5
6
*HoleyHead *Language/Reflection/Elab> :elab holeThatWasTheEmptyString


----------                 Goal:                  ----------
{hole0} : List String -> String
-HoleyHead.holeThatWasTheEmptyString>

When you first enter the elaboration shell, it prints the current elaboration state, with the goal – the term you’re trying to fill using elaboration scripts – shown below the line, and any other remaining goals shown above the line. You can review this state at any time by issuing the :state command. To get a list of available commands, run :help.

The elaborator shell has its own prompt, which tells you the hole you’re working on filling.

Reach Your Goals

Our current goal is hole0, and it has type List String -> String. This reflects that we currently have in scope – and available to our hole-filling efforts – a List String, in the form of the strings argument to our function, and that the type of whatever we compute using this context must end up as String.

In light of this List String -> String phrasing, what we had filling this space before was a constant function \strings => "" that ignored its arguments and always returned the empty string.

Since we don’t actually care about the name of the function argument, let’s use that intro' tactic function we saw earlier:

1
2
3
4
5
6
7
8
9
10
11
-HoleyHead.holeThatWasTheEmptyString> :state


----------                 Goal:                  ----------
{hole0} : List String -> String
-HoleyHead.holeThatWasTheEmptyString> intro'

----------              Assumptions:              ----------
----------                 Goal:                  ----------
{hole0} : String
-HoleyHead.holeThatWasTheEmptyString>

Filling a Hole

Cool, now all we need to do is provide a String to fill the hole with. What could we use to do that? Well…

1
2
3
4
5
-HoleyHead.holeThatWasTheEmptyString> :doc fill
Language.Reflection.Elab.Tactics.fill : Raw -> Elab ()
    Place a term into a hole, unifying its type

    The function is Total

That fill function looks like exactly what we need if we’re to put "" back in that hole. Maybe we can just fill "" directly?

1
2
3
4
5
6
7
-HoleyHead.holeThatWasTheEmptyString> fill ""
(input):1:6:When checking an application of function
Language.Reflection.Elab.Tactics.fill:
        Type mismatch between
                String (Type of "")
        and
                Raw (Expected type)

Welp, that didn’t quite do it.

Chasing Down Constructors

We need a way to turn the string "" into a Raw value. What’s a Raw?

1
2
3
-HoleyHead.holeThatWasTheEmptyString> :type Raw
FFI_C.Raw : Type -> Type
Language.Reflection.Raw : Type

Looks like there are a couple kinds of Raw around, but one is a Raw someType and the other is just a Raw. Plus, we’re not doing FFI, so let’s bet on the Language.Reflection.Raw. Let’s pull the docs on that:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
-HoleyHead.holeThatWasTheEmptyString> :doc Language.Reflection.Raw
Data type Language.Reflection.Raw : Type
    Raw terms without types

Constructors:
    Var : TTName -> Raw
        Variables, global or local

    RBind : TTName -> Binder Raw -> Raw -> Raw
        Bind a variable

    RApp : Raw -> Raw -> Raw
        Application

    RType : Raw
        The type of types

    RUType : Universe -> Raw


    RForce : Raw -> Raw


    RConstant : Const -> Raw
        Embed a constant

"" is a string constant, so RConstant sounds like what we want.

In order to create an RConstant, we need to pass it a Const. What’s a Const?

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
-HoleyHead.holeThatWasTheEmptyString> :doc Const
Data type Language.Reflection.Const : Type
    Primitive constants

Constructors:
    I : Int -> Const


    BI : Integer -> Const


    Fl : Double -> Const


    Ch : Char -> Const


    Str : String -> Const


    B8 : Bits8 -> Const


    B16 : Bits16 -> Const


    B32 : Bits32 -> Const


    B64 : Bits64 -> Const


    AType : ArithTy -> Const


    StrType : Const


    VoidType : Const


    Forgot : Const


    WorldType : Const


    TheWorld : Const

Bingo! Str "" will give us a Const, and then we can pass that to RConstant to get a Raw, and then we can pass that to fill:

1
2
3
4
5
-HoleyHead.holeThatWasTheEmptyString> fill (RConstant (Str ""))

----------              Assumptions:              ----------
----------                 Goal:                  ----------
{hole0} : String =?= ""

Solve et Coagulum

We’re sitting with one last goal, to show that our guess "" really is a String. If you take a peek at the docs, you’d see that solve does just this:

1
2
3
4
5
-HoleyHead.holeThatWasTheEmptyString> :doc solve
Language.Reflection.Elab.Tactics.solve : Elab ()
    Substitute a guess into a hole.

    The function is Total

(You could also find solve by running :search Elab () – all our tactics return a value in Elab, we have no inputs to provide, and we just want to trigger the side effect of finishing this up – and looking through the few lines of output to find a likely candidate. But peeping at the docs is faster.)

So let’s use it:

1
2
-HoleyHead.holeThatWasTheEmptyString> solve
holeThatWasTheEmptyString: No more goals.

And victoriously exit the elaborator shell:

1
2
3
4
5
6
-HoleyHead.holeThatWasTheEmptyString> :qed
Proof completed!
HoleyHead.holeThatWasTheEmptyString = %runElab (do intro'
                                                   fill (RConstant (Str ""))
                                                   solve)
*HoleyHead *Language/Reflection/Elab>

Let’s give it a go:

1
2
*HoleyHead *Language/Reflection/Elab> firstStringOrEmpty []
"" : String

It worked!

Paste In the Script

When we left the shell with :qed, it wrote out a function definition:

1
2
3
4
5
-HoleyHead.holeThatWasTheEmptyString> :qed
Proof completed!
HoleyHead.holeThatWasTheEmptyString = %runElab (do intro'
                                                   fill (RConstant (Str ""))
                                                   solve)

Copy and paste this into the code, and it will fill the hole when the code is compiled, just like we did interactively at the REPL:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
module HoleyHead

firstStringOrEmpty : List String -> String
firstStringOrEmpty strings =
    case strings of
        Nil =>
            ?holeThatWasTheEmptyString

        string :: _ =>
            string

HoleyHead.holeThatWasTheEmptyString = %runElab (do intro'
                                                   fill (RConstant (Str ""))
                                                   solve)

Fire this up in the REPL, and notice that there aren’t any unfilled holes:

1
2
3
4
5
6
7
> idris --nobanner HoleyHead.idr
Type checking ./HoleyHead.idr
HoleyHead.idr:12:37:
When checking right hand side of HoleyHead.holeThatWasTheEmptyString:
No such variable Language.Reflection.Elab.Elab
Holes: HoleyHead.holeThatWasTheEmptyString
*HoleyHead>

Oh, snap. Remember how we ran :module Language.Reflection.Elab before entering the elaboration shell? We also need to bring those names into scope in our file, too:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
module HoleyHead

import Language.Reflection.Elab

firstStringOrEmpty : List String -> String
firstStringOrEmpty strings =
    case strings of
        Nil =>
            ?holeThatWasTheEmptyString

        string :: _ =>
            string

HoleyHead.holeThatWasTheEmptyString = %runElab (do intro'
                                                   fill (RConstant (Str ""))
                                                   solve)

You can either run the :edit command at the REPL and add the import line, or edit it in your editor and ask the REPL to :reload your current file, or just exit, edit, and then run idris --nobanner <FILE> once more.

Either way, you’ve just completed your hello world!

Summary

Idris allows you to interactively build a script that generates source code at compile time by solving for a goal represented by a hole in your source code.

You’ve seen how to:

  • Represent a hole in source code using a question-mark–prefixed name like ?hole.
  • Import Language.Reflection.Elab to make the system-provide tactics available to you.
  • Enter the elaborator shell using :elab <HOLE>.
  • Get documentation on tactics using :doc <NAME>.
  • Use intro' to focus on the body of a function without naming the function’s arugment.
  • Use fill to provide a guess for a hole’s value.
  • Use solve to instantiate the guess.
  • Conclude the session with :qed to get a proof script you can paste into your file to fill the hole in future.

Challenges

Some challenges, in order of increasing difficulty:

  • Fill the hole with the string “bananas” instead of “”.
  • Name the function argument (check out intro rather than intro').
  • Replace the string result in the other case with a hole ?holeThatWasString, and interactively create an elaborator script to fill that hole.

For the More Curious: Quotation

Figuring out that whole RConstant (Str "")) bit was a pain. If you felt like Idris should have been able to do that work for you, you were right! Idris supports quoting syntax, which will seem awfully familiar if you’ve written any Lisp macros:

1
2
3
4
5
6
7
8
> :doc quote
Language.Reflection.quote : Quotable a t => a -> t
    Quote a particular element of a.

    Each equation should look something like
    quote (Foo x y) = `(Foo ~(quote x) ~(quote y))

    The function is Total

Instead of laboriously hunting down the various type constructors and then writing out fill (RConstant (Str "")), we can use quoting to do the hard work for us with:

1
fill (quote "")

Even sweeter, we can use Lisp-like quotation syntax to write this with even less typing as:

1
fill `("")