An Idris metaprogramming “hello world”
By: . Published: . Categories: idris-lang dependent-types walkthrough.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:
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 namestring
. 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:
> 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:
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:
> 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
:
*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:
*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:
*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:
*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:
-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…
-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?
-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
?
-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:
-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
?
-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
:
-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:
-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:
-HoleyHead.holeThatWasTheEmptyString> solve
holeThatWasTheEmptyString: No more goals.
And victoriously exit the elaborator shell:
-HoleyHead.holeThatWasTheEmptyString> :qed
Proof completed!
HoleyHead.holeThatWasTheEmptyString = %runElab (do intro'
fill (RConstant (Str ""))
solve)
*HoleyHead *Language/Reflection/Elab>
Let’s give it a go:
*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:
-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:
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:
> 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:
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 thanintro'
). - 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:
> :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:
fill (quote "")
Even sweeter, we can use Lisp-like quotation syntax to write this with even less typing as:
fill `("")