Idris review

I finally got Idris to build, and I spent last week reading "Type-driven Development with Idris". The build was tricky, mainly because Cabal is broken and my Haskell installation resembles sprinkler's water droplets on a grass yard.

After using it for a short while, I have lot of good to say about Idris. I like most of the syntax, and find that most of the features are sensible and straightforward to use.

Lets start with the bad things to say so we get them out of the way.

Implicit arguments are vague

Idris allows you to declare arguments as implicit. This means that the argument is automatically deduced from the context.

ident : {a:Type} -> a -> a

Such type arguments are inferred from the context, and overall it's very useful to have it this way.

However I have very little clue of how these implicit arguments are exactly working, even after reading the documentation. For example there are auto-implicits that try to solve automatically by expression search.

some_string : {auto x : Nat} -> String

And this all remotely resembles logic programming features.

Where is all the library documentation?

I've tried to figure this out for a while, but how am I supposed to find out what's in the existing libraries of Idris? It was so well hidden that I didn't find it immediately.

Eventually I stumbled upon something during searching. The IdrisDoc seems to have browseable documentation. Additionally you can use REPL to browse the documentation, I guess there must be also some other tools for browsing the documentation somewhere.

Otherwise there seem to be a quite nice bunch of libraries coming with Idris, and I don't need to do anything exciting to use them.

When Idris REPL starts up, it seem to take few seconds loading modules. This is something I don't like because a good runtime should start up immediately. They seem to have fixed this in Idris2 though, or then it's still missing the libraries that slow down the REPL startup.

Some type errors can be very misleading

While playing with it for a while, I've found that some simple failures may produce very weird type errors:

85 | format (Num fmt) acc = (\num => format fmt (acc ++ show i))
   |                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of format with expected type
        PrintfType (Num fmt)

When checking argument acc to Main.format:
        Can't disambiguate since no name has a suitable type: 
                Prelude.List.++, Prelude.Strings.++

What is wrong with that line 85, is that I had forgotten i into show i, it should have been num. Still I'm looking at this error and it's proposing that the concatenation here has something odd going on, completely misleading me to thinking that I've done something else wrong here.

A little demostration

Before we get to discussing good things about Idris, I'm bringing in few small example programs and explain what they do.

data Even : Nat -> Type where
  EvenZ : Even Z
  EvenS : Even n -> Even (S (S n))

data Odd : Nat -> Type where
  OddZ : Odd (S Z)
  OddS : Odd n -> Odd (S (S n))

Idris provides dependent datatypes, and those allow describing all kind of types that provide some constraints preventing us from constructing bad kind of types. Above statements describe what even and odd numbers are, and give the definition some labels.

Now we're able to express that no natural number can be both even and odd. It's fairly easy to state:

-- the proposition
either_even_or_odd : (n : Nat) -> Even n -> Odd n -> Void

-- the proof
either_even_or_odd Z EvenZ OddZ impossible
either_even_or_odd Z EvenZ (OddS _) impossible
either_even_or_odd (S (S k)) (EvenS x) (OddS y) =
  either_even_or_odd k x y

It should also mean that we can tell any number is either even or odd. Let's see about that:

decide_even_odd : (n : Nat) -> Either (Even n) (Odd n)
decide_even_odd Z = Left EvenZ
decide_even_odd (S Z) = Right OddZ
decide_even_odd (S (S k)) = case decide_even_odd k of
  (Left l) => Left (EvenS l)
  (Right r) => Right (OddS r)

Idris makes it really enjoyable to build this kind of proofs and programs. I'm using idris-vim that doesn't seem to be fully featured but still has enough featurewise that I am comfortably letting Idris expand case statements and fill up trivial proofs.

So far we proved a trivial property about even and odd numbers. Is this useful if we are programming something?

Consider you'd have indexing function such as get_record, with type telling you that you get either integers with even numbers or strings with odd numbers.

get_record : (n : Nat) -> Either (Even n, Int) (Odd n, String)

Now you'd like to conclude that with odd number, you get a string:

