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 Mainimport 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.