Type classes in idris: proving away constraints and ensuring 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))
λΠ> show (EON 3)
“odd 3”
λΠ> show (EON 4)
“even 4”
main : IO ()
main = do
args <- getArgs
putStrLn $ show $ EON $ length args
- + 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
^^^^^^^^^^^^^^^^^^^^^^^^
showEON : {n : Nat} -> EvenOrOddNumber n (isEven n) -> String
showEON _ with (decEq (isEven n) True)
showEON _ | Yes prf = ?showT
showEON _ | No contra = ?showF
showEON _ | Yes prf =
let
toShow : EvenOrOddNumber n True
toShow = ?showT
in
show toShow
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
showEON _ | No contra = -- contra : isEven n = True -> Void
let
notEven : (isEven n = False)
notEven =
?notEvenEven
toShow : EvenOrOddNumber n False
toShow = ?showF
in
show toShow
invertBoolFalse : {a : Bool} -> not a = True -> a = False
invertBoolFalse {a = True} prf impossible
invertBoolFalse {a = False} prf = Refl
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
$ idris2 --build ./tc.ipkg 
$ ./build/exec/tc
odd 1
$ ./build/exec/tc foo
even 2
$ ./build/exec/tc `ls -1`
even 4
  • 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.

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
art yerkes

art yerkes

An old programmer learning new tricks.