Over the last few weeks, there have been some changes to Epigram that make programming in the command-line interface slightly more pleasant. We are starting to think about a high-level language, but in the meantime, I thought it would be nice to look at what sort of programming is possible today. None of this is revolutionary or indeed particularly exciting, but it should make the exciting stuff easier to write. This post would be literate Epigram if there was such a thing; as there isn’t, you will have to copy code lines one at a time into Pig if you want to follow along.
We have been able to define data types by their constructors for some time. Behind the scenes, the data tactic is also generating a description in the universe of data types and specialising the generic induction principle.
data Bool := (false : Bool) ; (true : Bool) ;
data Nat := (zero : Nat) ; (suc : Nat -> Nat) ;
The make tactic comes in handy for making quick definitions:
make one := 'suc 'zero : Nat ;
make two := 'suc ('suc 'zero) : Nat ;
On the other hand, let is useful for actual programming. (Whether you consider plus an actual program is a matter of taste.) Here we invoke the induction principle for natural numbers, and the Pig’s response tells us the cases we need to define. While the define tactic makes it look like we are writing a pattern-matching definition, in fact the case split is done by <= and the following lines just have to match it.
let plus (m : Nat)(n : Nat) : Nat ;
<= Nat.Ind m ;
define plus 'zero n := n ;
define plus ('suc k) n := 'suc (plus k n) ;
root ;
The elaborate tactic allows you to evaluate an expression and check its result:
elaborate plus two two ;
With those preliminaries out of the way, on to the new stuff. First, Peter’s shiny new idata tactic allows indexed data types to be written in a nice syntax (nicer than codes, anyway). As usual, parameters occur before the colon and indices afterwards.
idata Vec (A : Set) : Nat -> Set := (nil : Vec A 'zero) ; (cons : A -> (n : Nat) -> Vec A n -> Vec A ('suc n)) ;
Once we have plus and vectors, what could be more natural than writing vector append? This has become much more pleasant in recent weeks, because equations that once had to be eliminated by hand are now dealt with automatically. Now you can write the program you would expect, more or less.
let append (A : Set)(m : Nat)(as : Vec A m)(n : Nat)(bs : Vec A n) : Vec A (plus m n) ;
<= Vec.Ind A m as ;
define append A 'zero 'nil n bs := bs ;
define append A ('suc k) ('cons a k as) n bs := 'cons a (plus k n) (append A k as n bs) ;
root ;
Finally, let us test our function:
make as := 'cons 'true one ('cons 'false 'zero 'nil) : Vec Bool two ;
make bs := 'cons 'false one ('cons 'true 'zero 'nil) : Vec Bool two ;
elaborate append Bool two as two bs ;
The output is not as pretty as it could be, and better implicit argument support could make the code a bit less verbose, but working with Epigram is starting to look like programming!