I’m learning Idris. Unfortunately, my heart sank when I read the words “The length of the list should be statically known”. Then I read this. I want to use dependent types to do real things. Specifically, I want to use a fixed-length vector type to perform arithmetic on data obtained from the outside world.

I have previously tried to approach this problem in Haskell land using some of its dependent type features and was always disappointed that I could not get a reasonable answer to the problem of reading in data of unknown size and performing operations on it using fixed-length data types. Fortunately, I did not give up and Edwin Brady’s book had the clues all along. The secrets lie in chapter 5 Interactive programs: input and output processing, in dependent pairs and in the use of the exactLength function.

Here is my first stab at this problem in all its glory:

The next part of my journey will be to grok how exactLength works. I think it’s something to do with this.

Update

In case you were wondering about the use of the the function in the (IO (Either FileError (List Int, List Int))): this is used to fix the type of the return from withFile. Without this, Idris cannot infer the type of the expression. This seems like a compiler bug to me.

Update (2)

Instead of the (IO (Either FileError (List Int, List))), the code now provides a value for the implicit a argument to withFile using {a = (List Int, List Int)}.

Tags