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!
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
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 ) and
CatB (being )?
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 , and, I hoped, , at that!), unifying that with , 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:
That, as far as it goes is just what we want, but when we try to prove it with this function:
See, the problem (or, more correctly: my problem) is that
is true, but that's a property of boolean decidability, perhaps? It's easy enough to solve if I refine the term
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:
With we say that something is true, typefully, (that's a word, now) for us to proceed. So, our , etc, functions become easy to write:
and then verification is simply the compilation unit, but you can query the type or test out any value with it as well:
And there you go, we've verified, for the left-adjoin anyway, that a type has the identity function. Let's verify the other three cases as well: