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.

--

--

--

An old programmer learning new tricks.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Tezos Community Rewards — April 2022 Winners

3 new ways to mock out APIs in Python

Download In *!PDF

Launching an AWS-EC2 Instance with Apache Server using a bash script and configuring a custom…

CloudFront Signed URLs / Cookies and S3 Presigned URLs

Extracting tweets or keywords using Twint: A step by step tutorial for beginners

Create High Availability Architecture with AWS CLI.

Creating and Using Dynamic Libraries in C

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.

More from Medium

SonarQube Code Coverage For Javascript/Typescript

Supercomputers

The Differences Between Static and Dynamic ibraries

Loops and Nested Loops