Most programming languages will only allow you to discover errors in your program through testing or when your users point out bugs. Idris however allows you to check your program's behaviour and other conditions you can define while you are writing your program. Here are three use cases that show the power of Idris' type system.
Many languages have a type system that checks that the right kind of data is used in a program. Idris uses values in types which lets you exclude bad values as well as restricting the kind of value allowed. Idris also lets you describe behaviour in types to prevents parts of a program interacting with each other in a way you didn't intend. Finally Idris checks that your programs actually produce results and don't get stuck in a loop doing nothing.
I came across Idris about a year ago while doing a Stepik course on dependent types by Dmytro Mitin. I was fascinated by how Idris used values in types. Idris types are as flexible as functions in other languages and tied to the values of your data instead of just the categories. One of the first examples that I found useful in Idris was how it uses different types for empty lists and lists that have values in them. It bothered me for a long time that getting the head of an empty list would throw an exception or return a null or Option type. Because Idris doesn't allow you to pass an empty list to the head function in the first place this is not an issue. That made me wonder about what other errors Idris's type system could prevent.
Checking for invalid function arguments with Idris
Idris lets you use values in types so the compiler can check that you don't pass invalid values into functions.
In order to test Idris' ability to constrain input values, I decided to play around with coding a noughts and crosses game. I didn't want to be able to pass coordinates that would exceed the boundaries of my board. Noughts and crosses is a children's game where you compete to fill a row, column or diagonal with either a circle or a cross. In the code, I represented the board as the list of filled in squares with the coordinate and either a circle or a cross.
In many other languages you couldn't guarantee that these coordinates are inside the bounds of the board, but in Idris you can specify the size of the board in its type and specify that the coordinates of squares have to be less than the size of the board. I did this by passing proof parameters to my function that adds squares to the board. They prove that the cell added has a row and column within the bounds of the board. Here LT is a proof that one natural number is less than another.
{ auto p1: LT r rows} { auto p2: LT c cols }
Fortunately Idris can infer proof parameters automatically much of the time, so I used the auto keyword to hint to Idris that the proofs can be found in the context where the function is called:
data Cell : Nat -> Nat -> Type where
Cross : (r: Nat) -> (c: Nat) -> { auto p1: LT r rows} ->
{ auto p2: LT c cols } -> Cell rows cols
Circle : (r: Nat) -> (c: Nat) -> { auto p1: LT r rows} ->
{ auto p2: LT c cols } -> Cell rows cols
data Board : (rows: Nat) -> (cols: Nat) -> Type where
Cells : {n : Nat} -> Vect n (Cell rows cols) -> Board rows cols
addCell : Cell rows cols -> Board rows cols -> Board rows cols
addCell cl (Cells cs) = Cells (cl :: cs)
Checking for behaviour errors with Idris
A type in Idris can also describe behaviour and the compiler can use types to check for errors in how a program behaves.
To test Idris' ability to encode behaviour, I wrote a program for a flight maintenance plan. It takes a made-up sequence of flights between cities, checks that there are regular safety inspections and that the airplane never runs out of fuel. Instead of examining the values when the program runs, the requirements are checked at compile time.
I used a type AirplaneCmd to encode state transitions when an airplane flies between two cities, refuels, and has a safety inspection. Again, I used proof parameters to encode constraints. The Fly type requires two proofs in order to execute the Fly command.
{ auto p1 : LTE r f } { auto p2 : LT flights 2 }
The first checks that the fuel required for a flight is less than the fuel an airplane has in it. The second checks that a safety inspection happens every two flights.
AirplaneState : Type
AirplaneState = (Nat, Nat)
data AirplaneCmd : (ty : Type) -> AirplaneState -> AirplaneState -> Type where
Refuel : (f : Nat) -> AirplaneCmd () (fuel, flights) ((fuel + f), flights)
Fly : (r : Nat) -> { auto p1 : LTE r f } -> { auto p2 : LT flights 2 } ->
AirplaneCmd () (f, flights) (f - r, flights + 1)
SafetyInspection : AirplaneCmd () (fuel, flights) (fuel, Z)
Pure : (ty : Type) -> AirplaneCmd ty s1 s2
(>>=) : (AirplaneCmd a s1 s2) -> (a -> AirplaneCmd b s2 s3) -> (AirplaneCmd b s1 s3)
When a plane flies, the fuel left in the type is decremented by the fuel required for the journey and the number of flights since a safety inspection is incremented.
(f - r, flights + 1)
When a plane refuels the fuel available in the type increases by the amount refueled.
((fuel+ f), flights)
and a safety inspection resets the flights since an inspection to zero (Z).
(fuel, Z)
This type can be used to create a flight plan and check that safety and fuel requirements are met. The trips in the flight plan are represented by natural numbers that indicate how much fuel they require.
JHBToNYC : Nat
JHBToNYC = 45
NYCToDubai : Nat
NYCToDubai = 35
DubaiParis : Nat
DubaiParis = 15
flightPlan : { auto pInitFlights : LTE flights 2 } -> (eFl ** eFu ** AirplaneCmd () (0, 0) (eFl, eFu))
flightPlan = (_ ** _ ** do
Refuel 80
Fly JHBToNYC
Fly NYCToDubai
SafetyInspection
Refuel 15
Fly DubaiParis)
If there were more than two flights in a row without a safety check in between, this code would not compile. The compiler would also complain if there wasn't enough fuel added in the Refuel step.
Totality checking with Idris
Idris can check that programs finish and produce meaningful output. This is called totality checking, and it prevents your program from getting stuck in endless loops.
When you write an interactive program you want it to keep running in a loop, and you want it to always respond to user input. Idris handles this by using a type called Inf to ensure that something useful happens before the next step in the interactive loop. The type Inf guarantees that the recursive call happens inside a data constructor and the data constructor creates steps in the loop. It's up to the programmer to ensure that the steps each do something like printing output or interacting with the user. I wrote a simplified version of the Eliza program to explore the idea.
Eliza is an early chatbot that pretended to be a psychologist by recognising words or phrases in a user's input and generating a response. If the user says that she is feeling lonely, Eliza might ask "What if you didn't feel lonely?". The program keeps looping until the user decides to quit. While Idris can't prove that it ever stops the Idris Inf type can ensure that each step in the loop responds to the user.
The type of Eliza is an interaction with the user (IO a) and a potentially infinite sequence of Eliza conversations (Inf Eliza). The Inf type guarantees that a constructor wraps the expansion of the Eliza type and the constructor in this case is Conversation.
data Eliza : Type where
Conversation : IO a -> Inf Eliza -> Eliza
The data type KeepRunning is a flag that potentially tells the process to stop and otherwise allows it to keep going.
data KeepRunning = Stop | Continue (Lazy KeepRunning)
Run conversation stops if it gets the Stop signal and otherwise runs the interaction in the Conversation and continues. Actually creating a never ending loop using runForever is not total because it doesn't have the Inf type. KeepRunning can't use the Inf type without making runConversation non total because Idris uses the possibility of reaching Stop to check that the program can finish. This small part of the program is excluded from totality checking, but most of the program is checked.
total
runConversation : KeepRunning -> Eliza -> IO ()
runConversation (Continue rest) (Conversation ioInteraction conv) = do
ioInteraction
runConversation rest conv
runConversation Stop comp = pure ()
runForever : KeepRunning
runForever = Continue runForever
total
conversation : Eliza
conversation = Conversation (getSeed >>= (\seed => run (listenAndReply seed))) conversation
main : IO ()
main = runConversation runForever conversation
Idris lets you constrain values and behaviour before you run your program and can guarantee that when you loop you are doing something at each step. All of this and more can be guaranteed with checks at compile time thanks to Idris's powerful type system.
If you're interested in Idris check out Edwin Brady's book Type driven development in Idris.
Henry is a Scala developer at Jemstep. He loves functional programming in Lisp and Haskell. When he's not coding, he loves to listen to classical music and also plays the piano.
