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
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
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.
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!
To my eye, it seems cleaner to just bind the new names with a
let instead of casing on one case.
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.