Type classes in idris: proving away constraints and ensuring totality

Sometimes you have disjoint but covering class instances for a type in idris. TLDR: you can use idris’ proof language and the curry-howard correspondence to both statically bind the instances and prove that disjoint class instance types are total in the same way that writing a total function is a self evident proof of its own totality.

module Main
import System
import Data.Bool
import Decidable.Equality
isEven : Nat -> Bool
isEven Z = True
isEven (S Z) = False
isEven (S (S x)) = isEven x
data EvenOrOddNumber : (n : Nat) -> (b : Bool) -> Type where
  EON : (n : Nat) -> EvenOrOddNumber n (isEven n)
rawNat : EvenOrOddNumber n b -> Nat
rawNat (EON n) = n
implementation Show (EvenOrOddNumber _ True) where
  show x = “even “ ++ (show (rawNat x))
implementation Show (EvenOrOddNumber _ False) where
  show x = “odd “ ++ (show (rawNat x))

In the repl, we can try it out:

λΠ> show (EON 3)
“odd 3”
λΠ> show (EON 4)
“even 4”

But when we add:

main : IO ()
main = do
  args <- getArgs
  putStrLn $ show $ EON $ length args

Something a bit unexpected happens:

- + Errors (1)
 ` — src/Main.idr line 28 col 13:
 While processing right hand side of main. Can’t find an implementation
 for Show (EvenOrOddNumber (length args) (isEven (length args))).
 
 src/Main.idr:28:14–28:38
 24 | 
 25 | main : IO ()
 26 | main = do
 27 | args <- getArgs
 28 | putStrLn $ show $ EON $ length args
                 ^^^^^^^^^^^^^^^^^^^^^^^^

How does one fix this?

The answer is the curry-howard correspondence! Functional programs are proofs of type systems. We can use idris’ proof language to erase the constraint obligation and statically determine the instances to be used. We can start with a skeleton that asks whether isEven is true in proof form.

showEON : {n : Nat} -> EvenOrOddNumber n (isEven n) -> String
showEON _ with (decEq (isEven n) True)
  showEON _ | Yes prf = ?showT
  showEON _ | No contra = ?showF

And then we can ensure that each of these cases does show on an instance whose type is statically determinable to be implemented.

In this case, we’ll declare a local variable with a type that matches one of our cases:

showEON _ | Yes prf =
  let
    toShow : EvenOrOddNumber n True
    toShow = ?showT
  in
  show toShow

This doesn’t have a constraint obligation because it trivially has the same shape as an instance of show for our EvenOrOddNumber.

We can use the language of proofs to construct this value by changing the result type back to what we get from the EON constructor.

showEON _ | Yes prf =
  let
    toShow : EvenOrOddNumber n True
    toShow =
      rewrite sym prf in
      ?eon_n -- Main.eon_n : EvenOrOddNumber n (isEven n)
  in
  show toShow

Shows that we can replace ?eon_n with EON n and this works.

The No case is trickier as is tradition with decEq, but we can start to sketch the proof like this:

showEON _ | No contra = -- contra : isEven n = True -> Void
  let
    notEven : (isEven n = False)
    notEven =
      ?notEvenEven
    toShow : EvenOrOddNumber n False
    toShow = ?showF
 in
 show toShow

So how do we get notEven from contra? Our new friend invertContraBool and some helpers.

invertBoolFalse : {a : Bool} -> not a = True -> a = False
invertBoolFalse {a = True} prf impossible
invertBoolFalse {a = False} prf = Refl

And done:

let
  invertedContra : (not (isEven n) = True)
  invertedContra = invertContraBool (isEven n) True contra
  notEven : (isEven n = False)
  notEven = invertBoolFalse invertedContra
  toShow : EvenOrOddNumber n False
  toShow =
    rewrite sym notEven in
    EON n
 in
 show toShow

And finally:

$ idris2 --build ./tc.ipkg 
$ ./build/exec/tc
odd 1
$ ./build/exec/tc foo 
even 2
$ ./build/exec/tc `ls -1`
even 4

So what have we learned?

• As I explored a while ago, you can use class constraint obligations as a (maybe even gentler) stand-in for proof obligations while writing type-heavy code.
• Using a class method on an object whose type unambiguously matches one instance statically uses that instance and doesn’t pass on a constraint obligation.
• You can use the language of proofs to rewrite a result type so that a value you hold can be held by an alias with a stronger type via rewrite.
• You can use strengthened types to both discharge constraint obligations and show totality even though we’re required to keep class instances disjoint.