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 |
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 |
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 |
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 |
> 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 |
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: _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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: I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape: _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
Free forum by Nabble | Edit this page |