Inspiration for this blog post came from my work on volgenmodel-nipype, a neuroimaging workflow written using Nipype. The Nipype package allows one to wrap legacy command line applications using traits to model the various command line options. Here’s a snippet for mincextract taken from nipypeminc.py:

Note the xor condition, which means that the user cannot set write_ascii and write_byte at the same time. So this would be ok:

but this would be rejected:

A few times I made mistakes with these xor specifications which resulted in run time errors. Recently I learned that Haskell’s type system can be used to make certain errors compile time errors instead of run-time errors, and I naturally wondered if an xor-type of condition could be encoded in Haskell’s type system, and if not that, perhaps in Idris.

A basic implementation in Haskell of a command line wrapper might look like this:

A command line option has a description, argument string, and a value. For simplicity we will only consider integer values.

Again, for simplicity, two options are considered equal if their arg strings match:

Here are some example options:

A program consists of a path to a binary, a list of options, and a list of xor conditions, which are lists of options that cannot be set simultaneously.

A list of options has a clash if it intersects with any of the xor-lists in more than two elements:

We won’t bother with the full details of spawning a process, tidying up output files, capturing stdout and stderr, and so on, so this runProgram function just prints some details and checks that the options list is acceptable:

Here’s a program with no xor conditions; it runs ok:

*OptionsInHaskell> runProgram prog1
Pretending to run: /usr/local/bin/foo
with options: [ MkOption {optDesc = "Value of Foo.", optArgStr = "-foo", optValue = 34}
, MkOption {optDesc = "Do bar.", optArgStr = "-bar", optValue = 99}
, MkOption {optDesc = "Blah.", optArgStr = "-blah", optValue = 0}
]
and xor lists: []


On the other hand, this program is not valid since options 1, 2, and 3 are set, but the xor list specifies that options 1 and 2 cannot be set at the same time:

*OptionsInHaskell> runProgram prog2
Pretending to run: /usr/local/bin/foo
with options: [ MkOption {optDesc = "Value of Foo.", optArgStr = "-foo", optValue = 34}
, MkOption {optDesc = "Do bar.", optArgStr = "-bar", optValue = 99}
, MkOption {optDesc = "Blah.", optArgStr = "-blah", optValue = 0}
]
and xor lists: [ [ MkOption {optDesc = "Value of Foo.", optArgStr = "-foo", optValue = 34}
, MkOption {optDesc = "Do bar.", optArgStr = "-bar", optValue = 99}
]
]
*** Exception: eek, options clash :(


I’m not sure if we can make this a compile time error in Haskell, so I’ll turn instead to Idris, where can exploit dependent types and other nice things.

First define an option data type, the equality instance, and a few examples:

Next we need to encode in the type system the result of an option list clashing or not:

Checking if an option list has a clash is basically the same as in Haskell except that we return a ClashValue instead of a Bool:

Next, the tricky bit. We create a data type IsNotClashing which has only one constructor, called Ok, that produces a value IsNotClashing NotClashing. There is no way to produce the value IsNotClashing Clashing.

Example values, used later:

The heart of the solution is the ValidOptionList data type. We take an option list and an xor list and, if a proof can be constructed for the value Ok using the expression IsNotClashing (notclash opts xors), then we produce the actual value ValidOptionList opts. Due to the definition of Ok, this condition means that notclash opts xors must evaluate to NotClashing. Hopefully this makes it clear why the data types ClashValue and IsNotClashing were needed.

Finally, the runProgram function takes a path to an executable and a valid list of options. The fact that the list of options is valid is encoded in the type system.

This program has options 1 and 2 set with the xor condition saying that options 2 and 3 cannot be set at the same time, so it type checks:

On the other hand, this program with options 2 and 3 set does not type check, as expected:

The first part of the error is a bit scary:

 Can't unify
IsNotClashing NotClashing
with
IsNotClashing (boolElim (foldrImpl (flip (.) . flip (\x => \y => x || Delay (Prelude.Classes.Nat instance of Prelude.Classes.Ord, method > (Nat instance of Prelude.Classes.Ord, method compare (length (OptionsInIdris.notclash, intersect myOptions23 myXors23 myOptions23 y)) 2) (length (OptionsInIdris.notclash, intersect myOptions23 myXors23 myOptions23 y)) 2 || Delay (Nat instance of Prelude.Classes.Eq, method == (length (OptionsInIdris.notclash, intersect myOptions23 myXors23 myOptions23 y)) 2)))) id id myXors23 False) (Delay Clashing) (Delay NotClashing))


but the second part has the goods:

 Specifically:
Can't unify
NotClashing
with
Clashing


So there we have it. Compile-time error checking in Idris of a disjointness condition in the options for wrapping a legacy command line program.