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 (^^
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 Wi
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
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.
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 ac
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 shou
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
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 existe
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
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, 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
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
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 f
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 -> Bo
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
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
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
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
htt
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:
>
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 possib
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, 200
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 w
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 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 thi
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,
the compiler has no problem.
instance Eq (Expr a) where
Const == Const =
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 "informat
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 to
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 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 i
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 hav
My iPhone (iPod Touch, actually) have 1.1.4 firmware, so there isn't
any code signing involved. I've just "configure"d and "make"d.
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 m
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,
> 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 y
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 fácilme
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 pr
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 t
36 matches
Mail list logo
