Do we need Monad fail (or MonadFail)?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
23 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Do we need Monad fail (or MonadFail)?

Jonathon Delgado
Monads seem to use fail in one of three ways:

-Regular monads leave it at the default definition of error
-MonadPlus sometimes redefines it to mzero
-IO redefines it to failIO

Are there any other definitions of fail? If not, does the special case of IO really need a class-level definition, or
could there be another way of dealing with failed pattern matches?


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Proof in Haskell

Patrick Browne
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@.../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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Do we need Monad fail (or MonadFail)?

Jonathan Geddes
In reply to this post by Jonathon Delgado
I'd love for the compiler to give an error (or maybe just a warning)
in the case that I have a pattern match in a monad that just blows up
(throws an exception) on a pattern match failure.

Currently there's no way to know the behavior of failed pattern match
failures without looking at the instance for the current monad. And
what if you're writing "monad agnostic" (higher-order polymorphism?)
code?

If there were a MonadFail class, you could explicitly codify that you
expect a monad to NOT crash your program in the case of a pattern
match.

For example:

someFunction :: (MonadState m, MonadFail m) => a -> m a
someFunction arg = do
    [x,y,z] <- action arg
    return z

Of course one of the "laws" for MonadFail would be that fail never
throws an exception. The compiler couldn't exactly enforce it, but
we're used to expecting sane instances that obey laws. I think IO
would be the exception (no pun intended) to this and be an instance of
MonadFail, but just throw an exception on fail. Since you can only
catch exceptions in the IO monad, this sounds reasonable to me.

--Jonathan

On Tue, Dec 21, 2010 at 2:49 AM, John Smith <[hidden email]> wrote:

> Monads seem to use fail in one of three ways:
>
> -Regular monads leave it at the default definition of error
> -MonadPlus sometimes redefines it to mzero
> -IO redefines it to failIO
>
> Are there any other definitions of fail? If not, does the special case of IO
> really need a class-level definition, or could there be another way of
> dealing with failed pattern matches?
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Do we need Monad fail (or MonadFail)?

Lauri Alanko
On Tue, Dec 21, 2010 at 08:31:08AM -0700, Jonathan Geddes wrote:
> I'd love for the compiler to give an error (or maybe just a warning)
> in the case that I have a pattern match in a monad that just blows up
> (throws an exception) on a pattern match failure.

You will be interested to know that everything you ask for already was
in Haskell ages ago:

http://www.cs.auckland.ac.nz/references/haskell/haskell-report-1.4-html/exps.html#do-expressions

They decided to get rid of it in Haskell 98, for reasons that someone
else can probably explain.


Lauri

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Do we need Monad fail (or MonadFail)?

Johannes Waldmann
> everything you ask for already was in Haskell ages ago:

those were the days ... where the method in "Functor" method was called "map",
and "zero" was a method of, guess what, "MonadZero"...




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Do we need Monad fail (or MonadFail)?

Jonathan Geddes
In reply to this post by Lauri Alanko

I'd be really interested in learning the rationale behind those changes. I'm sure it wasn't done for capricious or arbitrary reasons, but I can't help but see it as a step back.

--Jonathan Geddes (sent from android mobile)

On Dec 21, 2010 8:47 AM, "Lauri Alanko" <[hidden email]> wrote:

On Tue, Dec 21, 2010 at 08:31:08AM -0700, Jonathan Geddes wrote:
> I'd love for the compiler to give...

You will be interested to know that everything you ask for already was
in Haskell ages ago:

http://www.cs.auckland.ac.nz/references/haskell/haskell-report-1.4-html/exps.html#do-expressions

They decided to get rid of it in Haskell 98, for reasons that someone
else can probably explain.


Lauri


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
...


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

aditya siram-2
In reply to this post by Patrick Browne
I don't know the formal definition, but dependent types seem analogous
to checking an invariant at runtime.
-deech

On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne <[hidden email]> 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@.../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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Iavor Diatchki
Hi Patrick,

Indeed, you cannot really write proofs in Haskell because it is just
an ordinary (more or less) programming language and not a theorem
prover. (As an aside: you could write "tests", i.e. properties which
may or may not be theorems about your program, and test them on random
data (see QuickCheck), or exhaustively---if you managed to test a
property for all possible inputs, then you have essentially proved
it.).

Now about dependent types.  Some programming languages have very
expressive type systems (even more so then Haskell!) and they allow
for types which are parameterized by values.   Such types are called
"dependent types".  Here is an example:

decrement :: (x :: Int) -> (if x > 0 then Int else String)
decrement x = if x > 0 then x - 1 else "Cannot decrement"

