Re: [Haskell-cafe] Proving programs

2013-01-02 Thread AUGER Cédric
Le Tue, 01 Jan 2013 14:24:04 -0900, Christopher Howard christopher.how...@frigidcode.com a écrit : I'm working through a video lecture describing how to prove programs correct, by first translating the program into a control flow representation and then using propositional logic. In the

Re: [Haskell-cafe] Category Theory and Haskell

2012-11-30 Thread AUGER Cédric
Le Sun, 25 Nov 2012 21:41:47 +, Gytis Žilinskas gytis.zilins...@gmail.com a écrit : Greetings, I'm only taking my very first steps learning Haskell, but I believe that this mailing list might be appropriate for my question. How difficult would it be to study category theory and

Re: [Haskell-cafe] Compilers: Why do we need a core language?

2012-11-20 Thread AUGER Cédric
Le Tue, 20 Nov 2012 06:54:25 -0500 (EST), c...@lavabit.com a écrit : Hello, I know nothing about compilers and interpreters. I checked several books, but none of them explained why we have to translate a high-level language into a small (core) language. Is it impossible (very hard) to

Re: [Haskell-cafe] Compilers: Why do we need a core language?

2012-11-20 Thread AUGER Cédric
Le Tue, 20 Nov 2012 10:49:01 -0500 (EST), c...@lavabit.com a écrit : What would be the point in doing so? Well, I don't know. Would it save some time? Why bother with a core language? The compilation process might be slightly faster, but I guess it wouldn't be much noticeable. Also I

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

