Re: [Haskell-cafe] Alternative name for return
On Thu, Aug 8, 2013 at 7:40 AM, Timon Gehr timon.g...@gmx.ch wrote: You make the distinction between evaluate, Which essentially means applying reduction rules to an expression until the result is a value. and execute or run, etc. This is not functional. How would you know? I think Jerzy is alluding to the fact that we don't have a denotational semantics for IO. So I'm not sure I understand your response. Are you pointing out that some subspace of IO programs admit such a semantics via an easy inspection? 'putStr c' is a pure value. This is the crux of the matter: pure value means different things to different people. Some employ it to mean an effectful monadic expression to distinguish between getLine and (return Hello), both of type IO String. Others use it to distinguish between an ordinary Haskell expression and, say, C. So when you write: 'unsafePerformIO (putStr c)' is not a pure value. I infer you're in the latter camp. Would you then speak of 'effectful' values vs 'null-effectful' ones? What oral syntax would you actually use? -- Kim-Ee On Thu, Aug 8, 2013 at 7:40 AM, Timon Gehr timon.g...@gmx.ch wrote: On 08/08/2013 01:19 AM, Jerzy Karczmarczuk wrote: Bardur Arantsson comments the comment of Joe Quinn: On 8/7/2013 11:00 AM, David Thomas wrote: twice :: IO () - IO () twice x = x x I would call that evaluating x twice (incidentally creating two separate evaluations of one pure action description), but I'd like to better see your perspective here. x is only evaluated once, but/executed/ twice. For IO, that means magic. For other types, it means different things. For Identity, twice = id! Your point being? x is the same thing regardless of how many times you run it. What do you mean by the same thing? You cannot compare 'them' in any reasonable sense. ... http://en.wikipedia.org/wiki/**Identity_of_indiscernibleshttp://en.wikipedia.org/wiki/Identity_of_indiscernibles (He is reasoning _about_ the language and not _within_ the language because Haskell does not support very powerful reasoning internally.) ... You make the distinction between evaluate, Which essentially means applying reduction rules to an expression until the result is a value. and execute or run, etc. This is not functional. How would you know? Your program doesn't run anything, it applies (=) (or equivalent) to an IO (...) object. This is the only practical evaluation of it, otherwise it can be passed (or duplicated as above). But you cannot apply bind twice to the same instance of it (in fact, as I said above, the same instance is a bit suspicious concept...). ... Indeed, but you didn't say that above. The running or execution takes place outside of your program. In such a way Richard O'Keefe and I converge... That's why I say that the concept of purity is meaningless in the discussed context. Not meaningless, but redundant. The point of having a purely functional programming language is to have reasoning based on purity be universally applicable. It is a kind of counterfeit notion, inherited from pure functions to something which belongs to two different worlds. ... 'putStr c' is a pure value. On the other hand: 'unsafePerformIO (putStr c)' is not a pure value. (But this expression does not exist in standard Haskell. unsafePerformIO unquotes the action. You may be confusing the quoted and unquoted versions.) __**_ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://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] Some philosophy (Was: Alternative name for return)
On Fri, Aug 9, 2013 at 10:44 PM, Jerzy Karczmarczuk jerzy.karczmarc...@unicaen.fr wrote: I decided to reread some philosophical texts, and I suggest one for your evening reading. Indiscrete Thoughts by Gian-Carlo Rota, published by Birkhäuser in 1997. Available on the Web. I'm rather fond of Rota's two volumes of musings. For the purpose of furthering the quality of philosophizing, would it not be better served citing the relevant chapters, if not the actual page numbers? As you took note, the book covers a swathe of topics. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Identity of indiscernibles
On Thu, Aug 8, 2013 at 11:05 PM, Tom Ellis tom-lists-haskell-cafe-2...@jaguarpaw.co.uk wrote: On Thu, Aug 08, 2013 at 03:38:41PM +0200, Jerzy Karczmarczuk wrote: One could simply implement IO as a free monad Interesting. I wonder how. See [1] for an explanation of free monads in general. For IO in particular, define a functor data IOF a = GetChar (Char - a) | PutChar Char a | ... with constructors for all elementary IO operations. If I understand correctly, you're proposing equality of (IO a) based on the AST of imperatives, similar to what comes out of GCC's front-end for C [1]. In what way is this syntactical equality reasonable? Useful perhaps for detecting CP coding from befuddled undergrads? [1] http://digitocero.com/es/blog/exportar-y-visualizar-el-arbol-sintactico-abstractoast-de-gcc -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Release Candidates for Haskell Platform 2013.2
On Mon, May 13, 2013 at 9:39 PM, Mark Lentczner mark.lentcz...@gmail.comwrote: *Some of the release candidates for Haskell Platform 2013.2 are up.* Kudos! Exactly 7 days from the scheduled date, as stated. Hope to give them a whirl once the other OSes are baked. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Markdown extension for Haddock as a GSoC project
On Mon, Apr 29, 2013 at 8:42 AM, Alexander Solla alex.so...@gmail.comwrote: I've been scoffed at during interviews for saying I solve problems on paper before I start typing! That has to suck. I hope you're properly avenged when you find work in a savvier, respectful competitor and KICK THEIR ASSES! -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why were datatype contexts removed instead of fixing them?
On Thu, Apr 25, 2013 at 6:36 PM, Joe Quinn headprogrammingc...@gmail.comwrote: data Foo a where Foo :: Eq a = a - Foo a is equivalent to data Foo a = Eq a = Foo a but is different from data Eq a = Foo a = Foo a (Yup, tripped up a few of us already!) -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] NaN as Integer value
On Sun, Apr 14, 2013 at 3:28 PM, wren ng thornton w...@freegeek.org wrote: Whereas the problematic values due to infinities are overspecified, so no matter which answer you pick it's guaranteed to be the wrong answer half the time. Part of this whole problem comes from the fact that floats *do* decide to give a meaning to 1/0 (namely Infinity). I'm not sure what you mean about overspecification here, but in setting 1/0 as +infinity (as opposed to -infinity), there's an easily overlooked assumption that the limit is obtained from above as opposed to from below. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is there an escape from MonadState+MonadIO+MonadError monad stack?
On Sun, Apr 7, 2013 at 5:03 AM, Ömer Sinan Ağacan omeraga...@gmail.com wrote: That's interesting, thanks! Do you have any recommendations about which file to start reading? AFAIK, GHC is _huge_. Without a discussion of your interests, it's hard to say. Certainly, I'd set up the reading environment, namely an editor that can traverse from usage to point of definition and back. An interesting idea that occurred to me is to start with the file with the largest comments to code ratio. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] code-as-config, run-time checks and error locations
On Sun, Apr 7, 2013 at 12:23 AM, Steffen Schuldenzucker sschuldenzuc...@uni-bonn.de wrote: For the moment I think it would be enough to auto-insert the location of calls to a certain set of functions. Have you tried assert [1]? [1] http://hackage.haskell.org/packages/archive/base/4.6.0.1/doc/html/Control-Exception.html#v:assert -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] meaning of referential transparency
On Sun, Apr 7, 2013 at 12:43 AM, Henning Thielemann lemm...@henning-thielemann.de wrote: Can someone enlighten me about the origin of the term referential transparency? I can lookup the definition of referential transparency in the functional programming sense in the Haskell Wiki and I can lookup the meaning of reference and transparency in a dictionary, but I don't know why these words were chosen as name for this defined property. Instead of a immaculately precise definition, may I suggest going about it from the practical benefits POV? RT matters so much in Haskell because of the engineering leverage it gives us. Bird's Pearls are a good source of Why Equational Reasoning Matters. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] meaning of referential transparency
Should probably include the Reddit convo ongoing as we speak (zomg, it's live!): http://www.reddit.com/r/haskell/comments/1bsitm/lazy_io_breaks_equational_reasoning/ Not everyone here is a regular there. -- Kim-Ee On Sun, Apr 7, 2013 at 1:21 AM, Eli Frey eli.lee.f...@gmail.com wrote: Links SO: http://stackoverflow.com/questions/210835/what-is-referential-transparency Reddit discussions of said SO question. http://www.reddit.com/r/haskell/comments/x8rr6/uday_reddy_on_referential_transparency_and_fp/ http://www.reddit.com/r/haskell/comments/xgq27/uday_reddy_sharpens_up_referential_transparency/ This was a fascinating exchange and I'm glad to be reminded to revisit it :). On Sat, Apr 6, 2013 at 11:13 AM, Kim-Ee Yeoh k...@atamo.com wrote: On Sun, Apr 7, 2013 at 12:43 AM, Henning Thielemann lemm...@henning-thielemann.de wrote: Can someone enlighten me about the origin of the term referential transparency? I can lookup the definition of referential transparency in the functional programming sense in the Haskell Wiki and I can lookup the meaning of reference and transparency in a dictionary, but I don't know why these words were chosen as name for this defined property. Instead of a immaculately precise definition, may I suggest going about it from the practical benefits POV? RT matters so much in Haskell because of the engineering leverage it gives us. Bird's Pearls are a good source of Why Equational Reasoning Matters. -- Kim-Ee ___ 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] Is there an escape from MonadState+MonadIO+MonadError monad stack?
On Sun, Apr 7, 2013 at 4:22 AM, Ömer Sinan Ağacan omeraga...@gmail.com wrote: I'm a hobbyist Haskell programmer and my use of Haskell is mostly consists of writing interpreters, simple virtual machines, and type checkers. One thing I'm not happy about my Haskell programs is, almost all of my programs have a monad transformer stack consisting MonadError, MonadIO and MonadState. Welcome! Hobbyist Haskellers writing VMs and type checkers are a critical part of the community and what sets us apart. Not as well-known as it should be is the fact that GHC doesn't make much use of monad transformers. Have you taken a look at the sources? That might provide ideas on future ways of structuring your experiments. Also, what precisely are the infelicities with monad transformers in your code? Depth of stack? Forced type annotation? Syntax inflation due to extra lift* functions? Monad transformers provide an abstraction which may not be necessary for some apps. But it's easy to write something and then suddenly, the need for generalization kicks in. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] code-as-config, run-time checks and error locations
On Sun, Apr 7, 2013 at 4:37 AM, Steffen Schuldenzucker sschuldenzuc...@uni-bonn.de wrote: Reading through that now... [1] http://hackage.haskell.org/trac/ghc/wiki/ExplicitCallStack If you're reading that page, you probably also want to get up to speed on the latest. The thread titled RFC: rewrite-with-location proposal just ended recently [1]. [1] http://www.haskell.org/pipermail/haskell-cafe/2013-February/106617.html -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Possible GSoC project
On Thu, Apr 4, 2013 at 10:03 PM, Ketil Malde ke...@malde.org wrote: Not very much, some knowledge of string edit distance and dynamic programming would be good, but if not, it's something I can straighten out with a student in an afternoon, I think. Just a suggestion: People love quizzes and brain teasers. (Remember those google billboards?) If you could blog briefly (expository-style) about this with links to further reading, and more importantly, include challenges in the bottom-half, I bet you could get some buzz circulating. Especially if you manage those all-important bragging rights! -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GSoC Project Proposal: Markdown support for Haddock
On Fri, Apr 5, 2013 at 3:04 AM, Simon Heath icefo...@gmail.com wrote: I humbly suggest reStructuredText rather than Markdown, which is what is used by the Python community for documentation. Since it's specifically made for documentation it may be nicer. But, I don't want to spark a format argument. Could you say something about /why/ you make the suggestion? I, for one, would be happy to google and read links, but what's missing from that experience would be input from a fellow haskeller. In context. In real-time. On topic. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GSoC Project Proposal: Markdown support for Haddock
On Fri, Apr 5, 2013 at 10:44 AM, Ivan Lazar Miljenovic ivan.miljeno...@gmail.com wrote: I don't think so; this was one of the big issues recently when people were trying to get Gruber to actually _do_ something with Markdown as there were all these corner cases. In that case, surely this is an opportunity to convene a committee (a la H98) to craft a formal spec? -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
(Folks, let's rescue this increasingly tendentious thread.) Some points to ponder: (1) Any can be often be clarified to mean all, depending on how polymorphic functions are exegeted. In a homotopy-flavored explanation of natural transformation, its components (read parametric instances) exist /all at once/ like the collinear rays of a rainbow. So given this: f :: Bool - t f True = 'x' f False = 'y' nope, no rainbow. :( ... the aftermath flame war of why didn't you say it earlier? because it's obvious! no it's not! yes it is! is not! but all mathematicians find it obvious! well then I am not a mathematician and will never be! And more to the point, an excellent learning environment requires empathy from all participants, juniors and seniors alike. Where diversity is celebrated as a source of new ideas and new ways to explain old ones. And where the coupling between the two is as gut-obvious as day and night. (2) prove or disprove: for all e0, there exists d0, if 0bad, then (a-b)/sqrt(b) e I grant you that clearly the implicit quantifiers for a and b are for all. The unclear part is where to put them. There are essentially 4 choices That's a stretch. It's all in the context, and here it's clearly a continuity verification exercise from freshman calculus. Unless being deliberately obtuse, one has no excuse not inferring where the quantifiers go if one knows about a theorem prover, what more wielding one to nuke this gnat of a proof. Moreover, if we grant the imaginary student the rudiments of logic, 3 of the 4 choices render the statement vacuously true. Almost. Set d to deny the antecedent, QED. I partly agree with Albert's main point, notwithstanding his choice of examples, that the absence of explicit quantifiers can lead to confusion. It all depends. On the other hand Alexander Solla is also on the money with his remark. A mathematician writes [1], In particular, any given assertion in hard analysis usually comes with a number of unsightly quantifiers (For every there exists an N…) which can require some thought for a reader to parse. (3) Newspaper headline: Someone gets hit by a car every 6 seconds. A few months ago, a good chunk of Devlin's Intro to Math Thinking massive online course devoted itself to explicit and precise placement of quantifiers. So not only is the above headline judged improperly worded and hence badly ambiguous, but also commonplaces like In case of fire do not use elevator. I'm a fervent believer against ambiguity: Let zealotry take its place. [1] http://terrytao.wordpress.com/2007/06/25/ultrafilters-nonstandard-analysis-and-epsilon-management/ -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
Hi Tillmann, On Wed, Apr 3, 2013 at 11:59 PM, Tillmann Rendel ren...@informatik.uni-marburg.de wrote: From the type-theoretic point of view, I guess this is related to your view of what a polymorphic function is. Do you have a reference to the previous conversation? but we moved further and further towards the System-F-ish view that polymorphism is an explicit, computational thing. While that may be true, I read the original email as merely referring to the explicit annotation of types (where they are customarily neither seen nor written) as a particular pedagogical approach for new students, something which has much to recommend for. Which seems miles away from what you're alluding to. Full-blown type-level programming? Operational semantics at the type-level? I'm not sure. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsec community and up-to-date documentation
On Mon, Mar 25, 2013 at 5:19 AM, Konstantine Rybnikov k...@k-bx.com wrote: as a beginner had a lot of headache starting from outdated documentation in various places, lack of more tutorials, confusion between Text.Parsec and Text.ParseCombinator modules and so on. You're indeed right. While I solved most of my problems via googling / reading stackoverflow / reading source code (of outdated version first, btw, the one I got from Daan's homepage :), I still had a feeling all the time that I'm doing something wrong and that I can't find place where party is going on. If you look at the dates of the papers on Wikipedia [1], the party was totally hoppin' in the last decade of the previous century. Not so much since. Sigh. So I wondered, what can I do to create a community around Parsec, to get issue tracking, pull-requests, up-to-date comprehensive documentation and tutorials etc.? Parsec seems like a perfect candidate for something like this. While the experience is still fresh in your mind, may I suggest that you write a note or two on the most confusing things you encountered and how you dealt with them? Making your notes public is a way of gathering a community around shared experiences. Also, the denizens of the haskell IRC at freenode will gladly converse with you about parsec. The same goes for subscribers to this list and also haskell-beginners. [1] http://en.wikipedia.org/wiki/Parser_combinator -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Need some advice around lazy IO
On Tue, Mar 19, 2013 at 2:01 PM, Konstantin Litvinenko to.darkan...@gmail.com wrote: Yes. You (and Dan) are totally right. 'Let' just bind expression, not evaluating it. Dan's evaluate trick force rnf to run before hClose. As I said - it's tricky part especially for newbie like me :) To place this in perspective, one only needs to descend one or two more layers before the semantics starts confusing even experts. Whereas the difference between seq and evaluate shouldn't be too hard to grasp, that between evaluate and (return $!) is considerably more subtle, as Edward Yang notified us 10 days ago. See the thread titled To seq or not to seq. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Open-source projects for beginning Haskell students?
Question is: does the task even have to involve the the production of Haskell code? Is it possible that both the student and the community-at-large would benefit further from expository-style artifacts? Some possible activities: (1) producing documentation for popular packages that cater to different learning styles (e.g. styles: Little Schemer, RWH, LYAHFGG, etc.) (2) survey of the various approaches taken by similar packages, explaining the different choices taken (3) cheatsheets, whether of GHC extensions, packages, syntax, commonly used functions, etc. These don't have to be harder than they sound. Option (2) in particular could be e.g. a table listing the type signatures of the various Iteratee packages with regard to Iteratee, Enumerator, and Enumeratee. Or how a four-line Unix cat is implemented across them. It's been said that a good teacher doesn't cover material, he /uncovers/ them, i.e. the few core ideas that underpin everything. Well, Haskell is just this heap of everything that's pretty hard to dig under. Failing which, the indefatigable teacher would do well showing how the student can teach themselves. -- Kim-Ee On Mon, Mar 11, 2013 at 10:48 PM, Brent Yorgey byor...@seas.upenn.edu wrote: Hi everyone, I am currently teaching a half-credit introductory Haskell class for undergraduates. This is the third time I've taught it. Both of the previous times, for their final project I gave them the option of contributing to an open-source project; a couple groups/individuals took me up on it and I think it ended up being a modest success. So I'd like to do it again this time around, and am looking for particular projects I can suggest to them. Do you have an open-source project with a few well-specified tasks that a relative beginner (see below) could reasonably make a contribution towards in the space of about four weeks? I'm aware that most tasks don't fit that profile, but even complex projects usually have a few simple-ish tasks that haven't yet been done just because no one has gotten around to it yet. If you have any such projects, I'd love to hear about it! Just send me a paragraph or so describing your project and explaining what task(s) you could use help with --- something that I could put on the course website for students to look at. Here are a few more details: * The students will be working on the projects from approximately the end of this month through the end of April. During the next two weeks they would be contacting you to discuss the possibility of working on your project. * By relative beginner I mean someone familiar with the material listed here: http://www.cis.upenn.edu/~cis194/lectures.html and just trying to come to terms with Applicative and Monad. They definitely do not know much if anything about optimization/profiling, GADTs, the mtl, or Haskell-programming-in-the-large. (Although part of the point of the project is to teach them a bit about programming-in-the-(medium/large)). * What I would hope from you is a willingness to exchange email and/or chat with the student(s) over the course of the project, to give them a bit of guidance/mentoring. I am certainly willing to help on that front, but of course I probably don't know much about your particular project. Thanks! -Brent ___ 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] RFC: rewrite-with-location proposal
On Mon, Feb 25, 2013 at 9:42 PM, Simon Peyton-Jones simo...@microsoft.comwrote: One idea I had, which that page does not yet describe, is to have an implicit parameter, something like ?loc::Location** +1 Implicit params has a bad rap in some circles because of counterintuitive behavior when manually binding the parameter (the syntax is partly to blame). Since ?loc is never bound by hand, there should be no problems. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
On Sun, Feb 24, 2013 at 7:09 PM, Roman Cheplyaka r...@ro-che.info wrote: Thus, your recursion is well-founded — you enter the recursion with the input strictly smaller than you had in the beginning. Perhaps you meant /productive/ corecursion? Because the definition A ::= B A you gave is codata. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
On Sun, Feb 24, 2013 at 7:47 PM, Roman Cheplyaka r...@ro-che.info wrote: Or perhaps you meant that the production itself, when interpreted as a definition, is corecursive? I was merely thrown off by your mention of well-founded and the assertion that you're left with a strictly smaller input. I don't see any of this. That's when I remembered that well-founded recursion (a desirable) is sometimes confused with productive corecursion (another desirable). -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
On Sun, Feb 24, 2013 at 8:03 PM, Roman Cheplyaka r...@ro-che.info wrote: It may become more obvious if you try to write two recursive descent parsers (as recursive functions) which parse a left-recursive and a non-left-recursive grammars, and see in which case the recursion is well-founded and why. Which grammar are we discussing here? The one you outlined? A ::= B A As I pointed out earlier, this doesn't model a program (e.g. a compiler). It's an OS! What am I missing? -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
On Sun, Feb 24, 2013 at 10:04 PM, Tillmann Rendel ren...@informatik.uni-marburg.de wrote: The recursion is well-founded if (drop n1 text) is smaller then text. So we have two cases, as Roman wrote: If the language defined by B contains the empty string, then n1 can be 0, so the recursion is not well-founded and the parser might loop. Ah! So A ::= B A is really /not/ the full grammar of the language but an abbreviated one, minus terminals. At the very least, partial parses make sense and the input stream is assumed finite. Because A ::= B A could be understood, not so much as a parsing rule, but as the full definition of a language which comprises only one word: B ... ad infinitum. So all that mention of well-foundedness was confusing. Thanks, Tillmann! -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: monad-bool 0.1
On Thu, Jan 24, 2013 at 6:23 AM, wren ng thornton w...@freegeek.org wrote: NotOnHackage: a package repository just like Hackage, except the packages are just documentation on why there is no such package. Love the idea! It'll make us even more unique among other PLs and even more ways to be smug: A bigger set of libraries? So what? Haskell's the only one with a /negative/ repo. Eat your heart out, Python! ;) -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type hierarchy
On Wed, Jan 16, 2013 at 11:22 PM, Thiago Negri evoh...@gmail.com wrote: The C spec allows the use of GLboolean values where GLenums are expected. Some fixes off the top of my head (caveats apply): * define a lift :: GLboolean - GLenum * use a typeclass GLenumlike * if there aren't too many of them, roll a GLboolean specific function for every one taking GLenum -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A Meetup Group for MN Haskellers
Hey Danny, Good job taking the lead! Wish you all success because I think meetups have so many underrated benefits. (Where I am in a city 10 million, i.e. Jakarta, Indonesia, you'd think it would be a piece of cake, but so far no dice. Me and another guy are working on this ) Have you considered corralling a bunch of other FPers together, like the Bay Area FP group? Results from a search for Scala / Clojure Minneapolis look promising. -- Kim-Ee On Sat, Jan 12, 2013 at 10:32 PM, Danny Gratzer danny.grat...@gmail.comwrote: Hello, After seeing the post about Manchurian Haskellers I decided to start one for people in and around the Twin Cities. Here's the meetup page: http://www.meetup.com/HaskellMN/ If any Haskell guru's are lurking around here we'd love to have you give a talk! -- Danny Gratzer ___ 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] Object Oriented programming for Functional Programmers
On Fri, Jan 4, 2013 at 7:27 PM, David Thomas davidleotho...@gmail.comwrote: Well, hidden - it *is* right there in the type signature still, it just doesn't *look* like an argument. If you squint hard enough, (=) looks like (-). Or maybe the other way round. Whatever. :) It also might be optimized away in static cases (certainly, it *could* happen, whether does or is even worthwhile is another question). The optimization at stake is specialization. Given (Num a = a), specialize it to Int or Double or X so that it's memoizably first-class, which is where functions still fall down [1]. All functions are values but data values still play nicer than others. Isn't fixing this the real cure for the monomorphism restriction? [1] http://lukepalmer.wordpress.com/2009/07/07/emphasizing-specialization/#comment-862 -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
There's OOHaskell, which you can google for. The name's such a nice example of an aptronym: it's the Overlooked Object-oriented Haskell. -- Kim-Ee On Mon, Dec 31, 2012 at 2:58 AM, Daniel Díaz Casanueva dhelta.d...@gmail.com wrote: Hello, Haskell Cafe folks. My programming life (which has started about 3-4 years ago) has always been in the functional paradigm. Eventually, I had to program in Pascal and Prolog for my University (where I learned Haskell). I also did some PHP, SQL and HTML while building some web sites, languages that I taught to myself. I have never had any contact with JavaScript though. But all these languages were in my life as secondary languages, being Haskell my predominant preference. Haskell was the first programming language I learned, and subsequent languages never seemed so natural and worthwhile to me. In fact, every time I had to use another language, I created a combinator library in Haskell to write it (this was the reason that brought me to start with the HaTeX library). Of course, this practice wasn't always the best approach. But, why I am writing this to you, haskellers? Well, my curiosity is bringing me to learn a new general purpose programming language. Haskellers are frequently comparing Object-Oriented languages with Haskell itself, but I have never programmed in any OO-language! (perhaps this is an uncommon case) I thought it could be good to me (as a programmer) to learn C/C++. Many interesting courses (most of them) use these languages and I feel like limited for being a Haskell programmer. It looks like I have to learn imperative programming (with side effects all over around) in some point of my programming life. So my questions for you all are: * Is it really worthwhile for me to learn OO-programming? * If so, where should I start? There are plenty of functional programming for OO programmers but I have never seen OO programming for functional programmers. * Is it true that learning other programming languages leads to a better use of your favorite programming language? * Will I learn new programming strategies that I can use back in the Haskell world? Thanks in advance for your kind responses, Daniel Díaz. ___ 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] Non polymorphic numerals option -- avoiding type classes
Hi David, it looks like Rustom's aware that haskell's not lisp. What he really wants methinks is a way to suppress type classes altogether! That or a NoOverloadedNumerals extension. -- Kim-Ee On Thu, Dec 27, 2012 at 4:03 PM, David Virebayre dav.vire+hask...@gmail.com wrote: Prelude :t [[1,2],3] you have a list with 2 elements: - [1,2] - 3 the type of [1,2] is [Integer] the type of 3 is Integer But all elements in a list must have the same type. 2012/12/27 Rustom Mody rustompm...@gmail.com: On Thu, Dec 27, 2012 at 1:48 AM, Roman Cheplyaka r...@ro-che.info wrote: * Rustom Mody rustompm...@gmail.com [2012-12-26 20:12:17+0530] So is there any set of flags to make haskell literals less polymorphic? Yes, there is! % ghci -XRebindableSyntax GHCi, version 7.6.1: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. import Prelude hiding (fromInteger) Prelude let fromInteger = id Prelude :t 3 3 :: Integer Roman Thanks Roman -- that helps. And yet the ghci error is much more obscure than the gofer error: --- contents of .ghci --- :set -XRebindableSyntax let fromInteger = id -- ghci session - $ ghci GHCi, version 7.4.1: 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 :t 5 5 :: Integer Prelude :t [[1,2],3] interactive:1:8: Couldn't match expected type `[Integer]' with actual type `Integer' Expected type: Integer - [Integer] Actual type: Integer - Integer In the expression: 3 In the expression: [[1, 2], 3] - The same in gofer - Gofer session for: pustd.pre ? :t [[1,2],3] ERROR: Type error in list *** expression : [[1,2],3] *** term : 3 *** type : Int *** does not match : [Int] -- So the error is occurring at the point of the fromInteger (= id) but the message does not indicate that -- http://www.the-magus.in http://blog.languager.org ___ 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
Re: [Haskell-cafe] Non polymorphic numerals option -- avoiding type classes
On Thu, Dec 27, 2012 at 11:48 PM, Rustom Mody rustompm...@gmail.com wrote: On Thu, Dec 27, 2012 at 8:26 PM, Kim-Ee Yeoh k...@atamo.com wrote: What he really wants methinks is a way to suppress type classes altogether! That or a NoOverloadedNumerals extension. I'm not really sure about that... Look! Prelude :t [[1,2],3] [[1,2],3] :: (Num [t], Num t) = [[t]] As Satvik explained, well-typed does not imply instantiable. And with constraints, not instantiable /does/ imply not evaluable! :set -XRebindableSyntax let fromInteger = id Prelude :t [[1,2],3] Couldn't match expected type `[Integer]' with actual type `Integer' Expected type: Integer - [Integer] Actual type: Integer - Integer In the expression: 3 In the expression: [[1, 2], 3] You can see overloaded numerals at work again via the hidden hand of fromInteger. Presumably some imaginary NoOverloadedNumerals extension would thoroughly purge its presence. -- Kim-Ee On Thu, Dec 27, 2012 at 11:48 PM, Rustom Mody rustompm...@gmail.com wrote: On Thu, Dec 27, 2012 at 8:26 PM, Kim-Ee Yeoh k...@atamo.com wrote: Hi David, it looks like Rustom's aware that haskell's not lisp. What he really wants methinks is a way to suppress type classes altogether! That or a NoOverloadedNumerals extension. -- Kim-Ee I'm not really sure about that... Look! ghci with default startup $ ghci GHCi, version 7.4.1: 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 :t [[1,2],3] [[1,2],3] :: (Num [t], Num t) = [[t]] So it would appear that ghci is giving a well-typing for [[1,2], 3]. But is it? Prelude [[1,2],3] interactive:3:8: No instance for (Num [t0]) arising from the literal `3' Possible fix: add an instance declaration for (Num [t0]) In the expression: 3 In the expression: [[1, 2], 3] In an equation for `it': it = [[1, 2], 3] --- So is it well-typed in ghci or not?? And now we add Roman's suggestions... $ cat .ghci :set -XRebindableSyntax let fromInteger = id And run ghci again $ ghci GHCi, version 7.4.1: 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 :t [[1,2],3] interactive:1:8: Couldn't match expected type `[Integer]' with actual type `Integer' Expected type: Integer - [Integer] Actual type: Integer - Integer In the expression: 3 In the expression: [[1, 2], 3] Prelude [[1,2],3] interactive:3:8: Couldn't match expected type `[Integer]' with actual type `Integer' Expected type: Integer - [Integer] Actual type: Integer - Integer In the expression: 3 In the expression: [[1, 2], 3] Prelude So far so good -- when an expression is type-wrong, its 'wrongness' is the same irrespective of whether I ask for its type or evaluate it. But now we are in for new surprises: Try out f x y = x / y Prelude :l f [1 of 1] Compiling Main ( f.hs, interpreted ) f.hs:1:11: Not in scope: `/' Failed, modules loaded: none. Prelude (/) Oh is it that now integer literals are just plain Integers and cant be divided using '/' ?? So lets replace '/' with '+' f.hs:1:11: Not in scope: `+' And now I am at my wits end! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] MPTC or functional dependencies?
Petr, Your subject header is misleading: FDs don't make sense without MPTCs. As you acknowledge at the end, what you're ultimately asking is: to FD or not to FD. Note also, the contemporary debate has shifted to TFs (type families) vs FDs. -- Kim-Ee On Fri, Dec 21, 2012 at 7:38 PM, Petr P petr@gmail.com wrote: Dear Haskellers, I'm working on a small library for representing semigroup (or monoid) actions on a set http://hackage.haskell.org/package/semigroups-actions. The MultiParamTypeClasses extension seems to be best suited for the task, as a group can act on many sets, and a set can be acted on by different groups: -- | Represents an action of semigroup @g@ to set @a@. -- -- Laws: @'Endo' . 'act'@ must be a homomorphism of semigroups. class Semigroup g = SemigroupAct g a where act :: g - (a - a) But soon I realized that with MPTC the compiler has problems inferring types and I had to explicitly specify types when using `act` in many places. Because it seems that in most cases a set will have only a single group acting on it, I was thinking about using FDs: class Semigroup g = SemigroupAct g a | a - g where But on the other hand, this can limit the generality of the type class. I cannot decide which one I should choose. What would you suggest? According to your experience, would you choose plain MPTC or FD? Best regards, Petr Pudlak ___ 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] arr considered harmful
Hey Conal, I have something (another circuits formulation) that's almost an arrow but doesn't support arr. Have you seen Adam Megacz's generalized arrows? http://www.cs.berkeley.edu/~megacz/garrows/ -- Kim-Ee On Fri, Dec 21, 2012 at 7:55 AM, Conal Elliott co...@conal.net wrote: If you require the circuit to be parametric in the value types, you can limit the types of function you can pass to arr to simple plumbing. See the netlist example at the end of my Fun of Programming slides ( http://www.soi.city.ac.uk/~ross/papers/fop.html). I'm running into this same issue: I have something (another circuits formulation) that's almost an arrow but doesn't support arr. I'd like to use arrow notation, but then I run afoul of my missing arr. I'd like to understand Ross's suggestion and how to apply it. (I've read the FoP slides.) Ross: do you mean to say that you were able to implement arr and thus run your circuit examples via the standard arrow desugarer? Ryan: did you get a working solution to the problem you described for your Circuit arrow? Thanks. -- Conal On Mon, Oct 31, 2011 at 6:52 PM, Paterson, Ross r.pater...@city.ac.ukwrote: Ryan Ingram writes: Most of the conversion from arrow syntax into arrows uses 'arr' to move components around. However, arr is totally opaque to the arrow itself, and prevents describing some very useful objects as arrows. For example, I would love to be able to use the arrow syntax to define objects of this type: data Circuit a b where Const :: Bool - Circuit () Bool Wire :: Circuit a a Delay :: Circuit a a And :: Circuit (Bool,Bool) Bool Or :: Circuit (Bool,Bool) Bool Not :: Circuit Bool Bool Then :: Circuit a b - Circuit b c - Circuit a c Pair :: Circuit a c - Circuit b d - Circuit (a,b) (c,d) First :: Circuit a b - Circuit (a,c) (b,c) Swap :: Circuit (a,b) (b,a) AssocL :: Circuit ((a,b),c) (a,(b,c)) AssocR :: Circuit (a,(b,c)) ((a,b),c) Loop :: Circuit (a,b) (a,c) - Circuit b c etc. Then we can have code that examines this concrete data representation, converts it to VHDL, optimizes it, etc. However, due to the presence of the opaque 'arr', there's no way to make this type an arrow without adding an 'escape hatch' Arr :: (a - b) - Circuit a b which breaks the abstraction: circuit is supposed to represent an actual boolean circuit; (Arr not) is not a valid circuit because we've lost the information about the existence of a 'Not' gate. If you require the circuit to be parametric in the value types, you can limit the types of function you can pass to arr to simple plumbing. See the netlist example at the end of my Fun of Programming slides ( http://www.soi.city.ac.uk/~ross/papers/fop.html). ___ 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
Re: [Haskell-cafe] Substituting values
This is reminiscent of the Either (exception) monad where Left values, the
exceptions, pass through unaltered, and Right values are transformable,
i.e. acted on by functions.
But I have no idea what you're trying to achieve in the bigger picture.
Help us help you by fleshing out your use case.
-- Kim-Ee
On Sat, Dec 22, 2012 at 12:46 AM, Radical radi...@google.com wrote:
Sometimes I'll need something like:
if value == Foo then Bar else value
Or some syntactic variation thereof:
case value of { Foo - Bar; _ - value }
Is there a better/shorter way to do it? I'm surprised that it's more
complicated to substitute a value on its own than e.g. in a list, using
filter. Or perhaps I'm missing the right abstraction?
Thanks,
Alvaro
___
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] Exploring Programming Language Theory
SPJ's IFPL is an excellent starting point to learn the innards of Haskell. It allows a well-acculturated individual to grab the base of the trunk and start climbing the branches, which means reading the research papers (SPJ's website, mainly though not exclusively), all the way to the leaves (reading GHC source). To summarize, books that go from compiling a high level language to lambda calculus and/or the theory behind lambda calculus and similar? Other than Haskell? There's a comprehensive bibliography on the reading scheme website, which also has loads of links to theory you might be interested in. Gotta say though, reading is one thing, but you've got to check your understanding from time to time. Barendregt's bible on LC has good exercises. -- Kim-Ee On Sun, Dec 9, 2012 at 5:41 AM, Danny Gratzer danny.grat...@gmail.comwrote: Sorry for the multiple posts, last time I try to write any decent length email from my phone... Anyways, and that was a tutorial not an introduction. I am also reading his The Implementation of Functional Programming Languages. But in any case, I'm liking these books a lot! It's super interesting and everything but a little out of date. Does anyone know of books that cover a similar subject matter but are more current? To summarize, books that go from compiling a high level language to lambda calculus and/or the theory behind lambda calculus and similar? Thank you so much! On Sat, Dec 8, 2012 at 4:32 PM, Danny Gratzer danny.grat...@gmail.comwrote: Hello, Sorry in advance for the soft question: Recently I have been studying more about how a lazy functional language is designed and compiled and have been reading Peyton-Jones's book implementing functional languages: an introduction -- Danny Gratzer ___ 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] Exploring Programming Language Theory
I should add that IFPL has important chapters written by authors other than Simon. -- Kim-Ee On Sun, Dec 9, 2012 at 5:58 AM, Kim-Ee Yeoh k...@atamo.com wrote: SPJ's IFPL is an excellent starting point to learn the innards of Haskell. It allows a well-acculturated individual to grab the base of the trunk and start climbing the branches, which means reading the research papers (SPJ's website, mainly though not exclusively), all the way to the leaves (reading GHC source). To summarize, books that go from compiling a high level language to lambda calculus and/or the theory behind lambda calculus and similar? Other than Haskell? There's a comprehensive bibliography on the reading scheme website, which also has loads of links to theory you might be interested in. Gotta say though, reading is one thing, but you've got to check your understanding from time to time. Barendregt's bible on LC has good exercises. -- Kim-Ee On Sun, Dec 9, 2012 at 5:41 AM, Danny Gratzer danny.grat...@gmail.comwrote: Sorry for the multiple posts, last time I try to write any decent length email from my phone... Anyways, and that was a tutorial not an introduction. I am also reading his The Implementation of Functional Programming Languages. But in any case, I'm liking these books a lot! It's super interesting and everything but a little out of date. Does anyone know of books that cover a similar subject matter but are more current? To summarize, books that go from compiling a high level language to lambda calculus and/or the theory behind lambda calculus and similar? Thank you so much! On Sat, Dec 8, 2012 at 4:32 PM, Danny Gratzer danny.grat...@gmail.comwrote: Hello, Sorry in advance for the soft question: Recently I have been studying more about how a lazy functional language is designed and compiled and have been reading Peyton-Jones's book implementing functional languages: an introduction -- Danny Gratzer ___ 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] mtl: Why there is Monoid w constraint in the definition of class MonadWriter?
The only thing we can tell from the Monad laws is that that function f should be associative. That f is associative is a very small step away from f forming a monoid. What about listen :: m a - m (w, a)? What laws should it hold that are compatible with those of the monad and those of tell? Reasoning about listen is enough to force the existence of a monoid identity. -- Kim-Ee On Sun, Dec 9, 2012 at 5:41 AM, Roman Cheplyaka r...@ro-che.info wrote: * Edward Z. Yang ezy...@mit.edu [2012-12-08 14:18:38-0800] Excerpts from Roman Cheplyaka's message of Sat Dec 08 14:00:52 -0800 2012: * Edward Z. Yang ezy...@mit.edu [2012-12-08 11:19:01-0800] The monoid instance is necessary to ensure adherence to the monad laws. This doesn't make any sense to me. Are you sure you're talking about the MonadWriter class and not about the Writer monad? Well, I assume the rules for Writer generalize for MonadWriter, no? Here's an example. Haskell monads have the associativity law: (f = g) = h === f = (g = h) From this, we can see that (m1 m2) m3 === m1 (m2 m3) Now, consider tell. We'd expect it to obey a law like this: tell w1 tell w2 === tell (w1 w2) First of all, I don't see why two tells should be equivalent to one tell. Imagine a MonadWriter that additionally records the number of times 'tell' has been called. (You might argue that your last equation should be a MonadWriter class law, but that's a different story — we're talking about the Monad laws here.) Second, even *if* the above holds (two tells are equivalent to one tell), then there is *some* function f such that tell w1 tell w2 == tell (f w1 w2) It isn't necessary that f coincides with mappend, or even that the type w is declared as a Monoid at all. The only thing we can tell from the Monad laws is that that function f should be associative. Roman ___ 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] Design of a DSL in Haskell
Joerg, For definitions I'd search for Andres Loeh and haskell edsl. His PDF slides also have code examples which'll help. Lennart also gave a talk this year titled making edsls fly. The video is on the web. If you have specific questions bring them to the list! The community is a tremendous resource! -- Kim-Ee On Wed, Dec 5, 2012 at 2:09 PM, Joerg Fritsch frit...@joerg.cc wrote: Kim-Eeh, Tillmann, I am interested in the definition of deep vs shallow embedded, even if it is not featured in the Fowler textbook. Fowler that is one textbook only and I am not focused on it. --Joerg On Dec 5, 2012, at 2:59 AM, Kim-Ee Yeoh wrote: On Wed, Dec 5, 2012 at 8:32 AM, Tillmann Rendel ren...@informatik.uni-marburg.de wrote: I mean internal == embedded, independently of deep vs. shallow, following Martin Fowler [1]. [1] http://martinfowler.com/bliki/**DomainSpecificLanguage.htmlhttp://martinfowler.com/bliki/DomainSpecificLanguage.html If I look here [2] I see: An *internal DSL* is just a particular idiom of writing code in the host language. So a Ruby internal DSL is Ruby code, just written in particular style which gives a more language-like feel. As such they are often called *Fluent Interfaces* or*Embedded DSLs*. An *external DSL* is a completely separate language that is parsed into data that the host language can understand. Fowler places undue emphasis on the completely separate language, but other than that, the correspondence is clear. I wonder how he thinks about C implementing C? Or ghc implementing haskell in haskell? Would he say, Well, clearly C and haskell are not DSLs, they are general purpose languages!? [2] http://martinfowler.com/bliki/DslQandA.html -- Kim-Ee __**_ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://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] Design of a DSL in Haskell
On Tue, Dec 4, 2012 at 4:53 PM, Joerg Fritsch frit...@joerg.cc wrote: is a shallow embedded DSL == an internal DSL and a deeply embedded DSL == an external DSL or the other way around? Roughly speaking, yes. But a deep DSL doesn't mean you've got to have a parser tokenizer IO input. You can get a deep DSL merely from the free monad construction. -- Kim-Ee On Tue, Dec 4, 2012 at 4:53 PM, Joerg Fritsch frit...@joerg.cc wrote: Hi Tillmann, is a shallow embedded DSL == an internal DSL and a deeply embedded DSL == an external DSL or the other way around? --Joerg On Dec 3, 2012, at 11:40 PM, Tillmann Rendel wrote: Hi, Joerg Fritsch wrote: I am working on a DSL that eventuyally would allow me to say: import language.cwmwl main = runCWMWL $ do eval (isFib::, 1000, ?BOOL) I have just started to work on the interpreter-function runCWMWL and I wonder whether it is possible to escape to real Haskell somehow (and how?) either inside ot outside the do-block. You can already use Haskell in your DSL. A simple example: main = runCWMWL $ do eval (isFib::, 500 + 500, ?BOOL) The (+) operator is taken from Haskell, and it is available in your DSL program. This use of Haskell is completely for free: You don't have to do anything special with your DSL implementation to support it. I consider this the main benefit of internal vs. external DSLs. A more complex example: main = runCWMWL $ do foo - eval (isFib::, 1000, ?BOOL) if foo then return 27 else return 42 Here, you are using the Haskell if-then-else expression to decide which DSL program to run. Note that this example also uses (=) and return, so it only works because your DSL is monadic. Beyond writing the Monad instance, you don't have to do anything special to support this. In particular, you might not need an additional embed function if you've already implemented return from the Monad type class. I consider this the main benefit of the Monad type class. Tillmann ___ 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] Design of a DSL in Haskell
Little things to check understanding: * ghc/ghci implements a DSL called Haskell -- does it do so in a deep or shallow way? * where are the shallow DSLs? the deep ones? (hint: some of them are right under our very noses!) -- Kim-Ee On Wed, Dec 5, 2012 at 12:49 AM, Stephen Tetley stephen.tet...@gmail.comwrote: In Haskell, shallow DSLs generate values - deep DSLs generate structures (typically abstract syntax trees), the structure can subsequently be used to generate a value (or a C program, or a HTML page, etc.). See Andy Gill and colleagues Types and Type Families for Hardware Simulation and Synthesis, The Internals and Externals of Kansas Lava for a fuller definition. http://www.ittc.ku.edu/csdl/fpg/sites/default/files/Gill-10-TypesKansasLava.pdf Other communities may have their own definitions. On 4 December 2012 10:01, Kim-Ee Yeoh k...@atamo.com wrote: On Tue, Dec 4, 2012 at 4:53 PM, Joerg Fritsch frit...@joerg.cc wrote: is a shallow embedded DSL == an internal DSL and a deeply embedded DSL == an external DSL or the other way around? Roughly speaking, yes. But a deep DSL doesn't mean you've got to have a parser tokenizer IO input. You can get a deep DSL merely from the free monad construction. -- Kim-Ee ___ 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] Design of a DSL in Haskell
On Wed, Dec 5, 2012 at 8:32 AM, Tillmann Rendel ren...@informatik.uni-marburg.de wrote: I mean internal == embedded, independently of deep vs. shallow, following Martin Fowler [1]. [1] http://martinfowler.com/bliki/**DomainSpecificLanguage.htmlhttp://martinfowler.com/bliki/DomainSpecificLanguage.html If I look here [2] I see: An *internal DSL* is just a particular idiom of writing code in the host language. So a Ruby internal DSL is Ruby code, just written in particular style which gives a more language-like feel. As such they are often called *Fluent Interfaces* or*Embedded DSLs*. An *external DSL* is a completely separate language that is parsed into data that the host language can understand. Fowler places undue emphasis on the completely separate language, but other than that, the correspondence is clear. I wonder how he thinks about C implementing C? Or ghc implementing haskell in haskell? Would he say, Well, clearly C and haskell are not DSLs, they are general purpose languages!? [2] http://martinfowler.com/bliki/DslQandA.html -- Kim-Ee __**_ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://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] Is anyone working on a sparse matrix library in Haskell?
On Sun, Dec 2, 2012 at 10:52 AM, wren ng thornton w...@freegeek.org wrote: My goal for all this is in setting up the type system, not performance. I figure there are other folks who know and care a lot more about the numerical tricks of giving the actual implementations. You've got my support -- old-school optimizations, numerical, compiler, or otherwise, are deadly boring. Death to them, I say! If we don't explore uncharted waters, who will? -- Kim-Ee On Sun, Dec 2, 2012 at 10:52 AM, wren ng thornton w...@freegeek.org wrote: On 11/30/12 4:58 PM, Mark Flamer wrote: Thanks for all the replies, It sounds like there is enough interest and even some potential collaborators out there. I have created a few data structures to represent sparse vectors and matrices. The vector was a simple binary tree and the matrix a quad tree. As I suspected a standard IntMap was around 3X as fast as my binary tree, so I have switched to the IntMap for now. I was hoping to hold on to my quad tree for the matrix rep. because I like the elegance of the recursive algorithms like Strassen’s for multiplication. In the end it will most likely be best to have a few different matrix representations anyway. For instance, I know that compressed row form is most efficient for certain algorithms. I have a Gauss iterative solver working currently and am thinking of moving on to a parallel Conjugate gradient or direct solver using LU decomposition. I’m no expert in Haskell or numeric methods but I do my best. I've also been working haphazardly on some similar stuff lately. However, my focus is rather different[1] so I'm afeared not much code sharing could happen at the moment. While I'm certainly no expert on numerical methods, I seem to have acquired some experience in that domain so I may be able to lend a hand from time to time. [1] In particular my goal has been to revive some old ideas about making linear algebra well-typed. The vast majority (if not all) of extant linear algebra systems are poorly typed and will do stupid things to resolve type errors (e.g., automatically padding, truncating, and reshaping things). Because of the use case I have in mind, this project also involves setting up a proper numerical type-class hierarchy (i.e., one which expresses semirings and other things ignored by the numerical hierarchies out there today). My goal for all this is in setting up the type system, not performance. I figure there are other folks who know and care a lot more about the numerical tricks of giving the actual implementations. -- Live well, ~wren __**_ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://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] How to incrementally update list
On Sat, Dec 1, 2012 at 1:16 AM, Mark Thom markjordant...@gmail.com wrote: Is there a paper or other single resource that will help me thoroughly understand non-strictness in Haskell? If performance is utterly vital the best resource is Core, as in, the ability to read it. The order of evaluation is all laid out there. Don [1] and Johan [2] have written variously about it. [1] http://stackoverflow.com/questions/6121146/reading-ghc-core [2] http://blog.johantibell.com/2012/02/forcing-values-returned-from-monadic.html -- Kim-Ee On Sat, Dec 1, 2012 at 1:16 AM, Mark Thom markjordant...@gmail.com wrote: Haskell's laziness is tricky to understand coming from imperative languages, but once you figure out its evaluation rules, you'll begin to see the elegance. Is there a paper or other single resource that will help me thoroughly understand non-strictness in Haskell? Once my programs hit a certain level of complexity, their behaviour becomes much harder for me to predict. I've been using the wiki pages up to this point, but apparently they haven't pushed my understanding of laziness nearly far enough. ___ 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] Why Kleisli composition is not in the Monad signature?
Ben, Now, on to Bind: the standard finite structure example for Bind is most probably the substitution thingy ... Danger of conflating a bunch of things here: (1) the substitution monadic effect is always also applicative and always also unital/pointed because monads are always applicative and pointed. (2) the zippy applicative effect is NOT monadic (see main applicative paper) (3) for finite structures, there's even a pre-applicative-but-still-zippy-ish Apply effect that's apparently NOT unital/pointed. I don't know of any results that crystallize this intuition about finite/infinite cleanly distributing itself into Applicative and Apply bins. (4) all the above has thus far been functors! Gershom has explained a use case where Apply isn't even one. HTH, -- Kim-Ee On Sat, Dec 1, 2012 at 5:00 AM, Ben Franksen ben.frank...@online.de wrote: Gershom Bazerman wrote: On 11/30/12 10:44 AM, Dan Doel wrote: Lists! The finite kind. This could mean Seq for instance. On Nov 30, 2012 9:53 AM, Brent Yorgey byor...@seas.upenn.edu mailto:byor...@seas.upenn.edu wrote: Any data type which admits structures of arbitrary but *only finite* size has a natural zippy Apply instance but no Applicative (since pure would have to be an infinite structure). The Map instance I mentioned above falls in this category. Though I guess I'm having trouble coming up with other examples, but I'm sure some exist. Maybe Edward knows of other examples. Another common case would be an embedded DSL representing code in a different language, targeting a different platform (or even an FPGA or the like), etc. You can apply `OtherLang (a - b)` to an `OtherLang a` and get an `OtherLang b`, but you clearly can't promote (or lower, I guess) an arbitrary Haskell function into a function in your target language. This is the same reason that GArrows remove the `arr` function (http://www.cs.berkeley.edu/~megacz/garrows/). A fine example! And I am getting the drift... yes, this could be a useful abstraction. Now, on to Bind: the standard finite structure example for Bind is most probably the substitution thingy, i.e. if m :: m a, f :: a - m b, then m = f means replace all elements x :: a in m with f x and then flatten the result so it's an m b again. Like concatMap for lists, right? So, there is no return for that in the Map case for exactly the same reason as with Apply: the unit would have have value id for every possible key, so cannot be finite. So what about an example for Bind\\Monad that is not yet another variation of the finite structure theme? Cheers -- Ben Franksen () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ 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] How to incrementally update list
I want to incrementally update list lot of times, but don't know how to do this. Are you using the right data structure for the job? Maybe you want an array instead? -- Kim-Ee On Wed, Nov 28, 2012 at 6:43 PM, Branimir Maksimovic bm...@hotmail.comwrote: Problem is following short program: list = [1,2,3,4,5] advance l = map (\x - x+1) l run 0 s = s run n s = run (n-1) $ advance s main = do let s = run 5000 list putStrLn $ show s I want to incrementally update list lot of times, but don't know how to do this. Since Haskell does not have loops I have to use recursion, but problem is that recursive calls keep previous/state parameter leading to excessive stack.and memory usage. I don't know how to tell Haskell not to keep previous state rather to release so memory consumption becomes managable. Is there some solution to this problem as I think it is rather common? ___ 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] cabal configure cabal build cabal install
Nice tip, Albert! Good to know! One question I have is, is (runghc Setup.lhs) equivalent to (cabal) in runghc Setup.lhs $ [configure, build, install] ? On Mon, Nov 26, 2012 at 8:08 AM, Brent Yorgey byor...@seas.upenn.eduwrote: [cabal haddock, if you want] cabal copy cabal register Even this does not do the same thing as 'cabal install', because it does not download and install any dependencies (whereas 'cabal install' does). Brent, that's useful to know too, thanks! Fwiw, I think Albert had the backdrop of classic GNU autoconf in mind, predating all that newfangled stuff of downloading (!) dependencies (!!). -- Kim-Ee -Brent ___ 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] Compilers: Why do we need a core language?
Is it impossible (very hard) to directly translate high-level language into machine code? There's a context to your question I don't understand, so let me ask: Wouldn't it be easier to break a big step into smaller baby steps? And if it's indeed easier why wouldn't you choose that route? -- Kim-Ee On Tue, Nov 20, 2012 at 6:54 PM, c...@lavabit.com wrote: 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 directly translate high-level language into machine code? ___ 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] [Off-topic] How unimportant it is whether submarines can swim (EWD1056)
On Sun, Oct 28, 2012 at 11:29 AM, Rustom Mody rustompm...@gmail.com wrote: In particular, there is one small notational point that he insisted on towards the end of his career (and life) viz. where traditional mathematicians write *f(x) *and functional programmers write *f x*, he would write *f.x* , ie he showed apply with a '.' In trying to understand his intentions, I wrote the following 'thought-dialogue' [as in thought-experiment :-) ] http://www.the-magus.in/Publications/ewd.pdf I didn't read all of it, but near the end when EWD made the point about how function application should be a first-class operator and not mere whitespace, Haskeller missed a golden opportunity to segue into applicative functors. -- Kim-Ee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?
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 (η that I may have erroneously written ε in some previous mail) defines a monad (and requires some additionnal law). Auger: Your emails keep invoking the mathematical point of view as if it were something unique and universal. Mathematical definitions are created and adopted to the extent that they give rise to interesting, meaningful proofs. Coding in Haskell is precisely proving theorems in a branch of constructive mathematics. Its practitioners have found one set of monad definitions more intuitive and sensible when working on such proofs than another such set. I don't understand your dogmatism about return and join being canonically the best monad definition in all possible mathematics. That's truly a quantifier that beggars imagination. -- Kim-Ee On Tue, Oct 16, 2012 at 9:37 PM, 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, but that tends to not be terribly important for most cases, either. Join is not the most important, but I do think it's often easier to define than bind. I often find myself implementing bind by explicitly using join. 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, it is not always possible (see the Monad/Functor problem). As I said, from the mathematical point of view, join (often noted μ in category theory) is the (natural) transformation which with return (η that I may have erroneously written ε in some previous mail) defines a monad (and requires some additionnal law). As often some points it out, Haskellers are not very right in their definition of Monad, not because of the bind vs join (in fact in a Monad either of them can be defined from the other one), but because of the functor status of a Monad. A monad, should always be a functor (at least to fit its mathematical definition). And this problem with the functor has probably lead to the use of bind (which is polymorphic in two type variables) rather than join (which has only one type variable, and thus is simpler). The problem, is that when 'm' is a Haskell Monad which does not belong to the Functor class, we cannot define 'bind' in general from 'join'. That is in the context where you have: return:∀ a. a → (m a) join:∀ a. (m (m a)) → (m a) x:m a f:a → (m b) you cannot define some term of type 'm b', since you would need to use at the end, either 'f' (and you would require to produce a 'a' which would be impossible), or 'return' (and you would need to produce a 'b', which is impossible), or 'join' (and you would need to produce a 'm (m b)', and recursively for that you cannot use return which would make you go back to define a 'm b' term) For that, you need the 'fmap' operation of the functor. return:∀ a. a → (m a) join:∀ a. (m (m a)) → (m a) fmap:∀ a b. (a→b) → ((m a)→(m b)) x:m a f:a → (m b) in this context defining a term of type 'm b' is feasible (join (fmap f x)), so that you can express bind = \ x f - join (fmap f x). To sum up, mathematical monads are defined from 'return' and 'join' as a mathematical monad is always a functor (so 'fmap' is defined, and 'bind', which is more complex than 'join' can be defined from 'join' and 'fmap'). Haskell does not use a very good definition for their monads, as they may not be instance of the Functor class (although most of them can easily be defined as such), and without this 'fmap', 'join' and 'return' would be pretty useless, as you wouldn't be able to move from a type 'm a' to a type 'm b'. ___ 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] Which advanced Haskell topics interest you
Something to consider is that it's not so much whether the material is basic, advanced, or intermediate; it's that the way it's being presented is boring and ineffective. Take the Head First Java book, which was deliberately engineered to overcome precisely this hitherto neglected aspect of technical teaching. There's a lot we can learn from how that book was put together because it's done wonders for onboarding java developers. A summary of what makes the book different: http://books.google.com/books?id=lXEBwv0LYogCpg=PR22source=gbs_selected_pagescad=3 -- Kim-Ee On Thu, Oct 4, 2012 at 9:43 PM, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: Most existing Haskell books and similar teaching material is aimed at programmers who are new to Haskell. This survey is to assess the community interest in teaching material covering advanced topics beyond the commonly taught introductory material. https://docs.google.com/spreadsheet/viewform?formkey=dE1QZFNRLTFMdkllYWIyR2FkYnRzZHc6MQ Manuel ___ 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] Church vs Boehm-Berarducci encoding of Lists
Both are excellent points, thank you. Your mention of general recursion prompts the following: in 1995, ten years after publication of Boehm-Berarducci, Launchbury and Sheard investigated transformation of programs written in general recursive form into build-foldr form, with an eye towards the normalization laid out in A Fold for All Seasons. LS does not cite BB. Could they be the same algorithm? -- Kim-Ee On Wed, Sep 26, 2012 at 11:41 AM, o...@okmij.org wrote: Wouldn't you say then that Church encoding is still the more appropriate reference given that Boehm-Berarducci's algorithm is rarely used? When I need to encode pattern matching it's goodbye Church and hello Scott. Aside from your projects, where else is the B-B procedure used? First of all, the Boehm-Berarducci encoding is inefficient only when doing an operation that is not easily representable as a fold. Quite many problems can be efficiently tackled by a fold. Second, I must stress the foundational advantage of the Boehm-Berarducci encoding: plain System F. Boehm-Berarducci encoding uses _no_ recursion: not at the term level, not at the type level. In contrast, the efficient for pattern-match encodings need general recursive types. With such types, a fix-point combinator becomes expressible, and the system, as a logic, becomes inconsistent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Thu, Sep 20, 2012 at 3:15 PM,o...@okmij.org wrote:
Incidentally, there is more than one way to build a predecessor of Church
numerals. Kleene's solution is not the only one.
Wouldn't you say then that Church encoding is still the more appropriate
reference given that Boehm-Berarducci's algorithm is rarely used? And also
that on discovering Church numerals in the untyped setting, one easily sees
how to get it to work in Haskell? Even when one has no inkling of the
larger picture of the embedding into System F?
When I need to encode pattern matching it's goodbye Church and hello Scott.
Aside from your projects, where else is the B-B procedure used?
-- Kim-Ee
On Thu, Sep 20, 2012 at 3:15 PM, o...@okmij.org wrote:
Dan Doel wrote:
P.S. It is actually possible to write zip function using
Boehm-Berarducci
encoding:
http://okmij.org/ftp/Algorithms.html#zip-folds
If you do, you might want to consider not using the above method, as I
seem to recall it doing an undesirable amount of extra work (repeated
O(n) tail).
It is correct. The Boehm-Berarducci web page discusses at some extent
the general inefficiency of the encoding, the need for repeated
reflections and reifications for some (but not all) operations. That
is why arithmetic on Church numerals is generally a bad idea.
A much better encoding of numerals is what I call P-numerals
http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals
It turns out, I have re-discovered them after Michel Parigot (so my
name P-numerals is actually meaningful). Not only they are faster; one
can _syntactically_ prove that PRED . SUCC is the identity.
The general idea of course is Goedel's recursor R.
R b a 0 = a
R b a (Succ n) = b n (R b a n)
which easily generalizes to lists. The enclosed code shows the list
encoding that has constant-time cons, head, tail and trivially
expressible fold and zip.
Kim-Ee Yeoh wrote:
So properly speaking, tail and pred for Church-encoded lists and nats
are trial-and-error affairs. But the point is they need not be if we
use B-B encoding, which looks _exactly_ the same, except one gets a
citation link to a systematic procedure.
So it looks like you're trying to set the record straight on who actually
did what.
Exactly. Incidentally, there is more than one way to build a
predecessor of Church numerals. Kleene's solution is not the only
one. Many years ago I was thinking on this problem and designed a
different predecessor:
excerpted from http://okmij.org/ftp/Haskell/LC_neg.lhs
One ad hoc way of defining a predecessor of a positive numeral
predp cn+1 == cn
is to represent predp cn as cn f v
where f and v are so chosen that (f z) acts as
if z == v then c0 else (succ z)
We know that z can be either a numeral cn or a special value v. All
Church numerals have a property that (cn combI) is combI: the identity
combinator is a fixpoint of every numeral. Therefore, ((cn combI) (succ
cn)) reduces to (succ cn). We only need to choose the value v in such
a way that ((v I) (succ v)) yields c0.
predp = eval $
c ^ c
# (z ^ (z # combI # (succ # z))) -- function f(z)
# (a ^ x ^ c0) -- value v
{-# LANGUAGE Rank2Types #-}
-- List represented with R
newtype R x = R{unR :: forall w.
-- b
(x - R x - w - w)
-- a
- w
-- result
- w}
nil :: R x
nil = R (\b a - a)
-- constant type
cons :: x - R x - R x
cons x r = R(\b a - b x r (unR r b a))
-- constant time
rhead :: R x - x
rhead (R fr) = fr (\x _ _ - x) (error head of the empty list)
-- constant time
rtail :: R x - R x
rtail (R fr) = fr (\_ r _ - r) (error tail of the empty list)
-- fold
rfold :: (x - w - w) - w - R x - w
rfold f z (R fr) = fr (\x _ w - f x w) z
-- zip is expressed via fold
rzipWith :: (x - y - z) - R x - R y - R z
rzipWith f r1 r2 = rfold f' z r1 r2
where f' x tD = \r2 - cons (f x (rhead r2)) (tD (rtail r2))
z = \_ - nil
-- tests
toR :: [a] - R a
toR = foldr cons nil
toL :: R a - [a]
toL = rfold (:) []
l1 = toR [1..10]
l2 = toR abcde
t1 = toL $ rtail l2
-- bcde
t2 = toL $ rzipWith (,) l2 l1
-- [('a',1),('b',2),('c',3),('d',4),('e',5)]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
Oleg,
Let me try to understand what you're saying here:
(1) Church encoding was discovered and investigated in an untyped setting.
I understand your tightness criterion to mean surjectivity, the absence of
which means having to deal with junk.
(2) Church didn't give an encoding for pattern-matching to match with
construction. Boehm and Berarducci did. So properly speaking, tail and pred
for Church-encoded lists and nats are trial-and-error affairs. But the
point is they need not be if we use B-B encoding, which looks _exactly_ the
same, except one gets a citation link to a systematic procedure.
So it looks like you're trying to set the record straight on who actually
did what.
-- Kim-Ee
On Tue, Sep 18, 2012 at 3:27 PM, o...@okmij.org wrote:
There has been a recent discussion of ``Church encoding'' of lists and
the comparison with Scott encoding.
I'd like to point out that what is often called Church encoding is
actually Boehm-Berarducci encoding. That is, often seen
newtype ChurchList a =
CL { cataCL :: forall r. (a - r - r) - r - r }
(in
http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hshttp://community.haskell.org/~wren/list-extras/Data/List/Church.hs
)
is _not_ Church encoding. First of all, Church encoding is not typed
and it is not tight. The following article explains the other
difference between the encodings
http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
Boehm-Berarducci encoding is very insightful and influential. The
authors truly deserve credit.
P.S. It is actually possible to write zip function using Boehm-Berarducci
encoding:
http://okmij.org/ftp/ftp/Algorithms.html#zip-folds
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Where are the haskell elders?
Something I've noticed is the phenomenon of Help Vampires [1] on this list. Amy Hoy: As soon as an open source project, language, or what- have-you achieves a certain notoriety—its half-life, if you will— they swarm in, seemingly draining the very life out of the community itself. She proceeds to give some tips on handling vampires. Let me excerpt from #2 Cease Enabling Behavior: * Enforce autonomy. No matter how beneficent you’re feeling, never directly answer a common question. * Foster thinking. Even if it’s not a question you see go bye fifty times a day… don’t answer it with a direct fix (unless the person is a known non-vamp, or it’s a real puzzler). * Reward self-help and helping others. Thank people who ask intelligent questions and do research first, and people who make an effort to help others. Tell them they’re a credit to the community. [1] http://slash7.com/2006/12/22/vampires/ The post was apparently written as a follow-up to [2] that meditated on why the Ruby on Rails community wasn't as good as it used to be. [2] http://slash7.com/2006/03/22/s-o-s-save-our-sanity/ Lennart Augustsson wrote: What Don said. 2010/3/29 Don Stewart d...@galois.com: gue.schmidt: Hi all, I notice that posts from the Haskell elders are pretty rare now. Only every now and then we hear from them. How come? Because there is too much noise on this list, Günther -- Don -- View this message in context: http://old.nabble.com/Where-are-the-haskell-elders--tp28076211p28140624.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] (liftM join .) . mapM
I'd write it as foo f = join .$ sequence . (f $) where (.$) :: (.$) :: Functor f = (a - b) - ((x - f a) - (x - f b)) x .$ y = (x $) . y is part of my line-noise toolbox. This join .* sequence family of functions is quite common. Should really have a name for them. Tony Morris-4 wrote: Can (liftM join .) . mapM be improved? (Monad m) = (a - m [b]) - [a] - m [b] -- View this message in context: http://old.nabble.com/%28liftM-join-.%29-.-mapM-tp26953786p26954040.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finally tagless and abstract relational Algebra
Günther Schmidt wrote: Initially I had simply imported the CSV files into empty tables in a database and done the calculations directly in SQL, never ever again! [snip] But my 1st goal here is to express the algorithm. Sounds like you want a better DSL than SQL. You're in massive company. Conal gives a lot of useful advice on DSL design. One way to start is to articulate existing pain. Where and why is SQL painful? Another trick is to work backwards: What kind of code do you really want to write? Whether you employ GADTs, initial datatypes, finally-tagless codata, etc. isn't really relevant at this stage. Prematurely latching on to a particular tool gets everything treated like a nail, even when they're nowhere close. -- View this message in context: http://old.nabble.com/Finally-tagless-and-abstract-relational-Algebra-tp26943949p26954686.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finally tagless and abstract relational Algebra
The code we want to write is that which matches the way we think [snip] My way is to think hard about what the best way to think about things is. I'm in two minds. On the one hand, we're in violent agreement: The code we /want/ to write is that which matches the way we /want/ to think, genuflecting, as it were, before the cold altar of mathematical perfection. On the other hand, with a view towards AI, I'd want to code just the way I now currently think, warts and all, except that I've designed the DSL to fix all my idiosyncrasies, hidden contexts, annoying ambiguities, utter silliness, etc. You might claim that the former is easier and more achievable. I don't see why. It seems likely that the kind of perfection you seek can only be obtained by piercing insights into the nature of the mind's present drosses (if indeed they be so). If you do reach such lofty heights of re-cognition, why not just program all of that into the DSL so that it corrects for all those mental lapses? Surely no more difficult than retooling the mind permanently. Plus you get to share the wealth: make it easy for others to reach programming nirvana too. (We're already there: it's that tarpit called Perl *smacks forehead*) The completed journey ends with a return to where one first began. Or something like that. mathematicians spend a lot of time thinking about how to think about things. G.C. Rota (RIP): The philosopher's role has always been that of stating facts that may have been on everybody's mind but that no one dared state clearly. -- View this message in context: http://old.nabble.com/Finally-tagless-and-abstract-relational-Algebra-tp26943949p26961194.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pointfree-trouble
Here's another way of writing it:
data Matrix a = Matr {unMatr :: [[a]]} | Scalar a deriving (Show, Eq)
-- RealFrac constraint removed
reMatr :: RealFrac a = ([[a]] - [[a]]) - (Matrix a - Matrix a)
reMatr f = Matr . f . unMatr -- this idiom occurs a lot, esp. with
newtypes
Affixing constraints to type constructors is typically deprecated.
slemi wrote:
i have trouble making a function pointfree:
data RealFrac a = Matrix a = Matr [[a]] | Scalar a
deriving (Show, Eq)
unMatr :: RealFrac a = Matrix a - [[a]]
unMatr = (\(Matr a) - a)
reMatr :: RealFrac a = ([[a]] - [[a]]) - (Matrix a - Matrix a)
reMatr a = Matr . (flip (.) unMatr) a
this works fine, but if i leave the 'a' in the last function's definition
like this:
reMatr = Matr . (flip (.) unMatr)
it gives an error. can anybody tell me why? (i'm using ghci)
--
View this message in context:
http://old.nabble.com/pointfree-trouble-tp26881661p26885392.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pointfree-trouble
There you have it: fully- and semi-pointfree versions of reMatr.
A heads up: aggressively pursuing pointfreeness without type signatures
guarantees a courtesy call from the monomorphism restriction,
pace ()-garlic aficionados.
As for your question on why the original code doesn't typecheck: if
you explain how you arrived at it, perhaps we can figure out where
you tripped up. Daniel Fischer for instance, *calculated* for you
the right answer. Habeas calculus and all that.
slemi wrote:
thanks, that's a really neat syntactic sugar :)
however, my original question was how to make the reMatr function
pointfree, as
reMatr = Matr . (flip (.) unMatr)
is not working. any ideas/explanation why it doesnt work?
Kim-Ee Yeoh wrote:
Here's another way of writing it:
data Matrix a = Matr {unMatr :: [[a]]} | Scalar a deriving (Show, Eq)
-- RealFrac constraint removed
reMatr :: RealFrac a = ([[a]] - [[a]]) - (Matrix a - Matrix a)
reMatr f = Matr . f . unMatr -- this idiom occurs a lot, esp. with
newtypes
Affixing constraints to type constructors is typically deprecated.
slemi wrote:
i have trouble making a function pointfree:
data RealFrac a = Matrix a = Matr [[a]] | Scalar a
deriving (Show, Eq)
unMatr :: RealFrac a = Matrix a - [[a]]
unMatr = (\(Matr a) - a)
reMatr :: RealFrac a = ([[a]] - [[a]]) - (Matrix a - Matrix a)
reMatr a = Matr . (flip (.) unMatr) a
this works fine, but if i leave the 'a' in the last function's
definition like this:
reMatr = Matr . (flip (.) unMatr)
it gives an error. can anybody tell me why? (i'm using ghci)
--
View this message in context:
http://old.nabble.com/pointfree-trouble-tp26881661p26897626.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is there a null statement that does nothing?
Hi Brent, Re: 'if expressions, not statements' is an elegant clarification, one definitely for the haskellwiki, if not there already. Just for completeness' sake, bottom is a value for any expression. Wouldn't making the else clause optional by defaulting to undefined worthy of consideration for Evil Haskell? -- Kim-Ee Brent Yorgey-2 wrote: On Wed, Oct 21, 2009 at 07:49:14PM -0500, Tim Wawrzynczak wrote: Yes, an if statement must have both 'then' and 'else' branches. As an example, what if you had let a = if b == 2 then True else False and you were missing an else branch? What would 'a' get assigned to? The if statement returns a value so must have both branches. By the way, it helps to be precise with language here: statement usually indicates an instruction which causes some effect to happen. Expression indicates something which evaluates to a value. Haskell doesn't have if statements but it does have if expressions. It makes sense for an if *statement* (in imperative languages like C) to have an optional else clause, since do nothing is a perfectly valid *statement*. But it doesn't make sense for an if *expression* to have a missing else, since it must evaluate to something and (in general) there is no null value that could be used. Of course, as others have noted, in a monadic context there IS a special null value, namely return (), which can be used to indicate do nothing. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- View this message in context: http://www.nabble.com/Is-there-a-null-statement-that-does-nothing--tp26002445p26081461.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ** for nested applicative functors?
Does anyone know if it's possible to write the following: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) Clearly, if m and n were monads, it would be trivial. Rereading the original paper, I didn't see much discussion about such nested app. functors. Any help appreciated. -- View this message in context: http://www.nabble.com/%3C**%3E-for-nested-applicative-functors--tp25858792p25858792.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ** for nested applicative functors?
That's it: liftA2 (*), so obvious in hindsight. Mustn't ... code ... when ... drained Thanks to Jeremy and Josef. Jeremy Shaw-3 wrote: This looks like what is described in Section 4 to me: http://www.haskell.org/haskellwiki/Applicative_functor#Applicative_transfomers - jeremy On Oct 12, 2009, at 11:22 AM, Kim-Ee Yeoh wrote: ** :: (Applicative m, Applicative n) = m (n (a-b)) - m (n a) - m (n b) -- View this message in context: http://www.nabble.com/%3C**%3E-for-nested-applicative-functors--tp25858792p25859274.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Essentials about type classes?
Hi Fredrik, Temaran wrote: data Dar = Dar String String deriving (Show, Eq) class Bar a where foo :: a - Int instance Bar Dar where foo(Dar n c) = length c but it keeps generating the same error; ERROR ./Bar.hs:16 - Inferred type is not general enough *** Expression: foo *** Expected type : a - Int *** Inferred type : Dar - Int You're missing indentation. Instead of declaring foo as a member of the typeclass, your code says it's a top-level function fully-polymorphic in the first parameter. That's why defining it later as foo (Dar ...) gives the error message it does. -- View this message in context: http://www.nabble.com/Essentials-about-type-classes--tp25393728p25405022.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] n00b question: defining datatype
Consider
data Task = Task { title :: String, completed :: Bool, subtasks :: Maybe
[Task] }
Iain Barnett wrote:
Hi,
I'm trying to get my head around datatypes, and wondering how I might
define
a simple Task datatype in Haskell.
data Task = Task { title :: String, completed :: Bool }
Ok, that's straightforward, but sometimes tasks become a list of tasks
themselves
data Task = Task { title :: String, completed :: Bool, subtasks :: [Task]
}
But that's not really right, because obviously, some tasks don't have
subtasks. So I try this:
data Task = Task { title :: String, completed :: Bool } | TaskWithSubtasks
{
title :: String, completed :: Bool, subtasks :: [Task] }
It's a bit more accurate, but it's repeating things, which is ok with a
simple type. Could anyone suggest a better way to define this? If I was
using C#, which I'm far more familiar with, I could overload the
constructor
and refer to the smaller constructor. Is there a way to do that in
Haskell,
or am I still thinking too OOP?
Iain
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
View this message in context:
http://www.nabble.com/n00b-question%3A-defining-datatype-tp24631976p24632019.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Flipping *-*-* kinds, or monadic finally-tagless madness
Kim-Ee Yeoh wrote: As for fixing the original bug, I've found that the real magic lies in the incantation (Y . unY) inserted at the appropriate places. Aka unsafeCoerce, changing the phantom type |a|. The type of (Y . unY) is (Y . unY) :: forall a b c. Y c a - Y c b so modulo (Y c), it is indeed unsafeCoerce. The need to do it is caused by wanting to erase the existential introduced by Za/MkZa. That's not the primary reason. The earlier version of the code in my original message doesn't use existentials. We still however, need to wobble the type via (Y . unY) in order to typecheck. Depending on what the phantom type is supposed to represent, this may or may not give the semantics/safety you're after. If you're referring to the safety of the object/target language, then even without any Symantics instances, only type-correct code can compile, thanks to the finally-tagless embedding that lifts type-checking in the meta-language (Haskell) into type-checking for the target language. That safety isn't in the least bit compromised. The pretty-printing Symantics instance in question actually type-checks fine without unsafeCoerce or its like when written out without the additional Monad type-class abstraction and Y-Z isomorphism. Translating to the latter was entirely straightforward. Thanks to all who responded. -- View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24439023.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Flipping *-*-* kinds, or monadic finally-tagless madness
Hi Edward,
Your runPretty version fits the bill nicely, thank you. I might still retain
the state monad version because it allows generalizations beyond
pretty-printing.
As for fixing the original bug, I've found that the real magic lies
in the incantation (Y . unY) inserted at the appropriate places. Indeed,
I've removed type signatures because try as I might, I couldn't
write something the type-checker would accept. This is for 6.8.2.
FWIW, the final version:
instance Symantics (Y String) where
int = unZ . return . show
bool = unZ . return . show
lam f = unZ $ do
show_c0 - get
let
vname = v ++ show_c0
c0 = read show_c0 :: VarCount
c1 = succ c0
put (show c1)
bodyf - (Z . Y . unY . f . unZ . return) vname
return $ (\\ ++ vname ++ - ++ bodyf ++ )
fix f= pr3 [MkZa $ lam f] [(fix , )]
app e1 e2= pr3 [MkZa e1,MkZa e2] [(,,)]
add e1 e2= pr3 [MkZa e1,MkZa e2] [(, + ,)]
mul e1 e2= pr3 [MkZa e1,MkZa e2] [(, * ,)]
leq e1 e2= pr3 [MkZa e1,MkZa e2] [(, = ,)]
if_ be et ee = pr3 [MkZa be,MkZa et,MkZa ee] [(if , then , else
,)]
-- Suppress the Symantics phantom type by casting to an existential
data Za where
MkZa :: Y String a - Za
pr3 a b = unZ $ pr2 a b
pr2 :: forall a. [Za] - [String] - Z a String
pr2 _ [] = return
pr2 [] ts = (return . concat) ts
pr2 ((MkZa e):es) (t:ts) = do
s1 - (Z . Y . unY) e -- that (Y . unY) magical
incantation again!
s2 - pr2 es ts
return $ t ++ s1 ++ s2
Edward Kmett wrote:
You might also look at doing it without all the State monad noise with
something like:
class Symantics repr where
int :: Int - repr Int
add :: repr Int - repr Int - repr Int
lam :: (repr a - repr b) - repr (a-b)
app :: repr (a - b) - repr a - repr b
newtype Pretty a = Pretty { runPretty :: [String] - String }
pretty :: Pretty a - String
pretty (Pretty f) = f vars where
vars = [ [i] | i - ['a'..'z']] ++ [i : show j | j - [1..], i -
['a'..'z'] ]
instance Symantics Pretty where
int = Pretty . const . show
add x y = Pretty $ \vars - ( ++ runPretty x vars ++ + ++
runPretty y vars ++ )
lam f = Pretty $ \ (v:vars) - (\\ ++ v ++ . ++ runPretty (f (var
v)) vars ++ ) where
var = Pretty . const
app f x = Pretty $ \vars - ( ++ runPretty f vars ++ ++
runPretty
x vars ++ )
--
View this message in context:
http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24326046.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Flipping *-*-* kinds, or monadic finally-tagless madness
I'm trying to write HOAS Show instances for the finally-tagless
type-classes using actual State monads.
The original code:
http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs
Two type variables are needed: one to vary over the Symantics
class (but only as a phantom type) and another to vary over the
Monad class. Hence, the use of 2-variable type constructors.
type VarCount = int
newtype Y b a = Y {unY :: VarCount - (b, VarCount)}
Not knowing of a type-level 'flip', I resort to newtype isomorphisms:
newtype Z a b = Z {unZ :: Y b a}
instance Monad (Z a) where
return x = Z $ Y $ \c - (x,c)
(Z (Y m)) = f = Z $ Y $ \c0 - let (x,c1) = m c0 in (unY . unZ) (f
x) c1-- Pace, too-strict puritans
instance MonadState String (Z a) where
get = Z $ Y $ \c - (show c, c)
put x = Z $ Y $ \_ - ((), read x)
So far so good. Now for the Symantics instances (abridged).
class Symantics repr where
int :: Int - repr Int -- int literal
add :: repr Int - repr Int - repr Int
lam :: (repr a - repr b) - repr (a-b)
instance Symantics (Y String) where
int = unZ . return . show
add x y = unZ $ do
sx - Z x
sy - Z y
return $ ( ++ sx ++ + ++ sy ++ )
The add function illustrates the kind of do-sugaring we know and love
that I want to use for Symantics.
lam f = unZ $ do
show_c0 - get
let
vname = v ++ show_c0
c0 = read show_c0 :: VarCount
c1 = succ c0
fz :: Z a String - Z b String
fz = Z . f . unZ
put (show c1)
s - (fz . return) vname
return $ (\\ ++ vname ++ - ++ s ++ )
Now with lam, I get this cryptic error message (under 6.8.2):
Occurs check: cannot construct the infinite type: b = a - b
When trying to generalise the type inferred for `lam'
Signature type: forall a1 b1.
(Y String a1 - Y String b1) - Y String (a1 -
b1)
Type to generalise: forall a1 b1.
(Y String a1 - Y String b1) - Y String (a1 -
b1)
In the instance declaration for `Symantics (Y String)'
Both the two types in the error message are identical, which suggests
no generalization is needed. I'm puzzled why ghc sees an infinite type.
Any ideas on how to proceed?
--
View this message in context:
http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagless-madness-tp24314553p24314553.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] shadowing keywords like otherwise
Hi Vasili,
This isn't really a shadowing/redefinition issue. Here's
a perfectly legitimate snippet that compiles fine:
f 0 = 0
f otherwise = 1+otherwise
Redefinition is when you have:
g = let otherwise = not in x
-- Kim-Ee
VasiliIGalchin wrote:
swishParse :: String - String - SwishStateIO (Maybe RDFGraph)
swishParse fnam inp =
do { fmt - gets $ format
; case fmt of
N3- swishParseN3 fnam inp
otherwise -
do { swishError (Unsupported file format: ++(show fmt))
4
; return Nothing
}
}
I am receiving a shadow warning:
Swish/HaskellRDF/SwishCommands.hs:304:12:
Warning: Defined but not used: `otherwise'
It seems to me that in the code base somewhere that there is a redefine
of
the keywordotherwise. I haven't read the Haskell 98 Report but I thought
that it was not possible to redefine keywords. ??
--
View this message in context:
http://www.nabble.com/%22shadowing%22-keywords-like-%22otherwise%22-tp24239153p24239430.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] shadowing keywords like otherwise
I meant, of course,
g = let otherwise = not in otherwise
Sorry for the noise.
-- Kim-Ee
Kim-Ee Yeoh wrote:
Hi Vasili,
This isn't really a shadowing/redefinition issue. Here's
a perfectly legitimate snippet that compiles fine:
f 0 = 0
f otherwise = 1+otherwise
Redefinition is when you have:
g = let otherwise = not in x
-- Kim-Ee
VasiliIGalchin wrote:
swishParse :: String - String - SwishStateIO (Maybe RDFGraph)
swishParse fnam inp =
do { fmt - gets $ format
; case fmt of
N3- swishParseN3 fnam inp
otherwise -
do { swishError (Unsupported file format: ++(show
fmt)) 4
; return Nothing
}
}
I am receiving a shadow warning:
Swish/HaskellRDF/SwishCommands.hs:304:12:
Warning: Defined but not used: `otherwise'
It seems to me that in the code base somewhere that there is a redefine
of
the keywordotherwise. I haven't read the Haskell 98 Report but I
thought
that it was not possible to redefine keywords. ??
--
View this message in context:
http://www.nabble.com/%22shadowing%22-keywords-like-%22otherwise%22-tp24239153p24239439.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] shadowing keywords like otherwise
Whoops, you're right. Interestingly, the shadowing warnings vary between the 2 examples I gave, i.e. shadowing within 'function definition' vs 'binding group'. Felipe Lessa wrote: On Sun, Jun 28, 2009 at 12:49:12AM -0700, Kim-Ee Yeoh wrote: This isn't really a shadowing/redefinition issue. Here's a perfectly legitimate snippet that compiles fine: f 0 = 0 f otherwise = 1+otherwise What? It is a redefinition issue *as well*, but this kind of warning isn't active by default Prelude :s -Wall Prelude let f 0 = 0; f otherwise = 1 + otherwise interactive:1:15: Warning: This binding for `otherwise' shadows the existing binding imported from Prelude In the definition of `f' -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- View this message in context: http://www.nabble.com/%22shadowing%22-keywords-like-%22otherwise%22-tp24239153p24244760.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What is an expected type ...
Could you suggest a better word pair to describe the dichotomy then? How about 'calculated' vs 'user-imposed' (or even, 'explicitly- signatured')? Dan Piponi-2 wrote: I really dislike this error message, and I think the terms are ambiguous. I think the words 'expected' and 'inferred' apply equally well to the term, and the context in which it has been found. Both of the incompatible types were 'inferred', and 'unexpected' is a property of the combination, not a property of one or the other. -- Dan On Sun, Jun 28, 2009 at 8:24 AM, Martijn van Steenbergenmart...@van.steenbergen.nl wrote: Hi Michael, michael rice wrote: as opposed to an inferred type? Can you deduce from the following example? Prelude let foo = () :: Int interactive:1:10: Couldn't match expected type `Int' against inferred type `()' In the expression: () :: Int In the definition of `foo': foo = () :: Int Hope this helps! Martijn. ___ 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 -- View this message in context: http://www.nabble.com/What-is-an-%22expected-type%22-...-tp24242359p24244820.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functor and Haskell
Daryoush Mehrtash-2 wrote: I am not sure I follow how the endofunctor gave me the 2nd functor. As I read the transformation there are two catagories C and D and two functors F and G between the same two catagories. My problem is that I only have one functor between the Hask and List catagories. So where does the 2nd functor come into picture that also maps between the same C and D catagories? Consider singleton :: a - [a] singleton x = [x] Here F is the identity functor, and G is the list functor. And yes, C=D= category of (a subset of) Haskell types. -- View this message in context: http://www.nabble.com/Functor-and-Haskell-tp23166441p23170956.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functor and Haskell
Daryoush Mehrtash-2 wrote: singleton :: a - [a] singleton x = [x] Here F is the identity functor, and G is the list functor. And yes, C=D= category of (a subset of) Haskell types. Are you saying the function that goes from list functor to singleton funtor is a natural transformation? Here *singleton* is the natural transformation from the identity functor to the list functor. Daryoush Mehrtash-2 wrote: But aren't they functors to different subset of Haskell Types? They're usually treated as endofunctors on Hask, for reasons Ross Paterson has given. -- View this message in context: http://www.nabble.com/Functor-and-Haskell-tp23166441p23189784.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Heinrich Apfelmus wrote: Now, (forall a. T[a]) - S is clearly true while exists a. (T[a] - S) should be nonsense: having one example of a marble that is either red or blue does in no way imply that all of them are, at least constructively. (It is true classically, but I forgot the name of the corresponding theorem.) For the record, allow me to redress my earlier erroneous assertion by furnishing the proof for the classical case: (forall a. T(a)) - S = not (forall a. T(a)) or S, by defn of implication = not $ (forall a. T(a)) and (not S), by de Morgan's = not $ forall a. T(a) and (not S), product rule??? = exists a. not (T(a)) or S, de Morgan's again = exists a. T(a) - S, by defn of implication The only wrinkle is obviously in the logical and of (not S) distributing under the universal quantifier. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22208626.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Wolfgang Jeltsch-2 wrote: Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch: First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) - T' is equivalent to the type exists a. (T[a] - T'). It’s the same as in predicate logic – Curry-Howard in action. Oops, this is probably not true. The statement holds for classical predicate logic with only non-empty domains. Here's a counterexample, regardless of whether you're using constructive or classical logic, that (forall a. T[a]) - T' does not imply exists a. (T[a] - T'). Let a not exist, but T' true. Done. My apologies for not catching this earlier. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22126043.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Jonathan Cast-2 wrote: Summary: Existential types are not enough for ST. You need the rank 2 type, to guarantee that *each* application of runST may (potentially) work with a different class of references. (A different state thread). Interesting. What's going on in the example that you posted seems to be a stronger but still familiar version of there exists, namely there exists exactly one a.k.a. there uniquely exists, often represented with exists-bang: exists!. The problem is that given [1] exists! a. (U[a] -V) we can constructively derive [2] (forall a. U[a]) - V even though the program/proof of [2] derived from [1] is deficient as you've explained. In Haskell, the only existential quantification is exists-bang. The weaker form of existence is sufficient to regain thread safety for runST. Every application of a program of type (exists-w/o-bang a. U[a]) simply cannot assume that the (a) is always the same. What would be a suitable logic for framing these kinds of analyses I wonder? -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22099322.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
There's a lot to chew on (thank you!), but I'll just take something I can handle for now. Dan Doel wrote: An existential: exists a:T. P(a) is a pair of some a with type T and a proof that a satisfies P (which has type P(a)). In Haskell, T is some kind, and P(a) is some type making use of a. That doesn't mean that there is only one a:T for which P is satisfied. But it *does* mean that for any particular proof of exists a:T. P(a), only one a:T is involved. So if you can open that proof, then you know that that is the particular a you're dealing with, which leads to the problems in the grandparent. re: Constructivity and the opening of a proof A form of the theorem that the primes are infinite goes Given a finite set of primes, there's a prime bigger than any of them. The usual proof is constructive since factorization is algorithmic, but I don't see why a priori, applications of this theorem on a given input should always yield the same prime when more than one factor exists. Is non-deterministic choice forbidden in constructive math? A cursory google seems to suggest that if not, it's at least a bête noire to some. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22100873.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Jonathan Cast-2 wrote: Taking the `let open' syntax from `First-class Modules for Haskell' [1], we can say let open runST' = runST in let ref = runST' $ newSTRef 0 !() = runST' $ writeSTRef ref 1 !() = runST' $ writeSTRef ref 2 in runST' $ readSTRef ref This type-checks because the let open gives us the *same* skolemized constant for s everywhere in the sequel. One answer, of course, is to lift the skolem type-constant into a kind of IO-like type-monad. Sort of like getLine :: IO String, which is still constant in a way, since the program doesn't vary. You'd then want kind-level functions like returnK :: * - M * and the rest. It would be interesting to see this made explicit in System F. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22106898.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Peter Verswyvelen-2 wrote: I'm having trouble understanding the explanation of the meaning of the signature of runST at http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types I could try to read the article a couple of times again, but are there any other good readings about these existentially quantified types and how the ST monad works? Existential quantification can be discussed without reference to runST, and the more I reread the wikibooks link you gave, the more I'm convinced the runST section doesn't belong there. The tenuous connection between them is higher-ranked types. You can't do much with existential quantification without invoking them. That one presupposes the other does not necessitate its converse. Despite its rank-2 type, runST really doesn't have anything to do with e.q. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22042542.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Correct. And under the hood, GHC does implement runST in its existential dual form using a hidden State# type. I wonder however, if we're wandering too far away from the OP's query about grokking runST and how the ST monad works. I'd imagine that means he'd like to see how rank-2 polymorphism keeps different threads separated, something which doesn't require existentials, much less the perforce crippled (because constructivist) duality between the two flavors of quantification. Wolfgang Jeltsch-2 wrote: Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch: Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh: Despite its rank-2 type, runST really doesn't have anything to do with existential quantification. First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) - T' is equivalent to the type exists a. (T[a] - T'). It’s the same as in predicate logic – Curry-Howard in action. Oops, this is probably not true. The statement holds for classical predicate logic with only non-empty domains. But in constructivist logic only the first of the above statements follows from the second, not the other way round. So arguing with the Curry-Howard isomorphism fails and indeed, the two types are not equivalent. There is just a function from the second to the first (it’s the function application function ($) actually). -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22044960.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Peter Verswyvelen-2 wrote: I could try to read the article a couple of times again, but are there any other good readings about these existentially quantified types and how the ST monad works? The primary source is if I'm not mistaken, the following State in Haskell paper: http://research.microsoft.com/en-us/um/people/simonpj/Papers/state-lasc.ps.gz Having said that, I'm not sure about the statement on page 9 that readVar v simply does not have type forall s. ST s Bool. The variable v could be of type forall s. MutVar s Bool, in which case all of runST (readVar v) typechecks. The sticking point really arises from runST (newVar True). So there isn't really the other way round, but rather only one way. Am I misreading something? A minor nit, to be sure. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22026629.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Looking for pointfree version
import Control.Applicative data Pair a = a :*: a instance Functor Pair where f `fmap` (x :*: y) = f x :*: f y instance Applicative Pair where (f :*: g) * (x :*: y) = f x :*: f y The last f needs to be a g. pure x = x :*: x pointfree :: (a - b - c) - Pair a - Pair b - Pair c --pointfree o x y = pure o * x * y pointfree = ((*) .) . (*) . pure -- in the applicative paper notation: --pointfree o x y = [| o x y |] Very nice. Aside: I wonder how much work it would be to extend the pointfree tool to infer such equalities? -- View this message in context: http://www.nabble.com/Looking-for-pointfree-version-tp21913653p22027350.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Looking for pointfree version
On the same note, does anyone have ideas for the following snippet? Tried the pointfree package but the output was useless. pointwise op (x0,y0) (x1,y1) = (x0 `op` x1, y0 `op` y1) Edsko de Vries wrote: Perfect! Beautiful. I was hoping there'd be a simple solution like that. Thanks! On 9 Feb 2009, at 14:31, Wouter Swierstra wrote: How about using Data.Monoid: down = downPar `mappend` downNew `mappend` downTrans -- View this message in context: http://www.nabble.com/Looking-for-pointfree-version-tp21913653p21971304.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Problems with strictness analysis?
Luke Palmer-2 wrote: I would like to know or to develop a way to allow abstract analysis of time and space complexity. In the same way that type inference and strictness analysis can be seen as instances of abstract interpretation, so can complexity inference. I agree that the interplay between these various instances of AI is an unexplored lode for us cogheads. Below are 2 references to complexity inference. I have yet to look closely to ascertain the degree of compositionality of their methodologies. Can anyone recommend a survey paper of the entire field? Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time Amir M. Ben-Amram, Neil D. Jones and Lars Kristiansen http://dx.doi.org/10.1017/S095679683865 Automated complexity analysis of Nuprl extracted programs Ralph Benzinger http://dx.doi.org/10.1007/978-3-540-69407-6_7 -- View this message in context: http://www.nabble.com/Problems-with-strictness-analysis--tp20301967p2034.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Problems with strictness analysis?
David Menendez-2 wrote: On Mon, 3 Nov 2008, Luke Palmer wrote: I was actually being an annoying purist. f is strict means f _|_ = _|_, so strictness is a semantic idea, not an operational one. I think Luke was commenting on the terminology, not the optimization. We have a tendency to say lazy when we mean non-strict and strict when we mean eager. Good point. If it sheds light on such elusive, important distinctions then this incorrigible pedantry can only be encouraged. -- View this message in context: http://www.nabble.com/Problems-with-strictness-analysis--tp20301967p20319740.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object-oriented programming, Haskell and existentials
re: the importance of existential-cleansing On the one hand, it's easy to concur that existentials are simpler than the alternatives, the tortuous elimination of CC Shan's translucent existential being a case in point. And it's also easy to dismiss such caprice as a penchant for Houdinian escape perversities. Then again, why not? There may never be a real need for anything particular at all, existentials notwithstanding. Affirming that by cracking open the shackles of icons and diabolical shibboleths is arguably the only real need. Lennart Augustsson wrote: What do you mean by need? From a theoretical or practical perspective? We don't need them from a theoretical perspective, but in practice I'd rather use existentials than encodinging them in some tricky way. On Wed, Oct 15, 2008 at 11:05 AM, [EMAIL PROTECTED] wrote: The web page begs a question if there is ever any real need for existentials. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- View this message in context: http://www.nabble.com/Object-oriented-programming%2C-Haskell-and-existentials-tp19990499p20007420.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy vs correct IO [Was: A round of golf]
oleg-30 wrote: I have not expected to see this Lazy IO code. After all, what could be more against the spirit of Haskell than a `pure' function with observable side effects. What could even be more against the spirit of Haskell than the original theme of this thread, i.e. code that makes us cry? Lennart's piece fudges purity, agreed, but it reads nicely as idiomatic Haskell, swift on the eyes if not on the machine. Consider if readFile's semantics were modified, i.e. not lazy, at least not always. In the ideal world, a smart enough compiler would just do the right thing, i.e. the IO String returned would be strict, or better yet, it would automatically chunkify the read to obtain constant space usage. Lazy IO is indeed a nasty can of worms, not unrelated to the issue of monadic IO as a gigantic sin bin. We could avoid it entirely, or we could sort out and algebraize the different interactions into a happier marriage of the pair. -- View this message in context: http://www.nabble.com/Lazy-vs-correct-IO--Was%3A-A-round-of-golf--tp19567128p19573538.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] More on performance
Jon Harrop wrote: On Wednesday 04 June 2008 11:05:52 Luke Palmer wrote: Given unbounded time and space, you will still arrive at the same result regardless of the complexity. Given that the set of computers with unbounded time and space is empty, is it not fruitless to discuss its properties? The set of omnipotent people is also empty. That has not stopped homo sapiens from discussing /its/ properties. All history is ever only such a discussion for nothing fires up the imagination nor provokes acts of brilliant foolhardiness like the unattainable. -- Kim-Ee -- View this message in context: http://www.nabble.com/More-on-performance-tp17629453p17676772.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
Roberto Zunino-2 wrote: Alas, for code like yours: foo = \f - (f 'J', f True) there are infinite valid types too: (forall a. a - Int) - (Int, Int) (forall a. a - Char)- (Char, Char) (forall a. a - (a,a)) - ((Char,Char),(Bool,Bool)) ... and it is much less clear if a best, most general type exists at all. How about foo :: (exists. m :: * - *. forall a. a - m a) - (m Char, m Bool) Not quite Haskell, but seems to cover all of the examples you gave. -- Kim-Ee -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17531238.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
Luke Palmer-2 wrote: You have now introduced a first-class type function a la dependent types, which I believe makes the type system turing complete. This does not help the decidability of inference :-) God does not care about our computational difficulties. He infers types emp^H^H^H ... uh, as He pleases. Anyway, the original point of it was semantic. Let's first explore the meaning of the most general type. Type functions give one answer, intersection types another. -- Kim-Ee (yeoh at cs dot wisc dot edu) -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17534701.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
Andrew Coppin wrote: So, after an entire day of boggling my mind over this, I have brought it down to one simple example: (id 'J', id True) -- Works perfectly. \f - (f 'J', f True) -- Fails miserably. Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker. So what is the type of that second expression? You would think that (x - x) - (Char, Bool) as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all! In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble. Let's fill in the type variable: (x - x) - (Char, Bool) == forall x. (x - x) - (Char, Bool) == x_t - (x - x) - (Char, Bool), where x_t is the hidden type-variable, not unlike the reader monad. As you've pointed out, callER chooses x_t, say Int when passing in (+1) :: Int - Int, which obviously would break \f - (f 'J', f True). What we want is the callEE to choose x_t since callEE needs to instantiate x_t to Char and Bool. What we want is (x_t - x - x) - (Char, Bool). But that's just (forall x. x - x) - (Char, Bool). For completeness' sake, let me just state that if universal quantification is like (x_t - ...), then existential quantification is like (x_t, ...). Andrew Coppin wrote: At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory. My sympathies. You may find the haskell-cafe archive to be as useful as I have (search Ben Rudiak-Gould or Dan Licata). Having said that, I think you've done pretty well on your own. Andrew Coppin wrote: - Why can't the type system automatically detect where polymorphism is required? - Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned? Well, give it a try! I'm sure I'm not the only one interested in your type inference experiments. Warning: they're addictive and may lead to advanced degrees and other undesirable side-effects. -- Kim-Ee -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17498362.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Short circuiting and the Maybe monad
Dan Piponi-2 wrote: In fact, you can use the Reader monad as a fixed size container monad. Interesting that you say that. Reader seems to me more as an anti-container monad. -- View this message in context: http://www.nabble.com/Short-circuiting-and-the-Maybe-monad-tp17200772p17288351.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Couple of formal questions
I'm not sure there's a proof as such, more like a definitional absence of distinction between initiality and finality. In other words, the CPO framework is orthogonal to such extremality considerations. Perhaps someone here knows about work enriching CPOs in that direction. -- Kim-Ee Michael Karcher-7 wrote: Wouter Swierstra [EMAIL PROTECTED] wrote: Hi Creighton, Where could I find a proof that the initial algebras final coalgebras of CPO coincide? I saw this referenced in the Bananas.. paper as a fact, but am not sure where this comes from. Probably he was referring to the last paragraph of the introduction: Working in CPO has the advantage that the carriers of intial algebras and final co-algebras coincide, thus there is a single data type that comprises both finite and infinite elements. -- View this message in context: http://www.nabble.com/Couple-of-formal-questions-tp16974927p17020475.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Wrong Answer Computing Graph Dominators
Dan Weston wrote: f . and == and . map f where f = (not x ||) If and is defined with foldr, then the above can be proven for all well-typed f, and for f = (not x ||) in particular, even if ys is null. The law is painlessly extended to cover the null case automatically (and is therefore consistent): LHS: not x || (and []) == not x || True == True RHS: and (map (not x ||) []) == and [] == True Therefore True |- True, an instance of x |- x If (and [] == False), then the law becomes inconsistent: -- snipped -- Yes, the natural way of defining and [] is, well, natural in more than one sense of the word. I initially had a hard time grasping what you meant with the 3 equations that started this discussion. I was sure you meant something other than what I thought, but I couldn't work it out. I'm glad Matt Brecknell came to the rescue. Before I would've merely relied on a monoidal identity argument like the one Chris had presented. Appealing to uniformity (a la parametric polymorphism) definitely looks sexier. All the cool kids seem to be doing it. -- View this message in context: http://www.nabble.com/Wrong-Answer-Computing-Graph-Dominators-tp16714477p16786100.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Wrong Answer Computing Graph Dominators
Dan Weston wrote: Here, any path means all paths, a logical conjunction: and [True, True] = True and [True ] = True and [ ] = True Hate to nitpick, but what appears to be some kind of a limit in the opposite direction is a curious way of arguing that: and [] = True. Surely one can also write and [False, False] = False and [False ] = False and [ ] = False ??? -- Kim-Ee -- View this message in context: http://www.nabble.com/Wrong-Answer-Computing-Graph-Dominators-tp16714477p16760156.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional programmer's intuition for adjunctions?
ajb-2 wrote: In Haskell, natural transformations are functions that respect the structure of functors. Since you can't avoid respecting the structure of functors (the language won't let you do otherwise), you get natural transformations for free. (Free as in theorems, not free as in beer.) It's worth noting that polymorphism is one of those unavoidable, albeit hidden, functors. Polymorphizing a function forall a can be thought of as lifting it via the ((-) T_a) functor, where T_a is the type variable of a. E.g. reverse really has the signature T_a - [a] - [a]. But ((-) T_a) is left adjoint to ((,) T_a), which just happens to be the analogous type-explicit way of representing existentials. Adjunctions are a useful tool to describe and analyze such dualities precisely. ajb-2 wrote: Adjunctions, on the other hand, you have to make yourself. As such, they're more like monads. Constructing adjunctions, comprising as they do of a pair of functors, does seem double the work of a single monad. Duality OTOH is a powerful guiding principle and may well be easier than working with the monad laws directly. And besides, you get a comonad for free. ajb-2 wrote: One thing that springs to mind is that an adjunction could connect monads and their associated comonads. Is that a good picture? Definitely. -- View this message in context: http://www.nabble.com/Functional-programmer%27s-intuition-for-adjunctions--tp15832225p15866753.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Graphical graph reduction
dainichi wrote: Now to the point: Wouldn't it be great if I had a visual tool that visually showed me the graph while the above evaluation unfolded? I could use it to show some of my co-workers to whom laziness is a mystery, what it's all about. Check out http://thyer.name/lambda-animator/. Requires Java. Explores several forms of laziness and them some. -- View this message in context: http://www.nabble.com/Graphical-graph-reduction-tp15637156p15649433.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Elevator pitch for Haskell.
Devin Mullins wrote: As for the latter, the reason I hear most often is I want to be able to use the language at my job.* -- snip -- * This is somewhat odd, as the strong majority of vocal Rubyists /are/ using it at their job. Not without risk though. Their necks get wrung if things break, an ordinary case of No one got fired for using insert name brand here/. Price tags of industry best practice technologies have sizable, hidden insurance components. Devin Mullins wrote: Perhaps they're preparing for the condition that they lose their job and have to take one up at a Fortune 500 or something. -- View this message in context: http://www.nabble.com/Elevator-pitch-for-Haskell.-tf4380572.html#a12605053 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
