No Roam at the Inn(sbruck)

Okay, so, for yesterday's 1HaskellADay problem (about 'collect'ing 'stuff' from 'room's), we’re looking at a pathing-kind of problem, and that is 

{- You have a list of rooms, each rooms has two doors and contain one element.

  To enter a room, the first door must be opened. To leave a room, the second door

  must be open. It means that if you want to move from one room to the next one,

  both the second door of the first room and the first door of the second room.

-}

data Room a = Room (Bool, Bool) a

{- | Given a list of rooms, we want to go as far as we can and collect the elements

  in he room. This is the purpose of the function `collect`.

  Examples:

  >>> collect [Room (True, True) 1, Room (True, False) 2, Room (True, False) 3]

  [1,2]

  >>> collect [Room (False, True) 1, Room (True, False) 2, Room (True, False) 3]

  []

  >>> collect [Room (True, True) 'a', Room (False, True) 'b', Room (True, True) 'c']

  ['a']

-}

collect :: [Room Int] -> [Int]

collect = undefined

Okay, so right off the bat, you see the type is just ... wrong. Look at the type signature. It does not allow the third example at all, so, really collect’s type is:

collect :: [Room a] -> [a]

Ouch.

So, anyway (you know, running the examples before publishing them ... ‘might’ be prudent).

This particular, problem, albeit trivial, brings to mind two analogues: one is proof search, because we’re going from ‘room’ to ‘room’ (truth to truth) collecting ‘stuff’ (lemmas), and we stop when we hit a closed door (the proof search stops at a falsehood). So if we look at it this way, then all we need to do is build us some generic proof search algorithm, and make the Room type hypotheses, and we’re done.

But we don’t need to do this in Idris, as Idris already has a proof search algorithm.

It’s called, conveniently enough: ‘proof search.’

UGH! TOO EASY!

The other thing this little problem recalled to me was the optimization algorithms I was exploring, including GAs (genetic algorithms) and ACO (ant colony optimization), but the pathing is way too easy for these kinds of hammers.

Now if we had room defined something like:

data Room a = Room String [Room a] a

THEN we’re cooking with gas, because if you have a house, your rooms sometimes have one door, sometimes have several, so:

(bleh! draw a picture of our house here!)

And in this example here the rooms are identified (as they aren’t in today’s problem), and a room can have multiple egress points. Direction isn’t defined either. Another things: this graphic is not acyclic. So how do we deal with that.

Maybe now it’s time to call in the ants, eh?

At any rate, my solution to today’s problem was a rather straightforward Idris exercise:

module corn -- as in maze (pronounced mah-ees)

data Roam a = Room (Bool, Bool) a -- note: Roam, Room

collect : List (Roam a) -> List a -- note: NOT! Int, but _a_ duh!

collect [] = []

collect ((Room (False, _) _) :: _) = []

collect ((Room (True, x) y) :: rest) = 

    y :: (if x then (collect rest) else [])

soln-2014-06-16*> :total collect

corn.collect is Total

Note that Room defined by itself in Idris is a circular-type error. Since every value is typeful and every type is a value (‘valueful’?), then even instances of a (disjoint- or tagged-)type are a type, themselves, so

data Room a = Room (Bool, Bool) a

doesn’t work in Idris, ... at least, it didn’t work for me. So that’s why I ‘Roam’ed about my ‘Room’s for my solution.

But now we look at the problem of ‘shouldbe’ because

sample1 `shouldbe` [1,2]

sample2 `shouldbe` []

sample3 `shouldbe` [‘a’] or type-failure, because the function type is [Room Int] -> [Int] not [Room a] -> [a], amirite?!?!

I’m SO the right.

So here I tried to make the above provable properties. If I could prove the above statements, then I knew my implementation did what I said what it was supposed to do (which, I hope, is what was asked of me, too).

So, my first stab at it was to show decidability. I had gotten wrapped around this axel (of decidability) because from the nGrams problem from before I could show that it was decidable that a String equals a String, but I couldn’t prove a String equaled a String (because there are obvious counterexamples, e.g. “Joe” == “Smart” is false. (sorry, Joe. It’s not personal; it’s just the truth. You are not smart, even if you do (or you don’t) have smarts (as the case may be))).

So I went for decidability, because that worked in the existential case for me before when I was verifying:

isDecEqStr : String -> Bool

isDecEqStr str = case (decEq (concat $ nGrams 1 str) str) of

    Yes (_) => True

    No (_)  => False

For any (existing and non-empty) String str, we can show that it is decidable that

concat $ nGrams 1 str = str

... it’s like a join, right?

Anyway.

So, I thought we can show the decidability of collect over some List (Roam a)

So, we start with

isDecEqRoam : Eq a => List (Roam a) -> List a -> Bool 

isDecEqRoam rooms stuff = (collect rooms) == stuff

and that works fine. But to prove that? Hm. Lessee.

sample1Is12 : { dec : (isDecEqRoam sample1 [1,2]) } -> dec = True

sample1Is12 = refl

Nope. We get the following error when we try to compile our module:

When elaborating type of corn.sample1is12:

Can’t unify Bool with Type

(with the same ‘specifically’)

So, maybe we try ... 

Yeah, I iterated and iterated over decidability until I realized that I could just unify the resulting type of isDecEqRoam with True and I’d be done with it. I didn’t need decidability at all, because I wasn’t deciding that a list of things could equal a list of other (the same) things, no: I was unifying booleans, and that is provable.  Woot!

sample1Is12 : (isDecEqRoam sample1 [1,2]) = True

sample1Is12 = refl

soln-2014-06-16*> sample1Is12

refl : True = True

and so then:

sample2IsEmpty : (isDecEqRoam sample2 []) = True

sample2IsEmpty = refl

soln-2014-06-16*> sample2IsEmpty

refl : True = True

sample3IsA : (isDecEqRoam sample3 [‘a’]) = True

sample3IsA = refl

soln-2014-06-16*> sample3IsA

refl : True = True

YAY! ‘Unit’ ‘testing’ by proofs!

(Granted these are very simple (tautological, in fact) proofs, but I have a warm-fuzzy knowing that I proved my samples are true from my simple collect function. YAY!)

But what does that get us, besides proving what I wrote actually is what I said it would be.

The thing is ... this:

badSample : (isDecEqRoam sample3 [‘b’]) = True

badSample = refl

If I insert the above function (the above proof), the program won’t compile!

By putting these assertions, I’m not (just) ‘unit testing,’ nor am I catching unsafe things at runtime (throwing an ‘AssertionException,’ or whatever, aborting the program instead of allowing the program to proceed under false assumptions). No, I’m doing neither of these things, or, more precisely, I’m doing more than either of those things: much more.

What I am doing is this: I am proving my program is correct, and the proof is that I get a compiled object. The above ‘sampleXisY’ are proof-carry code and I’ve just certified my program as safe and correct for the given samples at compile-time.

Cool story, bro!