Does it make sense to use proof to validate that a given monad
implementation obeys its laws?
daryoush
2008/9/14 Greg Meredith [EMAIL PROTECTED]:
Daryoush,
One of the subtle points about computation is that -- via Curry-Howard --
well-typed programs are already proofs. They may not be the
Hola amigos del Foro ( México ), alguno de ustedes
sabe donde se puede adquirir en nuestro país pedacitos
de fibra de coco, lo que en inglés llaman coconut
husk chips...??
He tenido noticia acerca de su uso exitoso como
ingrediente en la preparación de sustrato, en USA se
puede conseguir
I have the same problems. Looks like the configure script needs some
updating to run on the iPhone.
On Mon, Sep 15, 2008 at 6:47 AM, Alberto R. Galdo
[EMAIL PROTECTED] wrote:
Cool! That's such a proof that it can be done...
I had lots of problems trying to cross compile hugs from my mac to
I recommend reading Conal Elliott's Efficient Functional Reactivity
paper for an in-depth real-world example.
http://www.conal.net/papers/simply-reactive
-- ryan
On Sun, Sep 14, 2008 at 11:31 AM, Daryoush Mehrtash [EMAIL PROTECTED] wrote:
I have been told that for a Haskell/Functional
A more difficult question is: how do I know that the formal
specification I've written for my program is the right one? Tools can
fairly easily check that your programs conform to a given
specification, but they cannot (to my knowledge) check that your
specification says exactly what you
On Mon, 15 Sep 2008 10:32:44 -0400
Stefan Monnier [EMAIL PROTECTED] wrote:
A more difficult question is: how do I know that the formal
specification I've written for my program is the right one? Tools
can fairly easily check that your programs conform to a given
specification, but they
Richard A. O'Keefe wrote:
On 14 Sep 2008, at 10:59 pm, Rafael Almeida wrote:
One thing have always bugged me: how do you prove that you have
correctly proven something?
This really misses the point of trying to formally verify something.
That point is that you almost certainly have NOT.
My iPhone (iPod Touch, actually) have 1.1.4 firmware, so there isn't
any code signing involved. I've just configured and maked.
On 15 Sep 2008, at 09:47, Alberto R. Galdo wrote:
Cool! That's such a proof that it can be done...
I had lots of problems trying to cross compile hugs from my mac
On Mon, 15 Sep 2008 13:05:11 -0300
Rafael C. de Almeida [EMAIL PROTECTED] wrote:
I do not know. I'm not experienced on the field and I was under the
impression you'd write your code then get a pen and a paper and try to
prove some property of it.
In fairness, that's how it's often done in
Interestingly, I was trying to read his paper when I realized that I
needed to figure out the meaning of denotational model, semantic
domain, semantic functions. Other Haskell books didn't talk about
design in those terms, but obviously for him this is how he is driving
his design. I am looking
On Sep 15, 2008, at 10:43 AM, Robin Green wrote:
In fairness, that's how it's often done in universities (where
correctness doesn't really matter to most people - no offense
intended). But once you start using software to write formal proofs,
it
is quite easy in principle to get a computer
Here's a quick overview that might help you.
For a reactive behavior, we have two types to think about:
type B a = Time - a
(the semantic domain)
data Behavior a = ?
(the library's implementation).
at :: Behavior a - B a
(observation function)
This is really just classic
On Mon, Sep 15, 2008 at 11:01 AM, Tom Hawkins [EMAIL PROTECTED] wrote:
Hi,
How do I compare a GADT type if a particular constructor returns a
concrete type parameter?
For example:
data Expr :: * - * where
Const :: Expr a
Equal :: Expr a - Expr a - Expr Bool -- If this read Expr a,
On Mon, Sep 15, 2008 at 2:43 PM, Robin Green [EMAIL PROTECTED] wrote:
On Mon, 15 Sep 2008 13:05:11 -0300
Rafael C. de Almeida [EMAIL PROTECTED] wrote:
Someone mentioned coq, I read a bit about it, but it looked really
foreign to me. The idea is to somehow prove somethings based only on
the
You mean like this?
import Data.List (foldl', nub)
Or am I misunderstanding your question?
Paulo
On Mon, Sep 15, 2008 at 2:26 PM, Mauricio [EMAIL PROTECTED] wrote:
Hi,
'import' allows one to say 'hiding' to
a list of names. Is it possible to do the
opposite, i.e., list the names I want to
Yes, just leave out the keyword hiding.
import Data.Map (Map, insert, lookup)
This is the safest way to do imports as you're guaranteed that
changes to the export list that do not affect those qualifiers won't
cause code to stop compiling or become ambiguous.
-- ryan
On Mon, Sep 15, 2008 at
Exactly! Thanks.
Maurício
Paulo Tanimoto a écrit :
You mean like this?
import Data.List (foldl', nub)
Or am I misunderstanding your question?
Paulo
On Mon, Sep 15, 2008 at 2:26 PM, Mauricio [EMAIL PROTECTED] wrote:
Hi,
'import' allows one to say 'hiding' to
a list of names. Is it
You're welcome. By the way, this page seems pretty comprehensive.
http://www.haskell.org/haskellwiki/Import
Also, if my memory serves me, Neil Mitchel raised a question about
extending the import system not long ago.
Paulo
On Mon, Sep 15, 2008 at 2:41 PM, Mauricio [EMAIL PROTECTED] wrote:
Hi,
'import' allows one to say 'hiding' to
a list of names. Is it possible to do the
opposite, i.e., list the names I want to
import? Something like import Module showing x?
Thanks,
Maurício
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
Would it make sense to add multiple imports to that wiki page? I'm not sure
if this is supported outside of GHC, but I've found it useful.
1 module Main where
2
3 import qualified Prelude as P
4 import Prelude ((++),show,($))
5
6 main = P.putStrLn (show $ P.length $ show $ [1] ++ [2,3])
On
Jason Dagit wrote:
Tom Hawkins wrote:
How do I compare a GADT type if a particular constructor returns a
concrete type parameter?
For example:
data Expr :: * - * where
Const :: Expr a
Equal :: Expr a - Expr a - Expr Bool -- If this read Expr a,
the compiler has no problem.
On Mon, Sep 15, 2008 at 3:04 PM, John Van Enk [EMAIL PROTECTED] wrote:
Would it make sense to add multiple imports to that wiki page? I'm not sure
if this is supported outside of GHC, but I've found it useful.
1 module Main where
2
3 import qualified Prelude as P
4 import Prelude
On Mon, Sep 15, 2008 at 3:11 PM, apfelmus [EMAIL PROTECTED] wrote:
So, in other words, in order to test whether terms constructed with Equal
are
equal, you have to compare two terms of different type for equality. Well,
nothing easier than that:
(===) :: Expr a - Expr b - Bool
Take a look at
http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap
Tom Hawkins wrote:
On Mon, Sep 15, 2008 at 3:11 PM, apfelmus [EMAIL PROTECTED] wrote:
So, in other words, in order to test whether terms constructed with Equal are
equal, you have to compare two terms of different type
Hi,
I tested the expression below
and it doesn't work. Is there
some way to achieve that (i.e.,
turning an expression inside
parenthesis into an operator)?
2 `(flip (^^))` (3%4)
Thanks,
Maurício
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
On Mon, Sep 15, 2008 at 2:25 PM, Tom Hawkins [EMAIL PROTECTED] wrote:
OK. But let's modify Expr so that Const carries values of different types:
data Expr :: * - * where
Const :: a - Term a
Equal :: Term a - Term a - Term Bool
How would you then define:
Const a === Const b = ...
You
On Mon, 15 Sep 2008, Tom Hawkins wrote:
OK. But let's modify Expr so that Const carries values of different types:
data Expr :: * - * where
Const :: a - Term a
Equal :: Term a - Term a - Term Bool
How would you then define:
Const a === Const b = ...
Apart from the suggestions about
On Mon, 2008-09-15 at 18:42 -0300, Mauricio wrote:
Hi,
I tested the expression below
and it doesn't work. Is there
some way to achieve that (i.e.,
turning an expression inside
parenthesis into an operator)?
2 `(flip (^^))` (3%4)
No it shouldn't work. The fact that the opening and
On Mon, Sep 15, 2008 at 2:50 PM, Ryan Ingram [EMAIL PROTECTED] wrote:
There are many papers that talk about using GADTs to reify types in
this fashion to allow safe typecasting. They generally all rely on
the base GADT, TEq; every other GADT can be defined in terms of
TEq and existential
Derek Elkins wrote:
On Mon, 2008-09-15 at 18:42 -0300, Mauricio wrote:
Hi,
I tested the expression below
and it doesn't work. Is there
some way to achieve that (i.e.,
turning an expression inside
parenthesis into an operator)?
2 `(flip (^^))` (3%4)
No it shouldn't work. The fact that
Rafael C. de Almeida a écrit :
Derek Elkins wrote:
On Mon, 2008-09-15 at 18:42 -0300, Mauricio wrote:
Hi,
I tested the expression below
and it doesn't work. Is there
some way to achieve that (i.e.,
turning an expression inside
parenthesis into an operator)?
2 `(flip (^^))` (3%4)
No it
On Mon, Sep 15, 2008 at 8:09 PM, Mauricio [EMAIL PROTECTED] wrote:
Rafael C. de Almeida a écrit :
Derek Elkins wrote:
On Mon, 2008-09-15 at 18:42 -0300, Mauricio wrote:
Hi,
I tested the expression below
and it doesn't work. Is there
some way to achieve that (i.e.,
turning an
On Mon, Sep 15, 2008 at 2:53 PM, Ganesh Sittampalam [EMAIL PROTECTED] wrote:
Apart from the suggestions about Data.Typeable etc, one possibility is to
enumerate the different possible types that will be used as parameters to
Const in different constructors, either in Expr or in a new type.
So
Tom Hawkins wrote:
data Expr :: * - * where
Const :: a - Term a
Equal :: Term a - Term a - Term Bool
Your basic problem is this:
p1 :: Term Bool
p1 = Equal (Const 3) (Const 4)
p2 :: Term Bool
p2 = Equal (Const yes) (Const no)
p1 and p2 have the same type, but you're not going
Ryan Ingram wrote:
There are many papers that talk about using GADTs to reify types in
this fashion to allow safe typecasting. They generally all rely on
the base GADT, TEq; every other GADT can be defined in terms of
TEq and existential types.
Ah, yes. See my paper Witnesses and Open
Mauricio wrote:
Hi,
I tested the expression below
and it doesn't work. Is there
some way to achieve that (i.e.,
turning an expression inside
parenthesis into an operator)?
2 `(flip (^^))` (3%4)
Another solution if you don't like defining extra (-|) and (|-)
operators is:
($2) (flip
36 matches
Mail list logo
