[Haskell-cafe] Proof in Haskell

[austin seipp]

Patrick,

Dependent types are program types that depend on runtime values. That
is, they are essentially a type of the form:

f :: (a :: X) -> T

where 'a' is a *value* of type 'X', which is mentioned in the *type* 'T'.

You do not see such things in Haskell, because Haskell separates
values from types - the language of runtime values, and the language
of compile-time values are separate by design. In dependently typed
languages, values and types are in fact, the same terms and part of
the same language, not separated by compiler phases. The distinction
between runtime and compile time becomes blurry at this stage.

By the Curry-Howard isomorphism, we would like to make a proof of some
property, particularly that "mirror (mirror x) = x" - but by CH, types
are the propositions we must prove, and values are the terms we must
prove them with (such as in first-order or propositional logics.) This
is what Eugene means when he says it is not possible to prove this at
the value level. Haskell cannot directly express the following type:

forall a. forall x:Tree a, mirror (mirror x) = x

We can think of the 'forall' parts of the type as bringing the
variables 'a' and 'x' into scope with fresh names, and they are
universally quantified so that this property is established for any
given value of type 'a'. As you can see, this is a dependent type - we
establish we will be using something of type a, and then we establish
that we also have a *value* x of type 'Tree a', which is mentioned
finally by saying that 'mirror (mirror x) = x'.

Because we cannot directly express the above type (as we cannot mix
runtime values and type level values) we cannot also directly express
a proof of such a proposition directly in Haskell.

However, if we can express such a type - that is, a type which can
encode the 'Mirror' function - it is possible to construct a
value-level term which is a proof of such a proposition. By CH, this
is also possible, only not nearly as palatable because we encode the
definition of 'mirror' at the value level as well as the type level -
again, types and values in haskell exist in different realms. With
dependent types we only need to write 'mirror' *once* because we can
use it at both the type and value level. Also, because dependently
typed languages have more expressive type systems in general, it
quickly becomes a burden to do dependent-type 'tricks' in Haskell,
although some are manageable.

For amusement, I went ahead and actually implemented 'Mirror' as a
type family, and used a little bit of hackery thanks to GHC to prove
that indeed, 'mirror x (mirror x) = x' since with a type family we can
express 'mirror' as a type level function via type families. It uses
Ryan Ingram's approach to lightweight dependent type programming in
Haskell.

https://gist.github.com/750279

As you can see, it is quite unsatisfactory since we must encode Mirror
at the type level, as well as 'close off' a typeclass to constrain the
values over which we can make our proof (in GHC, typeclasses are
completely open and can have many nonsensical instances. We could make
an instance for, say 'Mirror Int = Tip', for example, which breaks our
proof. Ryan's trick is to encode 'closed' type classes by using a type
class that implements a form of 'type case', and any instances must
prove that the type being instantiated is either of type 'Tip' or type
'Node' by parametricity.) And well, the tree induction step is just a
little bit painful, isn't it?

So that's an answer, it's just probably not what you wanted.

However, at one point I wrote about proving exactly such a thing (your
exact code, coincidentally) in Haskell, only using an 'extraction
tool' that extracts Isabelle theories from Haskell source code,
allowing you to prove such properties with an automated theorem
prover.

http://hacks.yi.org/~as/posts/2009-04-20-A-little-fun.html

Of course, this depends on the extractor tool itself being correct -
if it is not, it could incorrectly translate your Haskell to similar
but perhaps subtly wrong Isabelle code, and then you'll be proving the
wrong thing! Haskabelle also does support much more than Haskell98 if
I remember correctly, although that may have changed. I also remember
reading that Galois has a project of having 'provable haskell' using
Isabelle, but I can't verify that I suppose.

On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne <patrick.browne at dit.ie> wrote:
> Hi,
> In a previous posting[1] I asked was there a way to achieve a proof of
> mirror (mirror x) = x
>
> in Haskell itself. The code for the tree/mirror is below:
>
>  module BTree where
>  data Tree a = Tip | Node (Tree a) a (Tree a)
>
>  mirror ::  Tree a -> Tree a
>  mirror (Node x y z) = Node (mirror z) y (mirror x)
>  mirror Tip = Tip
>
> The reply from Eugene Kirpichov was:
>>> It is not possible at the value level, because Haskell does not
>>> support dependent types and thus cannot express the type of the
>>> proposition
>>> "forall a . forall x:Tree a, mirror (mirror x) = x",
>>> and therefore a proof term also cannot be constructed.
>
> Could anyone explain what *dependent types* mean in this context?
> What is the exact meaning of forall a and forall x?
>
> Thanks,
> Pat
> [1] http://www.mail-archive.com/haskell-cafe@haskell.org/msg64842.html
>
>
>
>
>
>
>
>
> This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Regards,
Austin