[Haskell-cafe] Proof in Haskell

[Dan Doel]

On Thursday 23 December 2010 12:52:07 pm Daniel Peebles wrote:
> Fair enough :) that'll teach me to hypothesize something without thinking
> about it! I guess I could amend my coinductive proof:
> 
> http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517
> 
> does that cover bottom-ness adequately? I can't say I've thought through it
> terribly carefully.

That isn't the usual way to model partially defined values. For instance, you 
can write functions with that datatype that would not be monotone:

  pdefined :: {A : Set} -> Tree A -> Bool
  pdefined ⊥ = false
  pdefined _ = true

It's somewhat more accurate to take the partiality monad:

  data D (A : Set) : Set where
    now   : A -> D A
    later : ∞ (D A) -> D A

  ⊥ : {A : Set} -> D A
  ⊥ = later (♯ ⊥)

Then we're interested in an equivalence relation on D As where two values are 
equal if they either both diverge, or both converge to equal inhabitants of A 
(not worrying about how many steps each takes to do so).

Then, the partially defined trees are given by:

  mutual {A}
    Tree = D Tree'

    data Tree' : Set where
      node : Tree -> A -> Tree -> Tree'
      tip  : Tree'

And equivalence of these trees makes use of the above equivalence for D-
wrapped things. (It's actually a little weird that this works, I think, if you 
expect Tree' to be a least fixed point; but Agda does not work that way).

If you're just interested in proving mirror (mirror x) = x, though, this is 
probably overkill. Your original type should be isomorphic to the Haskell type 
in a set theoretic way of thinking, and the definition of mirror does what the 
Haskell function would do at all the values. So the fact that you can write 
functions on that Agda type that would have no corresponding implementation in 
Haskell is kind of irrelevant.

-- Dan