Idiomatic way of listing elements of a sum type in Idris

Question

I have a sum type representing arithmetic operators:

data Operator = Add | Substract | Multiply | Divide

and I'm trying to write a parser for it. For that, I would need an exhaustive list of all the operators.

In Haskell I would use deriving (Enum, Bounded) like suggested in the following StackOverflow question: Getting a list of all possible data type values in Haskell

Unfortunately, there doesn't seem to be such a mechanism in Idris as suggested by Issue #19. There is some ongoing work by David Christiansen on the question so hopefully the situation will improve in the future : david-christiansen/derive-all-the-instances

Coming from Scala, I am used to listing the elements manually, so I pretty naturally came up with the following:

Operators : Vect 4 Operator
Operators = [Add, Substract, Multiply, Divide]

To make sure that Operators contains all the elements, I added the following proof:

total
opInOps : Elem op Operators
opInOps {op = Add} = Here
opInOps {op = Substract} = There Here
opInOps {op = Multiply} = There (There Here)
opInOps {op = Divide} = There (There (There Here))

so that if I add an element to Operator without adding it to Operators, the totality checker complains:

Parsers.opInOps is not total as there are missing cases

It does the job but it is a lot of boilerplate. Did I miss something? Is there a better way of doing it?

You can implement the Enum interface for Operator manually. — Anton Trunov
@AntonTrunov Thanks, that's where I started really but I'm not quite sure how fromNat should behave for example. — blouerat
That depends on your exact use case, but e.g. something like fromNat Z = Add fromNat (S Z) = Subtract fromNat (S (S Z)) = Multiply fromNat (S (S (S _))) = Divide might work for you. — Anton Trunov
Thanks a lot, using Enum does seem more idiomatic but then I have to give up exhaustiveness which is a bit of a shame — blouerat
you can still prove exhaustiveness, just prove that for every op, there is a k : Nat, such that fromNat k = op — Kim Stebel

Anton Trunov Anton Trunov · Accepted Answer · 2017-08-17T01:05:52

There is an option of using such feature of the language as elaborator reflection to get the list of all constructors.

Here is a pretty dumb approach to solving this particular problem (I'm posting this because the documentation at the moment is very scarce):

%language ElabReflection

data Operator = Add | Subtract | Multiply | Divide

constrsOfOperator : Elab ()
constrsOfOperator = 
  do (MkDatatype _ _ _ constrs) <- lookupDatatypeExact `{Operator}
     loop $ map fst constrs

  where loop : List TTName -> Elab ()
        loop [] =
          do fill `([] : List Operator); solve
        loop (c :: cs) =
          do [x, xs] <- apply `(List.(::) : Operator -> List Operator -> List Operator) [False, False]
             solve
             focus x; fill (Var c); solve
             focus xs
             loop cs

allOperators : List Operator
allOperators = %runElab constrsOfOperator

A couple comments:

It seems that to solve this problem for any inductive datatype of a similar structure one would need to work through the Elaborator Reflection: Extending Idris in Idris paper.
Maybe the pruviloj library has something that might make solving this problem for a more general case easier.

Idiomatic way of listing elements of a sum type in Idris

1 Answers