Re: [Haskell-cafe] A question on existential types and Church encoding
Thanks! That was exactly the sort of response I was looking for. This explains why you need to double up for your current definitions. To choose between two booleans (which will in turn allow you to choose between 'a's), you need a CB (CB a). You can eliminate the asymmetric type, though, like so: cand :: CB a - CB a - CB a cand p q t f = p (q t f) f Right. When he was working on it, I thought of that, and seemed to have completely forgotten when I reworked it. You can probably always do this, but it will become more tedious the more complex your functions get. type CB a = forall a . a - a - a Note: this is universal quantification, not existential. As I would assume. But I always see the forall keyword used when discussing existential quantification. I don't know if I've ever seen an exists keyword. Is there one? How would it be used? In the new type, the parameter 'a' is misleading. It has no connection to the 'a's on the right of the equals sign. You might as well write: type CB = forall a. a - a - a Ah! That makes sense. Which raises a new question: Is this type too general? Are there functiosn which are semantically non-boolean which fit in that type, and would this still be the case with your other suggestion (i.e. cand p q = p (q t f) f )? I guess it wouldn't much matter, since Church encodings are for untyped lambda calculus, but I'm just asking questions that come to mind here. :) And now, hopefully, a key difference can be seen: we no longer have the result type for case analysis as a parameter of the type. Rather, they must work 'for all' result types, and we can choose which result type to use when we need to eliminate them (and you can choose multiple times when using the same boolean value in multiple places). One may think about explicit typing and type abstraction. Suppose we have your first type of boolean at a particular type T. We'll call said type CBT. Then you have: CBT = T - T - T and values look like: \(t :: T) (f :: T) - ... By contrast, values of the second CB type look like this: \(a :: *) (t :: a) (f :: a) - ... *snip* cand (T :: *) (p :: CB T) (q :: CB T) = ... cand gets told what T is; it doesn't get to choose. I'm guessing that * has something to do with kinds, right? This is probably a silly question, but why couldn't we have (T :: *-*) ? Hopefully I didn't make that too over-complicated, and you can glean something useful from it. It turned out a bit longer than I expected. It was very helpful, thanks! Cory ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A question on existential types and Church encoding
Hello, A professor of mine was recently playing around during a lecture with Church booleans (I.e., true = \x y - x; false = \x y - y) in Scala and OCaml. I missed what he did, so I reworked it in Haskell and got this: type CB a = a - a - a ct :: CB aC ct x y = x cf :: CB a cf x y = y cand :: CB (CB a) - CB a - CB a cand p q = p q cf cor :: CB (CB a) - CB a - CB a cor p q = p ct q I found the lack of type symmetry (the fact that the predicate arguments don't have the same time) somewhat disturbing, so I tried to find a way to fix it. I remembered reading about existential types being used for similar type-hackery, so I added quantification to the CB type and got type CB a = forall a . a - a - a ctrue :: CB a ctrue x y = x cfalse :: CB a cfalse x y = y cand :: CB a - CB a - CB a cand p q = p q cfalse cor :: CB a - CB a - CB a cor p q = p ctrue q which works. But I haven't the faintest idea why that forall in the type makes things work... I just don't fully understand existential type quantification. Could anyone explain to me what's going on that makes the second code work? Thanks, Cory ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chicago Haskell User Group?
I and certainly some of my professors would be extremely interested in a Chicago HUG. Facebook sounds like a good idea, but I tend not to actually check facebook groups. They just aren't quite intrusive enough. :) Unfortunately (actually, quite fortunately), I'm in Budapest for the semester, so I can't participate in a very real way. I don't believe the professors who would be interested subscribe to Haskell Cafe, so I will pass any relevant info on. Cheers, Cory Jeremy Shaw wrote: Hello, Sounds good to me. I am in the Chicago area and do Haskell-based web development all day, every day, using the Happstack platform. I don't have much time to organize, but I would be able to attend meetings and give some presentations. Personally, I would recommend using a facebook page as a means of communicating within the group. Facebook offers the following features: 1. a proven track record of allowing users to control their levels of privacy, and not spamming them. More information regarding privacy here: http://www.google.com/search?q=privacyquery=site%3Awww.insidefacebook.com 2. many people already have accounts, and, if not, creating one is super easy 3. event calendar, invitations 4. free photo and video hosting 5. discussion boards 6. can be extended (free) via the Facebook API (in Haskell, I have a library I will be announcing soon). 7. Super easy to setup (less than 2 minutes). (Applications - Ads and Pages - Pages - Create Page). I would recommend a facebook page over a facebook group. I would - jeremy At Wed, 12 Aug 2009 14:13:37 -0500, Tom Tobin wrote: There isn't a Chicago-area Haskell group, is there? If not, would anyone be interested in forming one? I used to run Chicago's Django (a Python web framework) group, but lost interest (and since I lived in the suburbs back then, got sick of the commute). Unlike Python, I'm still very much a beginner with Haskell, so I feel I'd be able to benefit quite a bit from picking the brains of more skilled users and cooperating with other beginners. My particular interests are web development (as that's my professional field) and multimedia organization (I'm working on a Haskell audio tagging library to help teach myself the language), but I'm open to learning just about anything. :-) ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Graphs and graph algorithms?
Hey, Besides fgl, are there any graph libraries in Haskell that are still maintained? Are there other papers (or books) besides Erwig's that I could use to understand how graph algorithms have been implemented in functional languages? Has anything even been published on the topic since Erwig's paper? Thanks, Cory ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Just 3 = (1+)?
... There have been 12 replies to this question, all of which say the same thing. I'm glad we're so happy to help, but does Just 3 = return . (+1) Need to be explained by 12 different people? fmap (trying to++) $ Just help -- :D Cory Why doesn't this work? Michael [mich...@localhost ~]$ ghci GHCi, version 6.10.1: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. Prelude Just 3 = (1+) interactive:1:0: No instance for (Num (Maybe b)) arising from a use of `it' at interactive:1:0-14 Possible fix: add an instance declaration for (Num (Maybe b)) In the first argument of `print', namely `it' In a stmt of a 'do' expression: print it Prelude ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comments from OCaml Hacker Brian Hurt
Andrew Coppin wrote: I can't await the next Haskell standard, where at last all those extensions are builtin. This frightens me. The example he had had the uses keyword, so I assume it's built in in the same way Perl pragma are built in. So you can happily ignore code when you see uses at the top of the file. ;) Although I could be wrong. Cheers, Cory ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Improved documentation for Bool (Was: [Haskell-cafe] Comments from OCaml Hacker Brian Hurt)
rocon...@theorem.ca wrote: On Sun, 18 Jan 2009, Ross Paterson wrote: Anyone can check out the darcs repos for the libraries, and post suggested improvements to the documentation to librar...@haskell.org (though you have to subscribe). It doesn't even have to be a patch. Sure, it could be smoother, but there's hardly a flood of contributions. I noticed the Bool datatype isn't well documented. Since Bool is not a common English word, I figured it could use some haddock to help clarify it for newcomers. -- |The Bool datatype is named after George Boole (1815-1864). -- The Bool type is the coproduct of the terminal object with itself. -- As a coproduct, it comes with two maps i : 1 - 1+1 and j : 1 - 1+1 -- such that for any Y and maps u: 1 - Y and v: 1 - Y, there is a unique -- map (u+v): 1+1 - Y such that (u+v) . i = u, and (u+v) . j = v -- as shown in the diagram below. -- -- 1 -- u -- Y -- ^ ^^ -- |/ | -- i u + v v -- | /| -- 1+1 - j -- 1 -- -- In Haskell we call we define 'False' to be i(*) and 'True' to be j(*) -- where *:1. -- Furthermore, if Y is any type, and we are given a:Y and b:Y, then we -- can define u(*) = a and v(*) = b. -- From the above there is a unique map (u + v) : 1+1 - Y, -- or in other words, (u+v) : Bool - Y. -- Haskell has a built in syntax for this map: -- @if z then a else b@ equals (u+v)(z). -- -- From the commuting triangle in the diagram we see that -- (u+v)(i(*)) = u(*). -- Translated into Haskell notation, this law reads -- @if True then a else b = a...@. -- Similarly from the other commuting triangle we see that -- (u+v)(j(*)) = v(*), which means -- @if False then a else b = b@ I'm going to go ahead and assume this was a joke and crack up... The sad part is I didn't actually find this difficult to read... Cory lost touch with the real world Knapp ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Comments from OCaml Hacker Brian Hurt
Andrew Coppin wrote: Cory Knapp wrote: As far as I know, one of the draws of Haskell is the inherent mathematical nature of it. It's also simultaneously one of the biggest things that puts people off. Perhaps as we can curb this with sufficient documentation, as others have suggested. Actually, that was part of my point: When I mention Haskell to people, and when I start describing it, they're generally frightened enough by the focus on pure code and lazy evaluation-- add to this the inherently abstract nature, and we can name typeclasses cuddlyKitten, and the language is still going to scare J. R. Programmer. By inherently mathematical nature, I didn't mean names like monoid and functor, I meant *concepts* like monoid and functor. Not that either of them are actually terribly difficult; the problem is that they are terribly abstract. That draws a lot of people (especially mathematicians), but most people who aren' drawn by that are hugely put off-- whatever the name is. So, I guess my point is that the name is irrelevant: the language is going to intimidate a lot of people who are intimidated by the vocabulary. At the same time, I think everyone is arguing *for* better documentation. And you're probably right: better documentation will bring the abstract nonsense down to earth somewhat. But there's a deeper problem here, one that can't be resolved inside the Haskell community. The problem is that the Math?! Scary! Gross! attitude that's so pervasive in our society is hardly less pervasive in the computer subculture. No arguments here! However, that at least *is* completely beyond our power to alter. Unfortunately. Indeed. Cheers, Cory ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Documentation [Comments from OCaml Hacker Brian Hurt]
Dan Piponi wrote: On Fri, Jan 16, 2009 at 12:09 PM, Paul Moore p.f.mo...@gmail.com wrote: How about associativity means that how you pair up the operations does not affect the result? I think a better way is this: If you have an element of a monoid, a, there are two ways to combine it with another element, on the left or on the right. You get a `mappend` x or x `mappend` a. Now suppose you're going to combine a with x on the left and y on the right. Associativity means it doesn't matter which you do first. You can think of each element of a monoid as having two sides. The idea is that the left side and right side are independent things that don't interfere with each other. For example, adding some stuff at the beginning of a list, and adding some stuff at the end of a list, don't affect each other, and it doesn't matter which you do first. That's the idea that associativity captures. -- Dan Indeed, that's the idea that associativity captures; but explicitly pointing out that the left and the right side are their own bubbles is a bit misleading: addition is associative, but there is no left and right. I think a better wording is: If you have an element of a monoid, a, there are two ways to combine it with another element, on the left or on the right. You get a `mappend` x or x `mappend` a. Now suppose you're going to combine a with x on the left and y on the right. Associativity means it doesn't matter which you do first. So x `mappend` (a `mappend` y) = (x `mappend` a) `mappend` y, but as we've pointed out, a `mappend` x is not necessarily the same as x `mappend` a although a specific monoid might have them be equal, for example Int (where mappend is *). Is that better? Cory ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Comments from OCaml Hacker Brian Hurt
Perhaps as a math/CS major I'm a bit biased here, but as a haskell neophyte, I think my opinion is at least somewhat relevant... The immediate problem is certainly documentation. No one would groan more than once after hearing a term from abstract math if there was sufficient Haskell-oriented language. I can say that a monad is an endo-functor (in this case on Hask) which is the composition of two natural transformations; the clever parrot I am, I can even understand most of this... but that doesn't mean anything to me in a Haskell context; until a new Haskell programmer can find a Hasktionary with relevant terms in a Haskell context, everything is meaningless-- even though I can understand (i.e. apply meaning to) the definition of a monad on Hask, I can't apply the sort of meaning required to program with a monad without either figuring it out through experience, or seeing it shown to me in a programmer-relevant way (Or rather, both need to happen.) On the other hand, I really, really like getting behind things and understanding the theory. In C, well, C is the theory-- if I want to go deeper, I need to learn as much as I can about the way a computer actually, physically works (why, why, then, even have higher level languages?) or I need to take a history lesson so I can figure out the math that helped out... With Haskell, the theory is right there, staring at me. If the documentation were better, I wouldn't *need* to learn it, but if my curiosity is piqued, it's right there. Naming monoid appendable kills that-- by trying to make things warm and fuzzy, you've weakened one of my strongest motivators for programming (especially in Haskell), namely how much of a direct application of cool math it is. I know I'm not the only one. As far as I know, one of the draws of Haskell is the inherent mathematical nature of it-- in how many other languages do people write proofs of correctness because they don't want to write test-cases? The kind of people who are going to be drawn to a language which allows [(x,y)| x-somelist, y-someotherlist] are overall, a mathy set of people, and trying to make our terms fuzzy isn't going to change that. So why not embrace it? This leads to another point: monoids are probably called monoids for the same reason monads are monads: they came directly out of higher math. Someone did sit down trying to name this cool new Haskell idea he had and then say, Oh, of course, it's just [insert obscure math word that's used in Haskell]! I'll keep that name. He sat down, and said, Oh! Wait if I use [insert obscure math word that's used in Haskell] this problem is simpler. It's named for what it is: a monoid, a monad, a functor, existential quantification. But there's a deeper problem here, one that can't be resolved inside the Haskell community. The problem is that the Math?! Scary! Gross! attitude that's so pervasive in our society is hardly less pervasive in the computer subculture. I shouldn't be more able to discuss abstract math with a conservatory dropout theater student than with someone who plans, for a living, to put well-formed formulae onto a finite state machine. I am. I don't expect the average programmer to be able to give me a well-ordering of the reals (with choice, of course), or to prove that category C satisfying property P must also satisfy property Q; but for God's sake, they better have a good intuition for basic set theory, basic graph theory, and most importantly mathematical abstraction. What is good coding style if not making the exact same types of abstractions that mathematicians make? Again, I don't expect a CS major to write a good proof, to explain rings to a 13 year old, or actually do real math; but I expect one to be able to read In abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a single, associative binary operation and an identity element. and be able to get a basic intuitive idea for what a monad is; with some thought of course. I would go so far as to say that a programmer should be able to intuitively understand a system of objects and associative arrows, even if they can't do math with that... Programmers shouldn't be allowed to get away with the absolute ignorance of math that at least 75% of the CS majors at my school pass with. This doesn't mean there isn't a serious problem with Haskell documentation; it also doesn't mean that everyone should have a minor in math to be a programmer, but isn't an introductory course in discrete math required for most CS programs? Then why are programmers so afraid of basic mathematical definitions? And why do so many wear their ignorance and fear of math as a badge of honor? Sorry that this came out as a bit of a rant, but I spend enough time trying to convince people that math isn't horrid and disgusting... Cory Knapp ___ Haskell-Cafe mailing list Haskell