2012-10-24 Thread AUGER Cédric
Le Wed, 24 Oct 2012 12:36:52 +0700, Kim-Ee Yeoh k...@atamo.com a écrit : On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric sedri...@gmail.com wrote: As I said, from the mathematical point of view, join (often noted μ in category theory) is the (natural) transformation which with return (η

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

2012-10-16 Thread AUGER Cédric
composition is the holy grail, why not encourage the monadic code, too, to be compositional? Nicety can wait; some syntax sugar might take care of it. And as you have pointed out, arrows make a superior choice in this regard, but they are rather newer to monads. @ AUGER Cédric It would

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

2012-10-16 Thread AUGER Cédric
Le Tue, 16 Oct 2012 09:51:29 -0400, Jake McArthur jake.mcart...@gmail.com a écrit : On Mon, Oct 15, 2012 at 11:29 PM, Dan Doel dan.d...@gmail.com wrote: I'd be down with putting join in the class, but that tends to not be terribly important for most cases, either. Join is not the most

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

2012-10-16 Thread AUGER Cédric
… On Tue, Oct 16, 2012 at 10:37 AM, AUGER Cédric sedri...@gmail.com wrote: Le Tue, 16 Oct 2012 09:51:29 -0400, Jake McArthur jake.mcart...@gmail.com a écrit : On Mon, Oct 15, 2012 at 11:29 PM, Dan Doel dan.d...@gmail.com wrote: I'd be down with putting join in the class

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

2012-10-16 Thread AUGER Cédric
Le Tue, 16 Oct 2012 11:58:44 -0400, Dan Doel dan.d...@gmail.com a écrit : On Tue, Oct 16, 2012 at 10:37 AM, AUGER Cédric sedri...@gmail.com wrote: join IS the most important from the categorical point of view. In a way it is natural to define 'bind' from 'join', but in Haskell

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

2012-10-15 Thread AUGER Cédric
Le Mon, 15 Oct 2012 15:12:28 +0200, Benjamin Franksen benjamin.frank...@helmholtz-berlin.de a écrit : Ertugrul Söylemez wrote: damodar kulkarni kdamodar2...@gmail.com wrote: The Monad class makes us define bind (=) and unit (return) for our monads. Why the Kleisli composition (=) or

Re: [Haskell-cafe] Haskell with all the safeties off

2012-09-08 Thread AUGER Cédric
Le Sat, 8 Sep 2012 09:20:29 +0100, Ramana Kumar ramana.ku...@cl.cam.ac.uk a écrit : On Fri, Sep 7, 2012 at 5:56 PM, Edward Z. Yang ezy...@mit.edu wrote: Excerpts from David Feuer's message of Fri Sep 07 12:06:00 -0400 2012: They're not *usually* desirable, but when the code has been

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-06 Thread AUGER Cédric
Le Fri, 6 Jan 2012 10:59:29 +0100, Yves Parès limestr...@gmail.com a écrit : 2012/1/6 AUGER Cédric sedri...@gmail.com when you write forall a. exists b. a - b - a, then you allow the caller to have access to b to produce a (didn't you write a-b-a?) Yes, sorry, I always assumed

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-04 Thread AUGER Cédric
Le Tue, 3 Jan 2012 20:46:15 +0100, Yves Parès limestr...@gmail.com a écrit : Actually, my question is why the different type can't be unified with the inferred type? Because without ScopedTypeVariable, both types got expanded to : legSome :: *forall nt* t s. LegGram nt t s - nt -

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-04 Thread AUGER Cédric
So is there anyway to force the scoping of variables, so that f :: a - a f x = x :: a becomes valid? Do we need to do it the Ocaml way, that is not declaring the first line, activate XScopedVariables and do: f :: a - a = \x - x :: a or f (x :: a) = x :: a or some other thing ? I don't see the

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-04 Thread AUGER Cédric
Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès limestr...@gmail.com a écrit : I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-04 Thread AUGER Cédric
Le Wed, 4 Jan 2012 16:22:31 +0100, Yves Parès limestr...@gmail.com a écrit : Oleg explained why those work in his last post. It's the exact same logic for each one. f :: a - a f x = x :: a We explained that too: it's converted (alpha-converted, but I don't exactly know what 'alpha'

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-04 Thread AUGER Cédric
doesn't appear in the introduced type). 2012/1/4 AUGER Cédric sedri...@gmail.com Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès limestr...@gmail.com a écrit : I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

[Haskell-cafe] Solved but strange error in type inference

2012-01-03 Thread AUGER Cédric
Hi all, I am an Haskell newbie; can someone explain me why there is no reported error in @legSome@ but there is one in @legSomeb@ (I used leksah as an IDE, and my compiler is: $ ghc -v Glasgow Haskell Compiler, Version 7.2.1, stage 2 booted by GHC version 6.12.3 ) What I do not understand is

Re: [Haskell-cafe] Solved but strange error in type inference

2012-01-03 Thread AUGER Cédric
Thanks all, I finally give up to put Ord in the LegGram type. What was annoying me was that @legsome@ was in fact an instance of a class I defined. So I changed its signature to make it depend on Ord. That is not very nice, since at first glance, there could be implementations which does not

Re: [Haskell-cafe] On the purity of Haskell

2012-01-01 Thread AUGER Cédric
Le Sun, 1 Jan 2012 16:31:51 -0500, Dan Doel dan.d...@gmail.com a écrit : On Sun, Jan 1, 2012 at 3:26 PM, Ketil Malde ke...@malde.org wrote: Chris Smith cdsm...@gmail.com writes: I wonder: can writing to memory be called a “computational effect”? If yes, then every computation is impure.

Re: [Haskell-cafe] On the purity of Haskell

2011-12-29 Thread AUGER Cédric
struggling with anything else today. Maybe a third try... On 28/12/2011 19:38, AUGER Cédric wrote: Le Wed, 28 Dec 2011 17:39:52 +, Steve Hornesh006d3...@blueyonder.co.uk a écrit : This is just my view on whether Haskell is pure, being offered up for criticism. I haven't seen this view

Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?

2011-12-28 Thread AUGER Cédric
Le Mon, 26 Dec 2011 19:30:20 -0800, Alexander Solla alex.so...@gmail.com a écrit : So we give meaning to syntax through our semantics. That is what this whole conversation is all about. I am proposing we give Haskell bottoms semantics that bring it in line with the bottoms from various

Re: [Haskell-cafe] On the purity of Haskell

2011-12-28 Thread AUGER Cédric
Le Wed, 28 Dec 2011 17:39:52 +, Steve Horne sh006d3...@blueyonder.co.uk a écrit : This is just my view on whether Haskell is pure, being offered up for criticism. I haven't seen this view explicitly articulated anywhere before, but it does seem to be implicit in a lot of explanations -