Re: [Haskell-cafe] Is (==) commutative?
On 7/25/12, Christian Sternagel c.sterna...@gmail.com wrote: Dear Alexander, On 07/26/2012 01:09 PM, Alexander Solla wrote: On 7/25/12, Christian Sternagel c.sterna...@gmail.com wrote: On 07/26/2012 11:53 AM, Alexander Solla wrote: The classically valid inference: (x == y) = _|_ = (y == x) = _|_ Btw: whether this inference is valid or not depends on the semantics of (==) and that's exactly what I was asking about. In Haskell we just have type classes, thus (==) is more or less arbitrary (apart from its type). Indeed. This is true for the interpretation of any function. But you apparently want to treat (==) as equality. This may or may not be possible, depending on the interpretation you choose. Does _|_ == _|_, or _|_ =/= _|_, or do these questions not even make semantic sense in the object language? That's what you need to answer, and the solution to your problem will become clear. Note that picking any of these commits you to a philosophical position, insofar as the commitment will induce a metalanguage which excludes expressions from other metalanguages. for my specific case (HOLCF) there is already a fixed metalanguage which has logical equality (=) and differentiates between type 'bool' (True, False) for logical truth and type 'tr' (TT, FF, _|_) for truth-valued computable functions (including nontermination/error). Logical equality satisfies '_|_ = _|_'. Now in principle (==) is just an arbitrary function (for each instance) but I gather that there is some intended use for the type class Eq (and I strongly suspect that it is to model equality ;), I merely want to find out to what extend it does so). Yes, in my opinion, its purpose is to model mathematical/logical equality. That said, you brought up a very important point which you need to address. I'll discuss it more below. I will be using scare-quotes quite a bit. I'm not being sarcastic -- please ask if you don't understand what I mean. Currently the axioms of the formal eq class include (_|_ == y) = _|_ (x == _|_) = _|_ (and this decision was just based on how ghci evaluates corresponding expressions). The equations you use above would be (roughly) written '(_|_ == _|_) = TT' and '(_|_ /= _|_) = TT' in HOLCF and neither of them is satisfied, since both expressions are logically equivalent to _|_ (in HOLCF). (But still both expressions make sense.) Okay, you have a metalanguage. And it places limits on what you can express. But you can also put limits on what you can express, to induce a sublanguage of the metalanguage. I don't know how natural this idea is given your circumstances and goals, but you may want to consider it. I promise I'll get to the meat of my email soon. During the discussion I revisited the other two axioms I was using for eq... and now I am wondering whether those make sense. The other two axioms where (x == y) = TT == x = y (x == y) = FF == not (x = y) The second one should be okay, but the first one is not true in general, since it assumes that we would only ever use Eq instances implementing syntactic equality (which should be true for deriving?). E.g., for the data type data Frac = Frac Int Int we would have 'not (Frac 1 2 = Frac 2 4)' in HOLCF (since we have injectivity of all constructors). But nobody prevents a programmer from writing an Eq instance of Frac that compares 'normal forms' of fractions. Now, /this/ is an example of what I've been trying to get at. (To be fair, it's a generalization of what I've been trying to get at) You put it in behavioral terms -- nothing stops a programmer, whereas I've been trying to put it in interpretive terms (... is ..., but ... means many things -- you have to pick an interpretation) A hypothetical programmer can write: data Fraction = Fraction Int Int data Rational = Rational Int Int and have different semantics for each. In particular, we should treat Fraction 1 2 to be distinct from Fraction 2 4, /as fractions/. And Rational 1 2 should be the same as Rational 2 4, /as rational numbers/. These implied semantics are just as important as the minimum Haskell demands (in my opinion). The minimum Haskell demands is not (and cannot) be rich enough to distinguish between intentions/intensions. Obviously, Fraction and Rational are intimately related (the rationals should be a ring of fractions in normal form). And functions between Fraction and Rational should preserve the correct relationships. But, what are these? We can come up with theorems, but some things are nothing but the programmer/mathematician's choice. In other words, by choosing a semantic where (Rational 1 2) == (Rational 2 4), a programmer/mathematician has *generated* a sublanguage of Haskell by imposing his *intended* semantics. This is an example of intensions versus extensions in logic. So, your task is... difficult. From my point of view, you will have to axiomatize at least one set of best practices for Haskell
Re: [Haskell-cafe] Applicative functors with branch/choice ?
On Wed, Jul 25, 2012 at 09:22:23PM +0100, Евгений Пермяков wrote: So, it seems for me, that Applicative API should be extended with typeclass for making choice what actions to execute depending on result of some test (pattern matching). Is there any reasonable definition of such typeclass or clear explanation, why such typeclass is unneeded? The possible extension may look somehow like this: class Applicative a = Branching a where branch :: a (Either b c) - (a b - a d) - (a c - a d) - a d Do you have any instances in mind? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative functors with branch/choice ?
well... This code is both demonstration for use case and more sane
class + instance
typeclass name is selected quite randomly, may be native speaker will
select a better one
module Actuative where
import Control.Applicative
import System.IO
import System.IO.Error
-- | minimal complete definition : select
class Applicative f = Actuative f where
-- | select computation conditionally . Side effects of only one two
alternative take place
select :: f (Either a b) -- ^ selector
- f (a - c) -- ^ first alternative
- f (b - c) -- ^ second alternative
- f c
-- | correct possible error
correct :: f (Either a b) - f (a - b) - f b
correct i l = select i l (pure (\x - x))
-- | similiar for select, but mimics ArrowChoice
branch :: f (Either a b) - f (a - c) - f (b - d) - f (Either
c d)
branch i l r = select i (pure (\f x - Left (f x)) * l) (pure (\f x
- Right (f x)) * r)
-- | execute only if Left
onLeft :: f (Either a b) - f (a - c) - f (Either c b)
onLeft i l = branch i l (pure (\x - x))
-- | execute only if Right
onRight :: f (Either a b) - f (b - c) - f (Either a c)
onRight i r = branch i (pure (\x - x)) r
-- | This is streaming parser combinators for writing LR (k) grammars
newtype Parse a = Parse { runParse :: Handle - IO a }
-- | this function is one of reasons. If EOF occurs, we should produce
result. If not, we should continue parsing. Monadic interface, however,
gives too much freedom.
next :: Parse (Maybe Char)
next = Parse $ \h - catchIOError (fmap Just $ hGetChar h) (const $
return Nothing)
instance Functor Parse where
fmap f s = pure f * s
instance Applicative Parse where
pure a = Parse $ \_ - return a
(Parse l) * (Parse r) = Parse $ \h - do
lr - l h
rr - r h
return $ lr rr
-- instance for Actuative.
instance Actuative Parse where
select (Parse i) (Parse l) (Parse r) = Parse $ \h - do
ir - i h
case ir of
Left lv - do
lr - l h
return $ lr lv
Right rv - do
rr - r h
return $ rr rv
On 07/26/2012 12:48 PM, Ross Paterson wrote:
On Wed, Jul 25, 2012 at 09:22:23PM +0100, Евгений Пермяков wrote:
So, it seems for me, that Applicative API should be extended with
typeclass for making choice what actions to execute depending on result
of some test (pattern matching). Is there any reasonable definition of
such typeclass or clear explanation, why such typeclass is unneeded?
The possible extension may look somehow like this:
class Applicative a = Branching a where
branch :: a (Either b c) - (a b - a d) - (a c - a d) - a d
Do you have any instances in mind?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative functors with branch/choice ?
On 26/07/12 12:40, Евгений Пермяков wrote: class Applicative f = Actuative f where -- | select computation conditionally . Side effects of only one two alternative take place select :: f (Either a b) -- ^ selector - f (a - c) -- ^ first alternative - f (b - c) -- ^ second alternative - f c Can't you already define this function in terms of Applicative itself? I.e. select xs fs gs = sel $ xs * fs * gs where sel (Left a) f _ = f a sel (Right b) _ g = g b I assume that your intent is that `select` behaves differently from the one I defined here. But you need to specify in what way. Suppose it should work like if-then-else. Then you would perhaps have these laws: select (Left $ x) f g = f $ x select (fmap swapEither x) f g = select x g f I think this is a useful class to have, and I would support adding something like it to the standard library. Perhaps the arguments should be swapped to the same order as either, to give class Functor f = Selective f where eitherF :: f (a - c) - f (b - c) - f (Either a b) - f c The laws would then be: eitherF f g . fmap swapEither = eitherF g f eitherF f g . fmap Left = f eitherF f g . fmap Right = g -- follows from the other two laws every Monad is an instance via defaultEitherF ls rs xs = either ls rs = xs Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative functors with branch/choice ?
May be difference will be more clear with this example ? import Control.Monad.State instance (Functor m, Monad m) = Actuative (StateT s m) where select i l r = do iv - i case iv of Left lv - l = \lf - return (lf lv) Right rv - r = \rf - return (rf rv) select' xs fs gs = sel $ xs * fs * gs where sel (Left a) f _ = f a sel (Right b) _ g = g b increment :: Monad m = StateT Int m (() - ()) increment = get = (put . (+1)) return (const ()) the difference may be seen clearly, when you run in ghci *Actuative runState (select' (return $ Left ()) increment (increment * increment * increment)) 0 ((),4) *Actuative runState (select (return $ Left ()) increment (increment * increment * increment)) 0 ((),1) Not sure, what categorical concept is model for this type class On 07/26/2012 03:14 PM, Twan van Laarhoven wrote: On 26/07/12 12:40, Евгений Пермяков wrote: class Applicative f = Actuative f where -- | select computation conditionally . Side effects of only one two alternative take place select :: f (Either a b) -- ^ selector - f (a - c) -- ^ first alternative - f (b - c) -- ^ second alternative - f c Can't you already define this function in terms of Applicative itself? I.e. select xs fs gs = sel $ xs * fs * gs where sel (Left a) f _ = f a sel (Right b) _ g = g b No. Well, a function with same type signature may be defined in terms of Applicative, as you demonstrated. However, look how select will work with instance for IO, defined like this instance Actuative IO where select i l r = do ir - i case ir of Left lv - do lf - l return $ lf lv Right rv - do rf - r return $ rf rv As you can see, if I use select definition with Control.Applicative.*, I'll execute both l and r and the only choice will be, what result to drop. Both l and r, however, will be executed, and their side effects will take place. With select from my code only one action will be executed, depending on result of i, and only effects of one of actions (either l or r) will take place. I'm not sure, what categorical concept will correspond to this typeclass. I assume that your intent is that `select` behaves differently from the one I defined here. But you need to specify in what way. Suppose it should work like if-then-else. Then you would perhaps have these laws: select (Left $ x) f g = f $ x select (fmap swapEither x) f g = select x g f I think this is a useful class to have, and I would support adding something like it to the standard library. Perhaps the arguments should be swapped to the same order as either, to give class Functor f = Selective f where eitherF :: f (a - c) - f (b - c) - f (Either a b) - f c The laws would then be: eitherF f g . fmap swapEither = eitherF g f eitherF f g . fmap Left = f eitherF f g . fmap Right = g -- follows from the other two laws every Monad is an instance via defaultEitherF ls rs xs = either ls rs = xs Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative functors with branch/choice ?
On 26/07/12 13:58, Евгений Пермяков wrote: As you can see, if I use select definition with Control.Applicative.*, I'll execute both l and r and the only choice will be, what result to drop. Both l and r, however, will be executed, and their side effects will take place. With select from my code only one action will be executed, depending on result of i, and only effects of one of actions (either l or r) will take place. I realize that, and that is why I insisted on laws to formalize this. Your instance for IO is a special case of a function that works for any Monad: defaultEitherF :: (Functor f, Monad f) = f (a - c) - f (b - c) - f (Either a b) - f c defaultEitherF ml mr mx = either (ml $$) (mr $$) = mx where ($$) :: Functor f = f (a - b) - a - f b f $$ x = ($ x) $ f (the version of this function in my previous post was not correct) I'm not sure, what categorical concept will correspond to this typeclass. Well, this type class kind of corresponds to the functionality of ArrowChoice. I believe that class corresponds to a (symmetric) monoidal structure on the dual category. Plus a whole bunch of junk you get from its super classes. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell on Mac OS X Mountain Lion
Hi all, does the Haskell Platform (2012.2.0.0 I suppose) work on 10.8. http://hackage.haskell.org/platform/mac.html only says something about 10.7. I don't want to break my development system due to upgrading to 10.8, so if anybody has any experience regarding this topic, please let me know. Best wishes ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Making extra GMP bindings
Hello, We haven't found mpz_nextprime in the list of gmp functions that have bindings in integer-gmp, and we would like to call it from a Haskell project. We have first looked at a few simple examples of using the FFI but found several difficulties: - The mapping between Integer and the C data types isn't explicited anywhere - The gmp function gives its result by writing it in its second argument, instead of returning it. Building a wrapper for it that allocates the resulting Integer wouldn't be trivial because of how it could interact with the GC Then we looked at how integer-gmp itself does it, it seems to be writing lots of cmm wrappers that call inside of the GHC runtime. Is there an easier way to build a binding for a gmp function than to hack integer-gmp and recompile ghc ? Thanks, Robin Morisset Florian Bourse ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GHC type error pretty printing
Is it me or is this output not right? The \ syntax doesn't indicate a newline. chris@midnight:~$ ghci GHCi, version 7.4.2: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude abc\n123 :: () interactive:2:1: Couldn't match expected type `()' with actual type `[Char]' In the expression: abc\ \123 :: () In an equation for `it': it = abc\ \123 :: () ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] FP Developers Conference
Alex Miller is the organizer of a very successful Strange Loop developers conference in St Luis. He also happens to be a Closure programmer. He wants to organize a Functional Programming Developers Conference in the US (stress on _developers_). He will probably succeed, so it's very important that Haskell be well represented there. I would like to encourage everybody to take a minute and fill out a short preliminary poll at http://tech.puredanger.com/2012/07/24/functional-programming-conference/ . This is to give Alex the idea how many people are interested, what language they prefer, and what area of development they're interested in. -- [:Bartosz:] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell on Mac OS X Mountain Lion
On Thu, Jul 26, 2012 at 9:19 AM, mrbuchm...@googlemail.com wrote: does the Haskell Platform (2012.2.0.0 I suppose) work on 10.8. Yes. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
[Re-sent as my first post did not make it through.] Hi Christian, Am Mittwoch, den 25.07.2012, 10:19 +0900 schrieb Christian Sternagel: Btw: Isabelle/HOLCF unifies all error values and nontermination in a single bottom element _|_. Currently we are using the following axioms for our formal Eq class (where I'm using Haskell syntax although the real sources [2] use Isabelle/HOLCF syntax which is slightly different; (=) is meta-equality). (x == y) = True == x = y (x == y) = False == not (x = y) (x == _|_) = _|_ (_|_ == y) = _|_ I am slightly worried about the latter two; after all one might find it reasonable to specify instance Eq () where _ == _ = True or, maybe slightly more sensible instance Eq Void where _ == _ = True But I checked and both the instances of (), the instance of Data.Void (in the void package) and the derived instance for empty data types are strict: Prelude data V Prelude :set -XStandaloneDeriving Prelude deriving instance Eq V Prelude (error 1 :: V) == (error 2 :: V) *** Exception: Void == Greetings, Joachim -- Joachim Breitner e-Mail: m...@joachim-breitner.de Homepage: http://www.joachim-breitner.de Jabber-ID: nome...@joachim-breitner.de signature.asc Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