This function maps values of type "Int" to either "Int"s or "String"s.
 Note that the _type_ of the result of the function depends on the
_value_ of the input, which is why this function has a dependent type.

It turns out---and this is not at all obvious at first---that
languages with dependent types (and some other features) are suitable
not only for writing programs but, also, for proving theorems.
Theorems are expressed as types (often, dependent types), while proofs
are programs inhabiting the type of the theorem.  So, "true" theorems
correspond to types which have some inhabitants (proofs), while
"false" theorems correspond to empty types.

The correspondence between "proofs-theorems" and "programs-types" is
known as the Curry-Howard isomorphism.  Examples of some languages
which use depend types are Coq, Agda, and Cayenne.

I hope that this helps,
-Iavor

PS: The "forall"s in your example are just depend function types:  in
this setting, to prove "forall (x :: A). P x" amounts writing a
function of type: "(x :: A) -> P x".  In other words, this is a
function, that maps values of type "A" to proofs of the property.
Because the function can be applied to any value of type "A", we have
prove the result "forall (x::A). P x)".   The dependent type arises
because the property depends on the value in question.





On Tue, Dec 21, 2010 at 8:15 AM, aditya siram <[hidden email]> wrote:

> I don't know the formal definition, but dependent types seem analogous
> to checking an invariant at runtime.
> -deech
>
> On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne <[hidden email]> 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@.../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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

austin seipp-3
In reply to this post by Patrick Browne
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 <[hidden email]> 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@.../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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Regards,
Austin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Felipe Lessa
On Tue, Dec 21, 2010 at 3:57 PM, austin seipp <[hidden email]> wrote:
> 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.

You may also write your program, for example, using Coq and then extract correct Haskell code from it.  I'm far from a Coq expert so there must be a better way, but the following works =):

Inductive Tree (A : Type) :=
  | Tip : Tree A
  | Node : Tree A -> A -> Tree A -> Tree A.

Fixpoint mirror {A : Type} (x : Tree A) : Tree A :=
  match x with
  | Tip => Tip A
  | Node l v r => Node A (mirror r) v (mirror l)
  end.

Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
  induction x; simpl; auto.
  rewrite IHx1; rewrite IHx2; trivial.
Qed.

Extraction Language Haskell.
Recursive Extraction mirror.


Then Coq generates the following correct-proven code:

data Tree a = Tip
            | Node (Tree a) a (Tree a)

mirror :: (Tree a1) -> Tree a1
mirror x =
  case x of
    Tip -> Tip
    Node l v r -> Node (mirror r) v (mirror l)

Cheers! =)

--
Felipe.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Daniel Fischer
On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:
>
> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
>   induction x; simpl; auto.
>   rewrite IHx1; rewrite IHx2; trivial.
> Qed.

Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq
doesn't allow infinite structures?


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Daniel Fischer
In reply to this post by Patrick Browne
I wrote:

> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:
>>
>> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
>>   induction x; simpl; auto.
>>   rewrite IHx1; rewrite IHx2; trivial.
>> Qed.

> Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq
> doesn't allow infinite structures?

Oops, mirroring infinite binary trees should work. Ignore above.



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Colin Paul Adams
In reply to this post by Daniel Fischer
>>>>> "Daniel" == Daniel Fischer <[hidden email]> writes:

    Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:
    >>
> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
    >> induction x; simpl; auto.  rewrite IHx1; rewrite IHx2; trivial.
    >> Qed.

    Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take
    Daniel> it that Coq doesn't allow infinite structures?

Why doesn't it hold?
--
Colin Adams
Preston Lancashire
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Daniel Fischer
On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote:
> >>>>> "Daniel" == Daniel Fischer <[hidden email]>
> >>>>> writes:
>
>     Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa
wrote:
> > Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
> >
>     >> induction x; simpl; auto.  rewrite IHx1; rewrite IHx2; trivial.
>     >> Qed.
>
>     Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take
>     Daniel> it that Coq doesn't allow infinite structures?
>
> Why doesn't it hold?

Hit send before I finished thinking, it should hold.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Brandon Moore-2
In reply to this post by Colin Paul Adams




----- Original Message ----

> From: Colin Paul Adams <[hidden email]>
> To: Daniel Fischer <[hidden email]>
> Cc: [hidden email]
> Sent: Tue, December 21, 2010 1:11:37 PM
> Subject: Re: [Haskell-cafe] Proof in Haskell
>
> >>>>> "Daniel" == Daniel Fischer <[hidden email]>  writes:
>
>     Daniel> On Tuesday 21 December 2010 19:34:11,  Felipe Almeida Lessa wrote:
>     >>
> > Theorem  mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
>      >> induction x; simpl; auto.  rewrite IHx1; rewrite IHx2;  trivial.
>     >> Qed.
>
>     Daniel> Since  mirror (mirror x) = x doesn't hold in Haskell, I take
>      Daniel> it that Coq doesn't allow infinite structures?
>
> Why doesn't it  hold?

