Idris Auto-Implementations

So far, Type-Driven Development with Idris has been a great read and I’ve been learning quite a bit. The development style of using typed holes and auto-expanding cases is brilliant. However, whether because of this or for some other reason, some of the code examples are a bit messy.

One thing the book does a few times is create a function returning a Maybe, but where every case is Just.

getEntry : Integer -> DataStore -> String -> Maybe (String, DataStore)
getEntry pos store input =
  let store_items = items store
  in case integerToFin pos (size store) of
    Nothing => Just ("Out of range\n", store)
    Just id => Just (index id (items store) ++ "\n", store)

Of course, in these kinds of functions it’s simpler to remove the Maybe from your types and return the plain old values themselves. If we need a Maybe at the call site, we can always wrap in Just there.

It’s also strange that this example saves store_items but then never uses them. It’d be nice to have a check for unused variables.

getEntry : Integer -> DataStore -> String -> (String, DataStore)
getEntry pos store input =
  case integerToFin pos (size store) of
    Nothing => ("Out of range\n", store)
    Just id => (index id (items store) ++ "\n", store)

From the same example, we get this bit of code where we’re using a case statement to pattern match…but there’s only one possible pattern to match!

parse : (input : String) -> Maybe Command
parse input =
  case span (/= ' ') input of
    (cmd, args) => parseCommand cmd (ltrim args)

To my eye, it seems cleaner to just bind the new names with a let instead of casing on one case.

parse : (input : String) -> Maybe Command
parse input =
  let (cmd, args) = span (/= ' ') input
  in parseCommand cmd (ltrim args)

It’s pretty amazing the number of times Idris can write itself, but it’s good to remember that just because it can generate so much, that doesn’t mean the generated result is guaranteed to be clean.