How can i convince Idris that my function is covering?

Question

I wrote a function doSomething that takes an open or closed parenthesis and returns a corresponding Int:

doSomething : (c : Char) -> {auto isPar : c == '(' || c == ')' = True} -> Int
doSomething '(' {isPar = Refl} = 1
doSomething ')' {isPar = Refl} = -1

With isPar i want to make sure that only parentheses and no other characters can get passed to doSomething. But Idris complains:

Error: doSomething is not covering
Missing cases:
    doSomething _

How can i convince or proof to Idris that all possible cases are covered? I tried:

doSomething 'a' {isPar = Refl} impossible --this type checks
doSomething _   {isPar = Refl} impossible --this not

Answer 1

The compiler can't guess that ( and ) are the only values that allow the construction of an isPar values, and thus is not able to conclude that the remaining case is impossible.

A workaround is to keep track that something is not an open or a clos parenthesis. It can be done like so:

import Data.So

doSomething : (c : Char) -> {auto isPar : So (c == '(' || c == ')')} -> Int
doSomething x {isPar} = case (choose (x == '(')) of
  Left _ => 1
  Right notOpen => case (choose (x == ')')) of
    Left _ => -1
    Right notClose => case (soOr isPar) of
        Left isOpen => absurd $ soNotToNotSo notOpen isOpen
        Right isClose => absurd $ soNotToNotSo notClose isClose

So is a proof that a predicate is True, choose provides either a proof that a predicate is True (the left branch), or a proof that it isn't true (the right branch). Using the proof that x is neither ( (notOpen) nor ) (notClose), we can conclude by analysing why isPar is true (with soOr).

You can find the type of all the functions I used to deal with So in its package.

Answer 2

We can use a with expression to obtain an implementation that I think is a bit more elegant than using So, which I try to reserve only as a last resort.

||| Test if a Char is an open or close paren.
isParen : Char -> Bool
isParen '(' = True
isParen ')' = True
isParen _ = False

||| Obtain the integer code corresponding to a paren.
||| Proof is required that c is '(' or ')'.
parenCode :
  (c : Char) ->
  {auto 0 prf_isParen : isParen c === True}
  Integer
parenCode c with (isParen c)
  parenCode '(' | True = 1
  parenCode ')' | True = -1
  parenCode _   | False impossible

If we perform the comparison inside the with, the compiler is able to recognize isParen c as identical to the expression as in our prf_isParen.

This generates Scheme code that you would hope for:

(define Misc-isParen
  (lambda (arg-0)
    (cond ((equal? arg-0 #\() 1)
          ((equal? arg-0 #\)) 1)
          (else 0))))

(define Misc-with--parenCode-8826
  (lambda (arg-0 arg-1 arg-2)
    (cond
      ((equal? arg-0 #\() (cond (else 1)))
      (else (cond (else -1))))))

(define Misc-parenCode
  (lambda (arg-0)
    (Misc-with--parenCode-8826 arg-0
                               (Misc-isParen arg-0)
                               'erased)))

Although the with generates an extra function call, it only invokes one character comparison.

Also, the Chez compiler is smart enough to optimize away these nested functions:

(expand/optimize
  '(let ((Misc-isParen
           (lambda (arg-0)
             (cond ((equal? arg-0 #\() 1)
                   ((equal? arg-0 #\)) 1)
                   (else 0))))
         (Misc-with--parenCode-8826
           (lambda (arg-0 arg-1 arg-2)
             (cond ((equal? arg-0 #\() (cond (else 1)))
                   (else (cond (else -1))))))
         (Misc-parenCode
           (lambda (arg-0)
             (Misc-with--parenCode-8826 arg-0
                                        (Misc-isParen arg-0)
                                        'erased))))
  (Misc-parenCode #\()))

(Misc-with--parenCode-8826 #\( (Misc-isParen #\() 'erased)

---

You can also use with in this manner to construct the required proof that isParen c === True, by using the extra proof binding:

parenCodeTry : (c : Char) -> Maybe Integer
parenCodeTry c with (isParen c) proof prf_isParen
  _ | False = Nothing
  _ | True = Just $ parenCode c

In the True branch of parenCodeTry, the type of prf_isParen will be:

prf_isParen : Equal (isParen c) True

which will allow the compiler to find a value for the auto 0 prf_isParen parameter.

In the False branch of parenCodeTry, it will be:

prf_isParen : isParen c = False

which of course is not a valid value for the auto 0 prf_isParen parameter, and therefore you would not be able to invoke parenCode in that branch.