# 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.EqualityisEven : Nat -> Bool

isEven Z = True

isEven (S Z) = False

isEven (S (S x)) = isEven xdata EvenOrOddNumber : (n : Nat) -> (b : Bool) -> Type where

EON : (n : Nat) -> EvenOrOddNumber n (isEven n)rawNat : EvenOrOddNumber n b -> Nat

rawNat (EON n) = nimplementation 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.