oh : so True

So, ...

So, I'm going to say 'so' a lot in this post. You'll find out why this is, soonest.

soon, adv: composite word of the words 'so' and 'on.'

Amirite? Or amirite!

SO!

Today's 1HaskellADay challenge wasn't really a challenge, per se, so much as it was an observation, and that observation, keen as it might be...

keen, adj.: composite word of 'ki' (棋) and 'in' (院), transliteration from the Japanese: School of weiqi.

... was that the mapping function from one domain to a co-domain, and the corresponding co-mapping function from the co-domain to the domain gives you, when composed, the identity function in the domain or co-domain.

No, really! That was today's challenge.

To translate that into English:

f : a -> b
g : b -> a

(f . g) : a -> a
(g . f) : b -> b

Wowsers!

So, we're not going to dwell on this, as Eilenberg and Mac Lane have dwelt on this so much better than I, but ...

Okay, so how do we prove this for our

CatA (being Either a a) and
CatB (being (Bool, a))?

With Haskell, it's easy enough, run your functions through quickcheck and you've got a PGP, that is: a pretty good (kinda) proof of what you want.

Or, you could actually prove the thing.

'You' meaning 'I,' in this particular case, and, while proving the thing, actually learn some me some more Idris for greater good.

Let's do that.

So, my last post have looked at a bit of proof-carrying code, and my methodology was to create a predicate that said whether some supposition I had held (returning a Bool, and, I hoped, True, at that!), unifying that with True, and then using the reflexive property of equality to prove that my supposition held.

Well, super neat, but today's problem was much harder for me, because I wrote something like this for one of my proofs:

leftIsomorphism : Eq a => (Bool, a) -> Bool
leftIsomorphism pair = (f . g) pair == pair

That, as far as it goes is just what we want, but when we try to prove it with this function:

isEqLeftTrue : Ea a => (val : a)
-> leftIsomorphism (True, val) = True
isEqLeftTrue val = refl

That doesn't work because of a type-mismatch, so replacing the predicate through substitution eventually lead to this type-error:

When elaborating right hand side of isEqLeftTrue:

Can't unify
x = x
with
(val : a) -> val == val = True

See, the problem (or, more correctly: my problem) is that

val == val 

is true, but that's a property of boolean decidability, perhaps? It's easy enough to solve if I refine the term

val == val 

down to

True

then apply the reflexive property to obtain my proof, but the problem (again: my problem) is that I'm not all that savvy with refinement in proofs to get the answer out and blogged today.

The show must go on!

But the co-problem, or, getting a little less esoteric, the solution is that the Idris language already provides something that addresses this: so

Idris*> :t so
Prelude.Bool.so : Bool -> Type

With so we say that something is true, typefully, (that's a word, now) for us to proceed. So, our isEqLeftTrue, etc, functions become easy to write:

isEqLeftTrue : Eq a => (val : a) 
-> so (leftIsomorphism (True, val)) -> ()
isEqLeftTrue val pred = ()

and then verification is simply the compilation unit, but you can query the type or test out any value with it as well:

Idris*> isEqLeftTrue "hey"
isEqLeftTrue "hey" : (so True) -> ()

And there you go, we've verified, for the left-adjoin anyway, that a (,) True type has the identity function. Let's verify the other three cases as well:

isEqLeftFalse : Eq a => (val : a) 
-> so (leftIsomorphism (False, val)) -> ()
isEqLeftFalse val p = ()

... and for our right-adjoin proofs:

rightIsomorphism : Eq a => Either a a -> Bool
rightIsomorphism eith = (g . f) eith == eith

isEqRightLeft : Eq a => (val : a) 
-> so (rightIsomorphism (Left val)) -> ()
isEqRightLeft val p = ()

isEqRightRight : Eq a => (val : a) 
-> so (rightIsomorphism (Right val)) -> ()
isEqRightRight val p = ()

... and then the compilation proves the point, but we can exercise them, as well:

Idris*> isEqLeftFalse 1

isEqLeftFalse 1 : (so True) -> ()

Idris*> isEqRightLeft 'a'

isEqRightLeft 'a' : (so True) -> ()

Idris*> isEqRightRight "hey"

isEqRightRight "hey" : (so True) -> ()

... and there you have it.

Pensée

Huh. Looking at the above four proof-functions, they have the same type signatures (pretty much) and the same definitions. Hm. Maybe that's an indicator for me to start looking at Idris' syntactic extensions? Something for me to pensée about.

Ciao for now.