You are both onto something. It is true, but the Coq proof only covered
finite trees. Infinite tree could be defined with coinduction, but even that
doesn't allow the possibility of bottoms in the tree.

CoInductive Tree (A:Set) :=
  Branch (l r : Tree A) | Leaf.

CoFixpoint mirror {A:Set} (x : Tree A) : Tree A :=
  match x with
  | Leaf => Leaf A
  | Branch l r => Branch A (mirror r) (mirror l)
  end.

Also, you'd have to define some notion of Bisimilarity rather than working
with the direct equality.

CoInductive bisimilar {A : Set} : Tree A -> Tree A -> Prop :=
  | bisim_Leaf : bisimilar (Leaf A) (Leaf A)
  | bisim_Branch (l1 r1 l2 r2 : Tree A) : bisimilar l1 l2 -> bisimilar r1 r2 ->
bisimilar (Branch A l1 r1) (Branch A l2 r2).

I was hoping to write a proof, but it's much more annoying to work with
coinductive definitions.

Brandon



     

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Felipe Lessa
In reply to this post by Daniel Fischer
On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer
<[hidden email]> wrote:
> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:
>>
>> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
>>   induction x; simpl; auto.
>>   rewrite IHx1; rewrite IHx2; trivial.
>> Qed.
>
> Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq
> doesn't allow infinite structures?

Even if the theorem does hold with infinite structures, I don't really
know the answer to your question.  I'm just starting to study Coq in
my free time =).  My guess would be "no", because functions need to be
total.  But that's just a wild guess, and you shouldn't take my word
for it =).

Cheers!

--
Felipe.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Patrick Browne
In reply to this post by Patrick Browne
On 22/12/2010 14:48, Artyom Shalkhakov wrote:
> ..Do you want to prove a property of
> a function formally, using some kind of formal logic?

I am aware that functional languages do not do proofs at term level, but
the motivation for my question is to get a precise reason why this is
so. The replies from the café have clearly articulated the reasons.

Thanks to all,
Pat






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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Sjoerd Visscher-2
In reply to this post by austin seipp-3

On Dec 21, 2010, at 6:57 PM, austin seipp wrote:

> https://gist.github.com/750279

I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape:

https://gist.github.com/752982

Would this count as a function mirror with proof that mirror (mirror x) == x?

--
Sjoerd Visscher



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Daniel Peebles
I think it's pretty legit. You aren't actually making a claim about the values in the tree but I think parametricity handles that for you, especially since you have existential types for the payload at every tree level (so you can't go shuffling those around).

The only thing missing (and that you can't change in Haskell) is that your statement is about Mirror (Mirror x) == x, rather than mirror (mirror x) == x. mirror gives you Mirror but there's currently no proof to show that it's the only way to do it, so there's a missing step there, I think.

Anyway, for those talking about the coinductive proof, I made one in Agda: http://hpaste.org/42516/mirrormirror

Simulating bottoms wouldn't be too hard, but I don't think the statement is even true in the presence of bottoms, is it?

Dan

On Thu, Dec 23, 2010 at 9:27 AM, Sjoerd Visscher <[hidden email]> wrote:

On Dec 21, 2010, at 6:57 PM, austin seipp wrote:

> https://gist.github.com/750279

I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape:

https://gist.github.com/752982

Would this count as a function mirror with proof that mirror (mirror x) == x?

--
Sjoerd Visscher



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Proof in Haskell

Ryan Ingram
On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles <[hidden email]> wrote:
> Simulating bottoms wouldn't be too hard, but I don't think the statement is
> even true in the presence of bottoms, is it?

Isn't it?

data Tree a = Tip | Node (Tree a) a (Tree a)

mirror :: Tree a -> Tree a
mirror Tip = Tip
mirror (Node x y z) = Node (mirror z) y (mirror x)

--

-- base cases
mirror (mirror _|_)
 = mirror _|_
 = _|_

mirror (mirror Tip)
 = mirror Tip
 = Tip

-- inductive case
mirror (mirror (Node x y z))
  = mirror (Node (mirror z) y (mirror x))
  = Node (mirror (mirror x)) y (mirror (mirror z))
  -- induction
  = Node x y z

  -- ryan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12