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?
--
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
On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles pumpkin...@gmail.com 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 =
On Tue, Dec 21, 2010 at 9:57 AM, austin seipp a...@hacks.yi.org wrote:
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'
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.
On Thu,
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
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
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
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 patrick.bro...@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
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
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
On Tue, Dec 21, 2010 at 3:57 PM, austin seipp a...@hacks.yi.org 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
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
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
Daniel == Daniel Fischer daniel.is.fisc...@googlemail.com 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.
On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote:
Daniel == Daniel Fischer daniel.is.fisc...@googlemail.com
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.
- Original Message
From: Colin Paul Adams co...@colina.demon.co.uk
To: Daniel Fischer daniel.is.fisc...@googlemail.com
Cc: haskell-cafe@haskell.org
Sent: Tue, December 21, 2010 1:11:37 PM
Subject: Re: [Haskell-cafe] Proof in Haskell
Daniel == Daniel Fischer daniel.is.fisc
On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer
daniel.is.fisc...@googlemail.com 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.
Hi,
Below is a function that returns a mirror of a tree, originally from:
http://www.nijoruj.org/~as/2009/04/20/A-little-fun.html
where it was used to demonstrate the use of Haskabelle(1) which converts
Haskell programs to the Isabelle theorem prover. Isabelle was used to
show that the Haskell
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.
However, if you manage to express those trees at
One alternative approach is to use QuickCheck to test many trees and
look for counter-examples. You can also use SmallCheck to do an
exhaustive check up to a chosen size of tree.
To do this with QuickCheck you would write a function such as
prop_mirror :: Node a - Bool
prop_mirror x =
On Wednesday 12 November 2008 7:05:02 pm Jonathan Cast wrote:
I think the point is that randomIO is non-deterministic (technically,
pseudo-random) but causal --- the result is completely determined by
events that precede its completion. unsafeInterleaveIO, by contrast, is
arguably (sometimes)
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up that
claim. I know that, in practice, I can't write any counter-examples but
that's a bit handy-wavy. Is there a formal proof that, for all possible
haskell
Lennart Augustsson wrote:
You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
You could use a two step approach: first make a static semantics that
does type
It's possible that there's some more direct approach that
represents types as some kind of runtime values, but nobody
(to my knowledge) has done that.
It don't think its possible - I tried it and failed.
Consider:
show (f [])
Where f has the semantics of id, but has either the return
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On Nov 12, 2008, at 7:09 AM, Lennart Augustsson wrote:
It's possible that there's some more direct approach that represents
types as some kind of runtime values, but nobody (to my knowledge) has
done that.
I think JHC passes types at runtime,
Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up that
claim. I know that, in practice, I can't write any counter-examples but
that's a bit handy-wavy. Is there a formal proof that, for
Correct Lennart. The below mentioned papers assume some
evidence translation of type class programs. If you need/want
a direct semantics/translation of programs you'll need to
impose some restrictions on the set of allowable type class programs.
For such an approach see
Martin Odersky,
I had a quick look at Stuckey and Sulzmann, A Theory of Overloading
and it looks to me like the semantics is given by evidence
translation. So first you do evidence translation, and then give
semantics to the translated program. So this looks like the two step
approach I first mentioned.
Or have
Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up that
claim. I know that, in practice, I can't write any counter-examples but
that's a bit handy-wavy. Is there a formal proof that, for
See What is a purely functional language by Sabry. Not quite a
formal proof about *Haskell*, but then we would first need a formal
semantics of Haskell to be able to do that proof ;-)
On 12 Nov 2008, at 10:11, Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is
On 12 Nov 2008, at 11:11, Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially
transparent? Many people state haskell is RT without backing up
that claim. I know that, in practice, I can't write any counter-
examples but that's a bit handy-wavy. Is
On a totally non-theory side, Haskell isn't referentially transparent.
In particular, any code that calls unsafePerformIO or
unsafeInterleaveIO is not necessarily RT. Given that getContents and
interact use unsafeInterleaveIO, this includes most toy programs as
well as almost every non-toy
On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean [EMAIL PROTECTED] wrote:
Andrew Birkett wrote:
Hi,
Is a formal proof that the Haskell language is referentially transparent?
Many people state haskell is RT without backing up that claim. I know
that, in practice, I can't write any
Hi all,
On Wed, Nov 12, 2008 at 2:09 PM, Lennart Augustsson
[EMAIL PROTECTED]wrote:
You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
...
It's possible that
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Since you are talking to the outside world any behaviour is acceptable.
All the weird interactions between getContents and writing the same
file from the same program could, in principle, happen if a different
program wrote
On 12 Nov 2008, at 14:47, Mitchell, Neil wrote:
It's possible that there's some more direct approach that
represents types as some kind of runtime values, but nobody
(to my knowledge) has done that.
It don't think its possible - I tried it and failed.
Consider:
show (f [])
Where f has
On Wed, Nov 12, 2008 at 12:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Since you are talking to the outside world any behaviour is acceptable.
All the weird interactions between getContents and writing the same
file
You can't write a straightforward dynamic semantics (in, say,
denotational style) for Haskell.
The problem is that with type classes you need to know the types
compute the values.
You could use a two step approach: first make a static semantics that
does type inference/checking and translates
Edsko de Vries wrote:
See What is a purely functional language by Sabry. Not quite a formal
proof about *Haskell*, but then we would first need a formal semantics
of Haskell to be able to do that proof ;-)
Thanks for the reference, and also to everyone who replied - all very
useful and
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which when passed to
ostensibly pure functions yield different results depending on their
evaluation
On Wed, 2008-11-12 at 22:16 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which when passed to
ostensibly pure
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which when passed to
ostensibly pure functions yield different results
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of view.
Really? It seems easy to create things with it which
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of
On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast
[EMAIL PROTECTED] wrote:
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED]
On Wed, 2008-11-12 at 23:18 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 11:05 PM, Jonathan Cast
[EMAIL PROTECTED] wrote:
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12,
On Wed, 2008-11-12 at 23:02 +, David MacIver wrote:
On Wed, Nov 12, 2008 at 10:46 PM, Don Stewart [EMAIL PROTECTED] wrote:
david.maciver:
On Wed, Nov 12, 2008 at 8:35 PM, Lennart Augustsson
[EMAIL PROTECTED] wrote:
Actually, unsafeInterleaveIO is perfectly fine from a RT point of
On Wednesday 12 November 2008 6:18:38 pm David MacIver wrote:
To put it a different way, in the absence of unsafeInterleaveIO the IO
monad has the property that if f and g are observably equal up to
termination then x = f and x = g are equivalent in the IO monad
(actually this may not be true
On Wed, 2008-11-12 at 18:47 -0500, Dan Doel wrote:
On Wednesday 12 November 2008 6:18:38 pm David MacIver wrote:
To put it a different way, in the absence of unsafeInterleaveIO the IO
monad has the property that if f and g are observably equal up to
termination then x = f and x = g are
But how can you tell something being causal or not?
Assuming that all IO operations return random result, of course. :)
From a practical point of view unsafeInterleaveIO can give suspect results.
But theoretically you can't fault it until you have given a semantics
for the IO monad operations so
Interesting posts. Thanks!
On Wed, Nov 12, 2008 at 2:02 PM, Andrew Birkett [EMAIL PROTECTED] wrote:
Thanks for the reference, and also to everyone who replied - all very
useful and interesting. For what it's worth, the blog posts I was writing
are here:
52 matches
Mail list logo