get_string : (n : Nat) -> Odd n -> String
get_string n n_is_odd = case get_record n of
  (Left (n_is_even, _)) => absurd (either_even_or_odd n n_is_even n_is_odd)
  (Right (n_is_odd, s)) => s

Of course you could just pair integers and strings together within lists. Still it's quite impressively expressive, what else can you do with this?

Well, one thing I was particularly impressed about is that you can implement a printf that can be typechecked! This was presented in the book.

data Format = Num Format | Str Format | Lit String Format | End

PrintfType : Format -> Type
PrintfType (Num fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (s : String) -> PrintfType fmt
PrintfType (Lit s fmt) = PrintfType fmt
PrintfType End = String

format : (fmt : Format) -> (acc : String) -> PrintfType fmt
format (Num fmt) acc = (\num => format fmt (acc ++ show num))
format (Str fmt) acc = (\str => format fmt (acc ++ str))
format (Lit lit fmt) acc = format fmt (acc ++ lit)
format End acc = acc

The actual parsing of the printf-string seem involving, but once it has been done, it can be used to determine a type:

*Hello> PrintfType End
String : Type
*Hello> PrintfType (Lit "hello" End)
String : Type
*Hello> PrintfType (Lit "hello " $ Str $ End)
String -> String : Type
*Hello>

This is something I haven't seen often elsewhere except in dynamic languages:

*Hello> format (Lit "hello " $ Str $ End)
format (Lit "hello " (Str End)) : String -> String -> String
*Hello> format (Lit "hello " $ Str $ End) "*** "
\str => prim__concat "*** hello " str : String -> String
*Hello> format (Lit "hello " $ Str $ End) "*** " "foo"
"*** hello foo" : String

Sure, just having a strong static type system gets you much of the way there. That's bit like saying that a one-way train trip to Moscow can substitute a round-trip flight from Helsinki to Sydney, you get pretty much out there after all. Yeah.

Good things to say about Idris

Lets continue with the good things I have to say about Idris.

It's use is fairly simple to understand, it's bit like a simpler version of Haskell.

The reusable interfaces (typeclasses) have superb nice syntax. For example, here's how you'd define display and equality for vehicles described by dependent datatypes.

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
  Bicycle : String -> Vehicle Pedal
  Car : (fuel : Nat) -> String -> Vehicle Petrol
  Bus : (fuel : Nat) -> String -> Vehicle Petrol

Show (Vehicle a) where
    show (Bicycle name) = "bicycle " ++ name
    show (Car fuel name) = "car " ++ name
    show (Bus fuel name) = "bus " ++ name

Eq (Vehicle a) where
  (==) (Bicycle x) (Bicycle y) = (x == y)
  (==) (Car _ x) (Car _ y) = (x == y)
  (==) (Car _ x) (Bus _ y) = False
  (==) (Bus _ x) (Car _ y) = False
  (==) (Bus _ x) (Bus _ y) = (x == y)

Overall these dependent datatypes are also straightforward and enjoyable to use.

Another thing I like is that the whole thing consistently rolls around types. We can describe programs for different types with namespaces:

namespace Thing
  action : Bool
  action = True

namespace Thong
  action : String
  action = "hello"

And it selects either one depending on type. This really decreases the amount of things you need to remember, as similar ideas use similar terms.

Even the dependent pair is "overloaded" such that you use the ** to represent both the type and the proof for it.

For a short while I've found it very comfortable to use Idris, although I hope it'll be just a milestone for me. I'm planning to improve upon this in few ways.

Actually I have some proposal for Idris developers.

Version & separate modules and their interfaces

I'd propose that you provide ways to separate the library modules from their interfaces such that:

The interface can be shared between multiple implementations.
Interfaces are detailed enough such that you can't build the software if modules wouldn't work together correctly.
System checks that the interfaces once published are unable to change without a version being bumped upwards.

Otherwise modules can work like they are, I just want that we'd can create a packaging system that is reliable enough for daily casual use.

Btw. I also managed to get Idris2 to compile. Haven't looked into it much yet though.