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 t
As pie. Just downloaded the source and compiled it on iPhone itself
(no cross-compiling).
On 15 Sep 2008, at 09:25, Don Stewart wrote:
Very nice. Easy?
miguelimo38:
Did that.
http://migmit.vox.com/library/photo/6a00e398c5c26f000500fa9696d8c40002.html
On 14 Sep 2008, at 14:17, Alberto R. G
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 arm
architecture ( seems that hugs codebase is not capable of cross
compiling )
And when compiling directly on the iPhone, first there where problems
with code signing, now
Very nice. Easy?
miguelimo38:
> Did that.
> http://migmit.vox.com/library/photo/6a00e398c5c26f000500fa9696d8c40002.html
>
> On 14 Sep 2008, at 14:17, Alberto R. Galdo wrote:
>
> >Hi, is there any chance of having hugs compile for the iPhone?
> >
> >Cross-compiling? Compiling directly on the i
Did that.
http://migmit.vox.com/library/photo/6a00e398c5c26f000500fa9696d8c40002.html
On 14 Sep 2008, at 14:17, Alberto R. Galdo wrote:
Hi, is there any chance of having hugs compile for the iPhone?
Cross-compiling? Compiling directly on the iPhone?
Greets,
Alberto
_
On 15 Sep 2008, at 12:51 pm, Daniel Fischer wrote:
Am Montag, 15. September 2008 02:24 schrieb Cetin Sert:
Hi why do I get?
Buffering. For compiled programmes, stdin and stdout are line-
buffered by
default, so the output doesn't appear until the program finishes.
Either put
hSetBuffering
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. By the time you
get a theorem p
On 2008 Sep 14, at 20:47, Brandon S. Allbery KF8NH wrote:
On 2008 Sep 14, at 20:24, Cetin Sert wrote:
Hi why do I get?
[EMAIL PROTECTED]:~/lab/exp/1> ./eq
23
23
3
a = b = c = n1-0.8457820374040622n2-0.1542179625959377
As is typical for Unix, filehandles including standard input and
standard
Am Montag, 15. September 2008 02:24 schrieb Cetin Sert:
> Hi why do I get?
Buffering. For compiled programmes, stdin and stdout are line-buffered by
default, so the output doesn't appear until the program finishes.
Either put
hSetBuffering stdout NoBuffering
at the top of main or, better IMO,
ins
Hello,
If we look at these two examples, it appears that the results are reversed:
Prelude> let n o = (-1 `o` 1) in n (-)
0
Prelude> let n o = (-1 `o` 1) in n (+)
-2
Prelude>
we expect (-1 - 1) = -2 and (-1 + 1) = 0, but we get the opposite.
Due to operator precedence, the equations are being
On 2008 Sep 14, at 20:24, Cetin Sert wrote:
Hi why do I get?
[EMAIL PROTECTED]:~/lab/exp/1> ./eq
23
23
3
a = b = c = n1-0.8457820374040622n2-0.1542179625959377
As is typical for Unix, filehandles including standard input and
standard output are line buffered. See hSetBuffering ( http://www.
Hi why do I get?
[EMAIL PROTECTED]:~/lab/exp/1> ./eq
23
23
3
a = b = c = n1-0.8457820374040622n2-0.1542179625959377
when I run
import System.IO
main :: IO ()
main = do
a ← ask "a"
b ← ask "b"
c ← ask "c"
eval a b c
ask v = do
putStr (v ++ " = ")
readLn
eval a b c = do
case delta
Em Dom, 2008-09-14 às 14:52 -0700, Don Stewart escreveu:
> marcot:
> > Em Dom, 2008-09-14 às 16:07 -0300, Marco Túlio Gontijo e Silva escreveu:
> > > Thanks, I got it to work running
> > >
> > > threadWaitRead stdInput
> > >
> > > before getChar.
> >
> > Now I've got another problem:
> >
> > >
marcot:
> Em Dom, 2008-09-14 às 16:07 -0300, Marco Túlio Gontijo e Silva escreveu:
> > Thanks, I got it to work running
> >
> > threadWaitRead stdInput
> >
> > before getChar.
>
> Now I've got another problem:
>
> > import Control.Concurrent
> > import System.IO
> > import System.Process
>
>
Em Dom, 2008-09-14 às 16:07 -0300, Marco Túlio Gontijo e Silva escreveu:
> Thanks, I got it to work running
>
> threadWaitRead stdInput
>
> before getChar.
Now I've got another problem:
> import Control.Concurrent
> import System.IO
> import System.Process
> main :: IO ()
> main
> = do
>
Daryoush,
One of the subtle points about computation is that -- via Curry-Howard --
well-typed programs are *already* proofs. They may not be the proof you were
seeking (there are a lot of programs from Int -> Int), or prove the theorem
you were seeking to prove (Ord a => [a] -> [a] is a lot weake
Simon Richard Clarkstone <[EMAIL PROTECTED]> writes:
>> I can also do
>>
>> readFile "readme.markdown" <.> lines <.> length
>>
>> by making
(<.>) = flip fmap
?
-k
--
If I haven't seen further, it is by standing in the footprints of giants
___
Haske
Andrea Rossato wrote:
On Sun, Sep 14, 2008 at 02:24:23PM -0300, Marco Túlio Gontijo e Silva wrote:
and the result of ls only after I press a key. Does getChar blocks the
other threads?
yes, but you can use forkOS from Control.Concurrent and compile with
-threaded.
See the relevant documentat
Em Dom, 2008-09-14 às 11:08 -0700, Judah Jacobson escreveu:
> On Sun, Sep 14, 2008 at 10:24 AM, Marco Túlio Gontijo e Silva
> <[EMAIL PROTECTED]> wrote:
> <
> > When I run this code, I get
> >
> > fork
> >
> > and the result of ls only after I press a key. Does getChar blocks the
> > other threads
Hi,
On Sun, Sep 14, 2008 at 7:01 AM, Stephan Friedrichs
<[EMAIL PROTECTED]> wrote:
> I agree that the MonadZero class with a useful 'zero' :: m a would be
> the right abstraction for views. But MonadZero is not part of base, mtl
> or any other common package, or am I missing something? Changing th
Daryoush Mehrtash gmail.com> writes:
>
> I have been told that for a Haskell/Functional programmer the process
> of design starts with defining Semantic Domain, Function, and
> denotational model of the problem. I have done some googling on the
> topic but haven't found a good reference on it.
I have been told that for a Haskell/Functional programmer the process
of design starts with defining Semantic Domain, Function, and
denotational model of the problem. I have done some googling on the
topic but haven't found a good reference on it.I would appreciate
any good references on the t
jinjing wrote:
I found that as I can do
xs.map(+1).sort
by redefine . to be
a . f = f a
infixl 9 .
This looks rather like ($), but backwards. I believe the F# name for
this operator is (|>), which is also a legal name for it in Haskell.
Odd, since (|) alone isn't legal. Calling it
At Sun, 14 Sep 2008 12:17:52 +0200,
Alberto R. Galdo wrote:
>
> Hi, is there any chance of having hugs compile for the iPhone?
>
> Cross-compiling? Compiling directly on the iPhone?
I have successfully compiled hugs for the Nokia 770 which is ARM
based. I don't remember having to do anything sp
On Sun, Sep 14, 2008 at 10:24 AM, Marco Túlio Gontijo e Silva
<[EMAIL PROTECTED]> wrote:
<
> When I run this code, I get
>
> fork
>
> and the result of ls only after I press a key. Does getChar blocks the
> other threads?
>
I think this behavior is caused by (or at least related to) the
following
On Sun, Sep 14, 2008 at 02:24:23PM -0300, Marco Túlio Gontijo e Silva wrote:
> and the result of ls only after I press a key. Does getChar blocks the
> other threads?
yes, but you can use forkOS from Control.Concurrent and compile with
-threaded.
See the relevant documentation for the details.
Hello.
> import System.Cmd
> import GHC.Conc
>
> main :: IO ()
> main
> = forkIO
> ( do
> putStrLn "fork"
> system "ls"
> return ())
> >> getChar
> >> return ()
When I run this code, I get
fork
and the result of ls only after I press a key. Does getChar b
Cetin Sert wrote:
main = do
as <- getArgs
[...]
where
lo = read $ as !! 0
hi = read $ as !! 1
tx =as !! 2
Why is as not visible in the where block?
The where-block is outside the do-block. (Indentation cannot change that
fact.)
_
On 2008 Sep 14, at 10:01, Stephan Friedrichs wrote:
Johannes Waldmann wrote:
I think the crux of
the matter was that a monad is too general. Either there is a
result or
there is not. That's precisely the intended use of a Maybe.
Indeed "Monad m =>" is dangerous here
because not every Monad
On Sunday 14 September 2008 6:59:06 am Rafael Almeida wrote:
> One thing have always bugged me: how do you prove that you have
> correctly proven something? I mean, when I write a code I'm formaly
> stating what I want to happen and bugs happen. If I try to prove some
> part of the code I write mor
Seems that someone in this list got hugs working on the iPhone...
http://www.nabble.com/Re%3A-xmonad-on-the-openmoko-mobile-phone-p18914746.html
Miguel, are you out there?
On Sun, Sep 14, 2008 at 4:56 PM, Braden Shepherdson <
[EMAIL PROTECTED]> wrote:
> Braden Shepherdson wrote:
>
>> Alberto R.
On Sun, 2008-09-14 at 14:41 +0100, Neil Mitchell wrote:
> Hi
>
> Ignore the previous email message, as soon as I sent the email it
> started working - I guess it was just code.haskell.org server issues.
Yes it was unavailable for a short time yesterday. It got rebooted by
the hosting company, we'
Braden Shepherdson wrote:
Alberto R. Galdo wrote:
Hi, is there any chance of having hugs compile for the iPhone?
Cross-compiling? Compiling directly on the iPhone?
Greets,
Alberto
The iPhone, like most modern mobile devices, is based on the ARM
processor, for which there is currently no GH
Alberto R. Galdo wrote:
Hi, is there any chance of having hugs compile for the iPhone?
Cross-compiling? Compiling directly on the iPhone?
Greets,
Alberto
The iPhone, like most modern mobile devices, is based on the ARM
processor, for which there is currently no GHC port.
However, jhc outp
Johannes Waldmann wrote:
>> I think the crux of
>> the matter was that a monad is too general. Either there is a result or
>> there is not. That's precisely the intended use of a Maybe.
>
> Indeed "Monad m =>" is dangerous here
> because not every Monad has a reasonable definition of "fail".
>
>
Hi
Ignore the previous email message, as soon as I sent the email it
started working - I guess it was just code.haskell.org server issues.
Thanks
Neil
On 9/14/08, Neil Mitchell <[EMAIL PROTECTED]> wrote:
> Hi
>
> I'm currently unable to push to [EMAIL PROTECTED]:/srv/code/hoogle
> using darcs
Hi
I'm currently unable to push to [EMAIL PROTECTED]:/srv/code/hoogle
using darcs 1.0.9 on Windows Vista, and wasn't able to yesterday
either. Is code.haskell.org just being slow, or is there a chance
that Hoogle suffered as a result of the upgrade?
Thanks
Neil
On 9/11/08, Eric Y. Kow <[EMAIL
I think the crux of
the matter was that a monad is too general. Either there is a result or
there is not. That's precisely the intended use of a Maybe.
Indeed "Monad m =>" is dangerous here
because not every Monad has a reasonable definition of "fail".
But that seems to be a problem in the (c
Johannes Waldmann wrote:
>> a) ... to use Maybe
>> b) ... to provide my own Data.Heap.View type
>
> leave the choice up to the programmer,
> and provide a generic interface,
> accepting any MonadZero (*) instance.
>
> cf. Data.Set.maxView
AFAIK there has been a vivid discussion about that. I thi
2008/9/14 Rafael Almeida <[EMAIL PROTECTED]>:
>
> One thing have always bugged me: how do you prove that you have
> correctly proven something? I mean, when I write a code I'm formaly
> stating what I want to happen and bugs happen. If I try to prove some
> part of the code I write more formal text
2008/9/14 John Goerzen <[EMAIL PROTECTED]>:
> 2) Variable x defined but not used
>
> I most often ignore this when it occurs in a function definition.
> Sometimes I may have a function that could be written
>
> foo _ (x, _) _ = bar (x + 5)
>
> But for clarity's sake on what all the unused args are,
On Sun, Sep 14, 2008 at 5:56 AM, Thomas M. DuBuisson
<[EMAIL PROTECTED]> wrote:
>
>> What would theorem proofs do for me?
> Imagine if you used SmallCheck to exhastively test the ENTIRE problem
> space for a given property. Now imagine you used your brain to show the
> programs correctness before
Hi, is there any chance of having hugs compile for the iPhone?
Cross-compiling? Compiling directly on the iPhone?
Greets,
Alberto
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
I'm building a "really static" executable on OS X with options
`-optl-static -static` and, while the libraries seem to link
fine, the executable itself does not -- it can't find the C
runtime.
This is actually by design -- Apple "does not support" static
binaries. There is a work aroun
44 matches
Mail list logo
