Re: [Haskell-cafe] Lazy lists simulated by unboxed mutable arrays
Hello Henning, Wednesday, May 28, 2008, 9:51:28 AM, you wrote: >We could simulate a list with strict elements, i.e. > data StrictList a = Elem !a (StrictList a) | End > by an unboxed array with a cursor to the next element to be evaluated and > a function that generates the next element. Whenever an element with an > index beyond the cursor is requested, sufficiently many new elements are > written to the array and the cursor is advanced. This would still allow > the nice tricks for recursive Fibonacci sequence definition. This will > obviously save memory, but can we also expect that it is noticeably faster > than (StrictList a) ? looks like lazy.bytestring generalized to any a -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] re: a build problem
Hi Duncan, In response to your below, I am running "runhaskell Setup.hs configure -v3 --prefix=$HOME". Is v3 the current highest Cabal highest verbosity level? FYI basically I am running ghc that I just built a couple of days ago from the ghc source distribution. Vasili (I. Galchin) ;^) On Tue, 2008-05-27 at 15:33 -0700, Thomas Hartman wrote: > I think dist gets populated when you do build. Actually we also stash the configuration in ./dist/setup-config so that gets created at configure time. Galchin's problem is that something goes wrong during the configure and so nothing gets created in dist. From the log it looks like ghc or ld are failing during one of the early tests we do when configuring ghc. To make debugging this kind of thing a bit less mysterious in future Cabal now logs in greater detail what happens when it calls external programs (when invoked at the highest verbosity level). Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] So how do people pronounce 'cabal' around here?
Not always. Just to be sure, I just checked the "Longman Dictionary of Contemporary English Online" (http://pewebdic2.cw.idm.fr/topbar.html), and it came up with the following pronunciation for "cabal": \kəˈbæl\ In fact, this was the only pronunciation listed, so the other pronunciation is not listed at all. Here, the "æ" phoneme is identical to the same phoneme in "balance" (http://pewebdic2.cw.idm.fr/display/display.html?unfolded=3542&ids=3542,3543,3549,3544,3545,3546,3547,3548,3551,3679,29605,44549,47636,48407): \ˈbæləns\ If you don't say it that way, you get kicked out of the Longman cabal. Further, I asked two professional translators/interpreters at work, and they both said that either pronunciation was correct. Which cabal did you mean? Benjamin L. Russell --- On Wed, 5/28/08, Clifford Beshers <[EMAIL PROTECTED]> wrote: > From: Clifford Beshers <[EMAIL PROTECTED]> > Subject: Re: [Haskell-cafe] So how do people pronounce 'cabal' around here? > To: haskell-cafe@haskell.org > Date: Wednesday, May 28, 2008, 2:30 PM > On Tue, May 27, 2008 at 10:27 PM, Benjamin L. Russell < > [EMAIL PROTECTED]> wrote: > > > Actually, according to the definition that you used ( > > http://www.merriam-webster.com/dictionary/cabal), > there are the following > > two pronunciations of "cabal": > > > > 1) \kə-ˈbäl\ > > 2) \kə-ˈbal\ > > > > The "a" phoneme of the "ˈbal" > syllable of pronunciation 2 is actually > > defined to be identical to the first syllable > "ˈba" of "balance" ( > > http://www.merriam-webster.com/dictionary/balance); > viz.: > > > > \ˈba-lən(t)s\ > > > But if you say it that way, you get kicked out of the > cabal.___ > 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] Lazy lists simulated by unboxed mutable arrays
I wonder whether the following idea has been investigated or implemented somewhere: We could simulate a list with strict elements, i.e. data StrictList a = Elem !a (StrictList a) | End by an unboxed array with a cursor to the next element to be evaluated and a function that generates the next element. Whenever an element with an index beyond the cursor is requested, sufficiently many new elements are written to the array and the cursor is advanced. This would still allow the nice tricks for recursive Fibonacci sequence definition. This will obviously save memory, but can we also expect that it is noticeably faster than (StrictList a) ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] So how do people pronounce 'cabal' around here?
On Tue, May 27, 2008 at 10:27 PM, Benjamin L. Russell < [EMAIL PROTECTED]> wrote: > Actually, according to the definition that you used ( > http://www.merriam-webster.com/dictionary/cabal), there are the following > two pronunciations of "cabal": > > 1) \kə-ˈbäl\ > 2) \kə-ˈbal\ > > The "a" phoneme of the "ˈbal" syllable of pronunciation 2 is actually > defined to be identical to the first syllable "ˈba" of "balance" ( > http://www.merriam-webster.com/dictionary/balance); viz.: > > \ˈba-lən(t)s\ But if you say it that way, you get kicked out of the cabal. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Andrew Coppin <[EMAIL PROTECTED]> writes: > 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) A bit late in the fray, but have you considered this simpler expression: \f -> f 'J' I think you'll agree this does not have type (x->x) -> Char but rather (Char -> a) -> a right? Yet you can use 'id' as an argument (for f), since it has type forall a . a -> a where you are free to substitute Char for a and get (Char -> Char). An expression like: \f -> (f 'J', f True) requires an f that is both (Char -> a) and (Bool -> a) *at the same time*. A type like (a -> a) -> (Char,Bool) means that the expression is polymorphic in its argument, but here you need to specify that the function argument must be polymorphic itself. E.g. (forall a. a -> a) -> (Char,Bool). (Disclaimer: I hope I got it right :-) -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: the Network.URI parser
I am taking comments on a web forum from arbitrary people. The interpretation of the HTML occurs at the user's browser. A lot of people will be using outdated browsers (IE 5.5 / 6), ergo security (at the source) becomes my problem. I cannot force them to upgrade their browsers. I think this is very wrong for two reasons. First of all, the more web sites care of old browsers, the later people will upgrade them, therefore preventing the progress in Web (though IE 5.5 is not THAT old and bad, so this argument is not so strong). In Russia we some times say that a user with an outdated browser is an EPTH (Evil Pinocchio To Himself, don't ask me about source of this term). Secondly, I don't think that filtering HTML coming from an arbitrary user is a good idea. HTML is not very human-readable and too complex to achieve real safety without lots of work. My suggestion is to use some home-grown wiki-like syntax - it's easier to enter (*bold* instead of bold), easier to read (and your users would sometimes read their comments before posting - to check correctness), and easier to process, since it can't have security holes you're not aware of. But you're right, we are off topic. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] So how do people pronounce 'cabal' around here?
Actually, according to the definition that you used (http://www.merriam-webster.com/dictionary/cabal), there are the following two pronunciations of "cabal": 1) \kə-ˈbäl\ 2) \kə-ˈbal\ The "a" phoneme of the "ˈbal" syllable of pronunciation 2 is actually defined to be identical to the first syllable "ˈba" of "balance" (http://www.merriam-webster.com/dictionary/balance); viz.: \ˈba-lən(t)s\ Further, the second syllable of "robot" (http://www.merriam-webster.com/dictionary/robot) in fact does contain the same alternative phoneme "ä" as in pronunciation 1 of "cabal" above; viz.: \ˈrō-ˌbät\ To sum: The phoneme represented by the letter "a" in the second syllable of "cabal" is either pronounced like the phoneme "a" represented by the same letter in the first syllable "ˈba" of "balance" (for pronunciation 2), or like the phoneme "ä" represented by the letter "o" in the second syllable "ˌbät" of "robot." Further, as Clifford Beshers has already mentioned, the second syllable of "cabal" is the one stressed. Benjamin L. Russell --- On Wed, 5/28/08, Clifford Beshers <[EMAIL PROTECTED]> wrote: > As in the dictionary > (http://www.merriam-webster.com/dictionary/cabal), > accent on the second syllable, which is pronounced like > none of ball, > balance, boll and bale. Roughly the same rhythm as kaboom. > > On Tue, May 27, 2008 at 6:04 PM, Dan Piponi > <[EMAIL PROTECTED]> wrote: > > > In particular, which syllable gets the stress, and > what are the > > lengths of the two vowels? Couldn't find anything > in the FAQ > > (http://www.haskell.org/haskellwiki/Cabal/FAQ). > > -- > > Dan > > ___ > > Haskell-Cafe mailing list > > Haskell-Cafe@haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > >___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: the Network.URI parser
On 27/05/2008, at 6:08 PM, Neil Mitchell wrote: It most certainly is a security flaw. In the src of an img, yes, probably. In the href of a link, its a completely valid thing to do - and one that I've done loads of times. The URI is fine, its just the particular location that is dodgy. Sure, but for other reasons (potential inaccessibility) I am quite happy to ban JavaScript from URIs. (Not all URIs, just the ones coming from untrusted users.) whole pile of dodgy URIs. Most get culled (in my case) by the HaXml parser and/or XHTML 1.0 Strict validation, and now I hope to eliminate the rest by carefully handling the URIs. I don't think that's possible. A URI can validly have javascript, and can validly be a lot of things which are unsafe. Sure, I now realise my notion of allowable URI goes beyond (is an additional restriction of) the RFC. One way to show the URI is valid is to fetch what it is pointing to, and ensure it is an image or whatever. On that topic, does anyone have any good advice for handling these things? My advice is that you are targeting security at the wrong level. You shouldn't be cleaning the HTML to get a secure page, you should be having the level that interprets the HTML be secure regardless of the input. I am taking comments on a web forum from arbitrary people. The interpretation of the HTML occurs at the user's browser. A lot of people will be using outdated browsers (IE 5.5 / 6), ergo security (at the source) becomes my problem. I cannot force them to upgrade their browsers. If anyone knows of the state-of-the-art in this area, I'd appreciate a pointer. http://htmlpurifier.org/live/smoketests/printDefinition.php doesn't seem to think the style attribute is unsafe. Have they not been following the MySpace fiascos? Safety is a property of the HTML viewer, not of the HTML or CSS. Well, yes and no. I am heavily restricting the XHTML I accept (e.g. no scripts, no style attribute, ...), in an attempt to keep things visually accessible and avoid phishing attacks. I was alluding to the use of absolute positioning in CSS. If I had a CSS parser I might allow the style attribute. Safety for me involves making sure that what is displayed is trustworthy and easily identifiable as such. This is not something the HTML viewer can always help with. I think we're off-topic enough for me to stop here. Thanks for your comments. cheers peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] So how do people pronounce 'cabal' around here?
As in the dictionary (http://www.merriam-webster.com/dictionary/cabal), accent on the second syllable, which is pronounced like none of ball, balance, boll and bale. Roughly the same rhythm as kaboom. On Tue, May 27, 2008 at 6:04 PM, Dan Piponi <[EMAIL PROTECTED]> wrote: > In particular, which syllable gets the stress, and what are the > lengths of the two vowels? Couldn't find anything in the FAQ > (http://www.haskell.org/haskellwiki/Cabal/FAQ). > -- > Dan > ___ > 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] So how do people pronounce 'cabal' around here?
In particular, which syllable gets the stress, and what are the lengths of the two vowels? Couldn't find anything in the FAQ (http://www.haskell.org/haskellwiki/Cabal/FAQ). -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
On Tue, May 27, 2008 at 5:55 PM, Andrew Coppin <[EMAIL PROTECTED]> wrote: > Gleb Alexeyev wrote: >> >> foo :: (forall a . a -> a) -> (Bool, String) >> foo g = (g True, g "bzzt") > > 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) When you're reasoning about this, I think it would help you greatly to explicitly put in *all* the foralls. In haskell, when you write, say: map :: (a -> b) -> [a] -> [b] All the free variables are *implicitly* quantified at the top level. That is, when you write the above, the compiler sees: map :: forall a b. (a -> b) -> [a] -> [b] (forall has low precedence, so this is the same as: map :: forall a b. ((a -> b) -> [a] -> [b]) ) And the type you mention above for the strange expression is: forall x. (x -> x) -> (Char, Bool) Which indicates that the caller gets to choose. That is, if a caller sees a 'forall' at the top level, it is allowed to instantiate it with whatever type it likes. Whereas the type you want has the forall in a different place than the implicit quantifiaction: (forall x. x -> x) -> (Char, Bool) Here the caller does not have a forall at the top level, it is hidden inside a function type so the caller cannot instantiate the type. However, when implementing this function, the argument will now have type forall x. x -> x And the implementation can instantiate x to be whatever type it likes. But my strongest advice is, when you're thinking through this, remember that: x -> x Is not by itself a type, because x is meaningless. Instead it is Haskell shorthand for forall x. x -> x Luke > 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. > > Interestingly, if you throw in the undocumented "forall" keyword, everything > magically works: > > (forall x. x -> x) -> (Char, Bool) > > Obviously, the syntax is fairly untidy. And the program is now not valid > Haskell according to the written standard. And best of all, the compiler > seems unable to deduce this type automatically either. > > 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. So far, the only really plausible theory I have been > able to come up with is this: > > - A function starts out with a polymorphic type, such as 'x -> x'. > > - Each time the function is called, all the type variables have to be locked > down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or > something. > > - By the above, any function passed to a high-order function has to have all > its type variables locked down, yielding a completely monomorphic function. > > - In the exotic case above, we specifically WANT a polymorphic function, > hence the problem. > > - The "forall" hack somehow convinces the type checker to not lock down some > of the type variables. In this way, the type variables relating to a > function can remain unlocked until we reach each of the call sites. This > allows the variables to be locked to different types at each site [exactly > as they would be if the function were top-level rather than an argument]. > > This is a plausible hypothesis for what this language feature actually does. > [It is of course frustrating that I have to hypothesise rather than read a > definition.] However, this still leaves a large number of questions > unanswered... > > - Why are top-level variables and function arguments treated differently by > the type system? > - Why do I have to manually tell the type checker something that should be > self-evident? > - Why do all type variables need to be locked down at each call site in the > first place? > - Why is this virtually never a problem in real Haskell programs? > - Is there ever a situation where the unhacked type system behaviour is > actually desirably? > - 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? > > > > Unfortunately, the GHC manual doesn't have a lot to say on the matter
Re: [Haskell-cafe] a build problem ....
On Tue, 2008-05-27 at 15:33 -0700, Thomas Hartman wrote: > I think dist gets populated when you do build. Actually we also stash the configuration in ./dist/setup-config so that gets created at configure time. Galchin's problem is that something goes wrong during the configure and so nothing gets created in dist. From the log it looks like ghc or ld are failing during one of the early tests we do when configuring ghc. To make debugging this kind of thing a bit less mysterious in future Cabal now logs in greater detail what happens when it calls external programs (when invoked at the highest verbosity level). Duncan > > > > 2008/5/27 Galchin, Vasili <[EMAIL PROTECTED]>: > >> when I do a "clean" followed by "configure" then dist is empty > >> > >> vasili > >> > >> On Tue, May 27, 2008 at 4:37 PM, Thomas Hartman <[EMAIL PROTECTED]> wrote: > >>> > >>> maybe try > >>> > >>> runghc Setup.hs clean > >>> > >>> or fresh darcs checkout and try build again from scratch. it's helped > >>> me in the past. > >>> > >>> thomas. > >>> > >>> > >>> Am 26. Mai 2008 21:32 schrieb Galchin, Vasili <[EMAIL PROTECTED]>: > >>> > Hello, > >>> > > >>> > One of my test cases will not build. I am running: > >>> > > >>> > [EMAIL PROTECTED]:~$ ghc -v > >>> > Glasgow Haskell Compiler, Version 6.8.2, for Haskell 98, stage 2 booted > >>> > by > >>> > GHC version 6.8.2 > >>> > Using package config file: /usr/local/lib/ghc-6.8.2/package.conf > >>> > wired-in package base mapped to base-3.0.1.0 > >>> > wired-in package rts mapped to rts-1.0 > >>> > wired-in package haskell98 mapped to haskell98-1.0.1.0 > >>> > wired-in package template-haskell mapped to template-haskell-2.2.0.0 > >>> > wired-in package ndp not found. > >>> > Hsc static flags: -static > >>> > *** Deleting temp files: > >>> > Deleting: > >>> > *** Deleting temp dirs: > >>> > Deleting: > >>> > ghc-6.8.2: no input files > >>> > Usage: For basic information, try the `--help' option. > >>> > [EMAIL PROTECTED]:~$ > >>> > > >>> > Here is the build: > >>> > > >>> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > >>> > Setup.lhs configure --prefix=$HOME > >>> > Configuring mlock-1.0... > >>> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > >>> > Setup.lhs build > >>> > Preprocessing executables for mlock-1.0... > >>> > Building mlock-1.0... > >>> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > >>> > Setup.lhs install > >>> > Installing: /home/vigalchin/bin > >>> > Setup.lhs: dist/build/mlock/mlock: copyFile: does not exist (No such > >>> > file or > >>> > directory) > >>> > > >>> > The install step fails. I guess "copyFile" is used to copy the > >>> > executable to > >>> > the install directory?? > >>> > > >>> > Regards, vasili > >>> > > >>> > > >>> > > >>> > > >>> > ___ > >>> > 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] Aren't type system extensions fun?
On 5/26/08, Andrew Coppin <[EMAIL PROTECTED]> wrote: > This is probably the first real use I've ever seen of so-called rank-2 > types, and I'm curios to know why people think they need to exist. > [Obviously when somebody vastly more intelligent than me says something is > necessary, they probably know something I don't...] The usual example I've seen for "beauty in rank-2 types" is the ST monad. ST lets you define 'stateful' imperative algorithms with destructive update, but be able to call them safely from pure-functional code. This is made safe by a "phantom" type variable and the rank-2 type of runST: > runST :: forall a. (forall s. ST s a) -> a The "s" in ST logically represents the "initial state" used by the imperative computation it represents; it tracks any allocations and updates that need to be made before the computation can run. By requiring that the passed in computation works for *any* initial state, you guarantee that it can't reference any external store or return data from within the store; for example, consider this: > newSTRef :: forall s a. a -> ST s (STRef s a) > mkZero :: forall s. ST s (STRef s Int) > mkZero = newSTRef 0 Now consider trying to type "runST mkZero"; first we generate a new type variable "s1" for the "s" in mkZero, then use it to instantiate the result type, "a": runST :: (forall s. ST s (STRef s1 a)) -> STRef s1 a Now we need to unify s1 with s to match mkZero's type for the first argument. But we can't do that, because then "s" escapes its forall scope. So we can statically guarantee that no references escape from runST! --- Another example that I personally am attached to is Prompt: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/MonadPrompt (There's no Haddock documentation on that site, but the source code is well-commented and there's a module of examples). The function I want to talk about is "runPrompt" > prompt :: forall p a. p a -> Prompt p a > runPrompt :: forall p r. (forall a. p a -> a) -> Prompt p r -> r Lets instantiate p and r to simplify things; I'll use [] for p and Int for r. > test1 :: Prompt [] Int > test1 = prompt [1,2,3] > test2 :: Prompt [] Int > test2 = do >x <- prompt ['A', 'B', 'C'] >return (ord x) -- ord :: Char -> Int Now, the type of runPrompt specialized for these examples is > runPrompt :: (forall a. [a] -> a) -> Prompt [] Int -> Int Notice that we need to pass in a function that can take -any- list and return an element. One simple example is "head": > head :: forall a. [a] -> a > head (x:xs) = x So, putting it together: ghci> runPrompt head test1 1 ghci> runPrompt head test2 65 -- ascii code for 'A'. Now, this isn't that great on its own; wouldn't it be useful to be able to get some information about the type of result needed when writing your prompt-handler function? Then you could do something different in each case. That's a question for another topic, but to get you started, start looking around for information on GADTs. -- ryan ___ 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]
On 5/27/08, Darrin Thompson <[EMAIL PROTECTED]> wrote: > On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <[EMAIL PROTECTED]> wrote: > > 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). > Nice. That's the first time any of this really made sense to me. Is it > possible to construct valid argument for that function? Yes, it's easy, especially since there is only one total function of that type: id -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Warning for Andrew: this post explains a new-to-you typed lambda calculus and a significant part of the innards of Hindley-Milner typing in order to answer your questions. Expect to bang your head a little! On Tue, 27 May 2008, Andrew Coppin wrote: > - A function starts out with a polymorphic type, such as 'x -> x'. > Which is the same as "forall x. x -> x". > - Each time the function is called, all the type variables have to be locked > down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or > something. > Yep, in fact in the explicitly-typed calculus commonly used as a model for rank-n polymorphism (System F) there are explicit type lambdas and type applications that do exactly this. Using /\ for a type lambda and [term type] for type applications, id might be written thus: id = /\t.(\x::t->x) and called thus: [id Int] 1 > - By the above, any function passed to a high-order function has to have all > its type variables locked down, yielding a completely monomorphic function. > Yep. > - The "forall" hack somehow convinces the type checker to not lock down some > of the type variables. In this way, the type variables relating to a function > can remain unlocked until we reach each of the call sites. This allows the > variables to be locked to different types at each site [exactly as they would > be if the function were top-level rather than an argument]. > Not a hack. If there is a hack, it's in /not/ including a forall for rank-1 types. Foralls correspond to type lambdas in the same way that ->s correspond to ordinary lambdas. > - Why are top-level variables and function arguments treated differently by > the type system? The big difference is between lambdas and binding groups (as in let, top-level etc). With the binding group, any constraints on a value's type will be found within its scope - so the type can be 'generalised' there, putting a forall around it. The same isn't true of lambdas, and so their parameters can only be polymorphic given an appropriate type annotation. For extra confusion, type variables are themselves monomorphic[1]. > - Why do I have to manually tell the type checker something that should be > self-evident? It isn't - the general case is in fact undecidable. > - Why do all type variables need to be locked down at each call site in the > first place? Find an alternative model for parametric polymorphism that works! Note that 'not locking down' is equivalent to locking down to parameters you took from elsewhere. As such, if you stick to rank-1 types you never actually notice the difference - whereas it makes the type system an awful lot easier to understand. > - Why is this virtually never a problem in real Haskell programs? I wouldn't go so far as to say virtually never, I've run into it a fair few times - but normally until you're trying to do pretty generalised stuff it's just not necessary. > - Is there ever a situation where the unhacked type system behaviour is > actually desirably? There are plenty of situations where a rank-1 type is the correct type. If you give id a rank-2 type, it's more specific - just as if you typed it Int->Int. > - Why can't the type system automatically detect where polymorphism is > required? Because there's often more than one possible type for a term, without a 'most general' type. > - 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? > About as much as the undecidability of the halting problem and the incompleteness theory suggest our understanding of computation and logic is fundamentally flawed - which is to say, not at all. > The key problem seems to be that the GHC manual assumes that anybody reading > it will know what "universal quantification" actually means. Unfortunately, > neither I nor any other human being I'm aware of has the slightest clue what > that means. Guess nobody on this list's human, huh? It's really not the GHC manual's job to teach you the language extensions from scratch any more than it should teach Haskell 98 from scratch. I guess the real question is where the relevant community documentation is, something I have to admit to not having needed to check. > existential quantification = "this is true for SOMETHING" > universal quantification = "this is true for EVERYTHING" > The type "forall x. x -> x" is "for all types x, x -> x". As in, "for all types x, (\y -> y) :: x -> x". [1] Actually this is no longer quite true since GHC now supports impredicative polymorphism in which type variables can be instantiated with polymorphic types. But please ignore that for now? -- [EMAIL PROTECTED] 'In Ankh-Morpork even the shit have a street to itself... Truly this is a land of opportunity.' - Detritus, Men at Arms ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.
Re: [Haskell-cafe] a build problem ....
I think dist gets populated when you do build. > > 2008/5/27 Galchin, Vasili <[EMAIL PROTECTED]>: >> when I do a "clean" followed by "configure" then dist is empty >> >> vasili >> >> On Tue, May 27, 2008 at 4:37 PM, Thomas Hartman <[EMAIL PROTECTED]> wrote: >>> >>> maybe try >>> >>> runghc Setup.hs clean >>> >>> or fresh darcs checkout and try build again from scratch. it's helped >>> me in the past. >>> >>> thomas. >>> >>> >>> Am 26. Mai 2008 21:32 schrieb Galchin, Vasili <[EMAIL PROTECTED]>: >>> > Hello, >>> > >>> > One of my test cases will not build. I am running: >>> > >>> > [EMAIL PROTECTED]:~$ ghc -v >>> > Glasgow Haskell Compiler, Version 6.8.2, for Haskell 98, stage 2 booted >>> > by >>> > GHC version 6.8.2 >>> > Using package config file: /usr/local/lib/ghc-6.8.2/package.conf >>> > wired-in package base mapped to base-3.0.1.0 >>> > wired-in package rts mapped to rts-1.0 >>> > wired-in package haskell98 mapped to haskell98-1.0.1.0 >>> > wired-in package template-haskell mapped to template-haskell-2.2.0.0 >>> > wired-in package ndp not found. >>> > Hsc static flags: -static >>> > *** Deleting temp files: >>> > Deleting: >>> > *** Deleting temp dirs: >>> > Deleting: >>> > ghc-6.8.2: no input files >>> > Usage: For basic information, try the `--help' option. >>> > [EMAIL PROTECTED]:~$ >>> > >>> > Here is the build: >>> > >>> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell >>> > Setup.lhs configure --prefix=$HOME >>> > Configuring mlock-1.0... >>> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell >>> > Setup.lhs build >>> > Preprocessing executables for mlock-1.0... >>> > Building mlock-1.0... >>> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell >>> > Setup.lhs install >>> > Installing: /home/vigalchin/bin >>> > Setup.lhs: dist/build/mlock/mlock: copyFile: does not exist (No such >>> > file or >>> > directory) >>> > >>> > The install step fails. I guess "copyFile" is used to copy the >>> > executable to >>> > the install directory?? >>> > >>> > Regards, vasili >>> > >>> > >>> > >>> > >>> > ___ >>> > 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] Re: 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! All possible choices wouldn't be type-safe, so its even worse. 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. Interestingly, if you throw in the undocumented "forall" keyword, everything magically works: (forall x. x -> x) -> (Char, Bool) But you have to do it right. forall x . (x -> x) -> (Char, Bool) is equivalent to the version without forall, and does you no good. (Note the parentheses to see why these two types are different). So there lies no magic in mentioning forall, but art in putting it in the correct position. The key problem seems to be that the GHC manual assumes that anybody reading it will know what "universal quantification" actually means. Unfortunately, neither I nor any other human being I'm aware of has the slightest clue what that means. A quick search on that infallable reference [sic] Wikipedia yields several articles full of dense logic theory. Trying to learn brand new concepts from an encyclopedia is more or less doomed from the start. As far as I can comprehend it, we have existential quantification = "this is true for SOMETHING" universal quantification = "this is true for EVERYTHING" Quite how that is relevant to the current discussion eludes me. Your "MUST accept any type" is related to universal quantification, and your "MAY accept any type" is related to existential quantification: This works for EVERYTHING, so it MUST accept any type. This works for SOMETHING, so it accepts some unknown type. Quantification is the logic word for "abstracting by introducing a name to filled with content later". For example, in your above paragraph you wanted to tell us that no human being you are aware of has the slightest clue what "universal quantification" means. You could have done so by enumerating all human beings you are aware of. Instead, you used universal quantification: for all HUMAN BEING, HUMAN BEING has no clue. (shortened to not overcomplicate things, HUMAN BEING is the name here). Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANN: HSmugMug 0.1 - a haskell wrapper to the photo site smugmug's api
Released May 27th, 2008. I've been working for a little while on a haskell wrapper to the photo hosting site Smugmug's api. As of now, the library is pretty simple - it is 'read-only' - ie, you can't use it to upload to or create galleries, but I still think it is potentially useful to haskell/smugmug users. I created it primarily so I could integrate my photos at smugmug into my website, which you can see in the 'photos' section of my website - a very primitive but proof of concept-esque demonstration. I have deliberately not included much glue between the actual api and the use of it, because I think that is something that can more cleanly evolve out of use - if people find themselves repeating certain patterns when using the api, those would logically become part of the api wrapper. So, let me know what you think! Full release notes, brief tutorial, install instructions, etc, at http://dbpatterson.com/articles/10 . Feedback welcome! (this is the first thing longer than a 5 liner that I've written in haskell, so be gentle) Daniel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] a build problem ....
actually I also got a core file. ... when I am running "runghc Setup.lhs ." and get a core file when I run "gdb" on the core file in this situation what Linux executable should I specify with the core file? ghc? Also when building ghc how to do I specify to keep symbol table for debugging? Is it -g just like C?? Vasili On Tue, May 27, 2008 at 4:47 PM, Galchin, Vasili <[EMAIL PROTECTED]> wrote: > when I do a "clean" followed by "configure" then dist is empty > > vasili > > > On Tue, May 27, 2008 at 4:37 PM, Thomas Hartman <[EMAIL PROTECTED]> > wrote: > >> maybe try >> >> runghc Setup.hs clean >> >> or fresh darcs checkout and try build again from scratch. it's helped >> me in the past. >> >> thomas. >> >> >> Am 26. Mai 2008 21:32 schrieb Galchin, Vasili <[EMAIL PROTECTED]>: >> > Hello, >> > >> > One of my test cases will not build. I am running: >> > >> > [EMAIL PROTECTED]:~$ ghc -v >> > Glasgow Haskell Compiler, Version 6.8.2, for Haskell 98, stage 2 booted >> by >> > GHC version 6.8.2 >> > Using package config file: /usr/local/lib/ghc-6.8.2/package.conf >> > wired-in package base mapped to base-3.0.1.0 >> > wired-in package rts mapped to rts-1.0 >> > wired-in package haskell98 mapped to haskell98-1.0.1.0 >> > wired-in package template-haskell mapped to template-haskell-2.2.0.0 >> > wired-in package ndp not found. >> > Hsc static flags: -static >> > *** Deleting temp files: >> > Deleting: >> > *** Deleting temp dirs: >> > Deleting: >> > ghc-6.8.2: no input files >> > Usage: For basic information, try the `--help' option. >> > [EMAIL PROTECTED]:~$ >> > >> > Here is the build: >> > >> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell >> > Setup.lhs configure --prefix=$HOME >> > Configuring mlock-1.0... >> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell >> > Setup.lhs build >> > Preprocessing executables for mlock-1.0... >> > Building mlock-1.0... >> > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell >> > Setup.lhs install >> > Installing: /home/vigalchin/bin >> > Setup.lhs: dist/build/mlock/mlock: copyFile: does not exist (No such >> file or >> > directory) >> > >> > The install step fails. I guess "copyFile" is used to copy the >> executable to >> > the install directory?? >> > >> > Regards, vasili >> > >> > >> > >> > >> > ___ >> > 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] a build problem ....
when I do a "clean" followed by "configure" then dist is empty vasili On Tue, May 27, 2008 at 4:37 PM, Thomas Hartman <[EMAIL PROTECTED]> wrote: > maybe try > > runghc Setup.hs clean > > or fresh darcs checkout and try build again from scratch. it's helped > me in the past. > > thomas. > > > Am 26. Mai 2008 21:32 schrieb Galchin, Vasili <[EMAIL PROTECTED]>: > > Hello, > > > > One of my test cases will not build. I am running: > > > > [EMAIL PROTECTED]:~$ ghc -v > > Glasgow Haskell Compiler, Version 6.8.2, for Haskell 98, stage 2 booted > by > > GHC version 6.8.2 > > Using package config file: /usr/local/lib/ghc-6.8.2/package.conf > > wired-in package base mapped to base-3.0.1.0 > > wired-in package rts mapped to rts-1.0 > > wired-in package haskell98 mapped to haskell98-1.0.1.0 > > wired-in package template-haskell mapped to template-haskell-2.2.0.0 > > wired-in package ndp not found. > > Hsc static flags: -static > > *** Deleting temp files: > > Deleting: > > *** Deleting temp dirs: > > Deleting: > > ghc-6.8.2: no input files > > Usage: For basic information, try the `--help' option. > > [EMAIL PROTECTED]:~$ > > > > Here is the build: > > > > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > > Setup.lhs configure --prefix=$HOME > > Configuring mlock-1.0... > > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > > Setup.lhs build > > Preprocessing executables for mlock-1.0... > > Building mlock-1.0... > > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > > Setup.lhs install > > Installing: /home/vigalchin/bin > > Setup.lhs: dist/build/mlock/mlock: copyFile: does not exist (No such file > or > > directory) > > > > The install step fails. I guess "copyFile" is used to copy the executable > to > > the install directory?? > > > > Regards, vasili > > > > > > > > > > ___ > > 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] Aren't type system extensions fun? [Further analysis]
Darrin Thompson wrote: On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <[EMAIL PROTECTED]> wrote: 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). Nice. That's the first time any of this really made sense to me. Is it possible to construct valid argument for that function? agree, the types-are-arguments-too makes thinking about how it works A LOT clearer... and it's actually what GHC's intermediate Core language does. It's too bad there's no way in the language syntax to make that interpretation clearer. (That's a subset of explicit dependent types -- explicitness is opposite type inference, not static vs. dependentness.) -Isaac ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Chaddaï Fouché wrote:
- Why are top-level variables and function arguments treated differently by
the type system?
They aren't
In a sense, they are.
id :: (forall a. a -> a)
useId :: (forall a. a -> a) -> (Int,Bool)
brokenUseId :: (forall a. (a -> a) -> (Int,Bool))
brokenUseId :: (a -> a) -> (Int,Bool)
Note that polymorphic variables in function argument types scope over
the function results too by default. And that's a good thing. Otherwise,
id :: a -> a
would be understood as
brokenId :: (forall a. a) -> (forall a. a)
which is not at all intended ("id" specialized to _|_ values only).
Basically, you only want higher-rank types in Haskell when you know what
you're doing: due to parametric polymorphism it is less often useful to
apply an argument function to, e.g., both Int and Bool than you might
find in Python, for example. In Haskell, more often you would just take
two functions as arguments e.g.
useFunctions :: (Int -> Int) -> (Bool -> Bool) -> (Int,Bool)
or more interestingly, let's make the caller be able to choose any kind
of number:
useFunctions2 :: (Num a) => (a -> a) -> (Bool -> Bool) -> (a,Bool)
a.k.a.
useFunctions2 :: forall a. (Num a) => (a -> a) -> (Bool -> Bool) -> (a,Bool)
-Isaac
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] a build problem ....
maybe try runghc Setup.hs clean or fresh darcs checkout and try build again from scratch. it's helped me in the past. thomas. Am 26. Mai 2008 21:32 schrieb Galchin, Vasili <[EMAIL PROTECTED]>: > Hello, > > One of my test cases will not build. I am running: > > [EMAIL PROTECTED]:~$ ghc -v > Glasgow Haskell Compiler, Version 6.8.2, for Haskell 98, stage 2 booted by > GHC version 6.8.2 > Using package config file: /usr/local/lib/ghc-6.8.2/package.conf > wired-in package base mapped to base-3.0.1.0 > wired-in package rts mapped to rts-1.0 > wired-in package haskell98 mapped to haskell98-1.0.1.0 > wired-in package template-haskell mapped to template-haskell-2.2.0.0 > wired-in package ndp not found. > Hsc static flags: -static > *** Deleting temp files: > Deleting: > *** Deleting temp dirs: > Deleting: > ghc-6.8.2: no input files > Usage: For basic information, try the `--help' option. > [EMAIL PROTECTED]:~$ > > Here is the build: > > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > Setup.lhs configure --prefix=$HOME > Configuring mlock-1.0... > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > Setup.lhs build > Preprocessing executables for mlock-1.0... > Building mlock-1.0... > [EMAIL PROTECTED]:~/FTP/Haskell/unix-2.2.0.0/tests/mlock$ runhaskell > Setup.lhs install > Installing: /home/vigalchin/bin > Setup.lhs: dist/build/mlock/mlock: copyFile: does not exist (No such file or > directory) > > The install step fails. I guess "copyFile" is used to copy the executable to > the install directory?? > > Regards, vasili > > > > > ___ > 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] Examples of using Haskell for mathematics
Along these lines, check out (and maybe quote) the July 2007 note from Doug McIlroy to the Haskell list: http://www.haskell.org/pipermail/haskell/2007-July/019632.html I've particularly been enjoying Doug's paper "The Music of Streams", mentioned in that note. - Conal On Mon, May 26, 2008 at 11:49 AM, Henning Thielemann < [EMAIL PROTECTED]> wrote: > > On Mon, 26 May 2008, Brent Yorgey wrote: > > Hi all! >> >> In a couple weeks I will be giving a short (15-min.) talk to an audience >> of >> mostly mathematicians, entitled "Executable Mathematics: A Whirlwind >> Introduction to Haskell". The idea will be to give a flavor of Haskell, >> its >> uniquenesses, and why it is a great language for playing around with >> mathematics, by way of some well-chosen examples. There are definitely >> plenty of such examples out there, and I've already found quite a few that >> I >> might use, but I thought I would send an email to the cafe to ask whether >> anyone has any code which you think particularly exemplifies some aspect >> of >> why Haskell is a great language for mathematics. I'm looking to include a >> wide range of examples, so any length (from a few to hundreds of lines of >> code) and any level (from simple number theory to things only a few people >> in the world understand) are fair game. >> > > The mathematical examples I like most are power series (including elegant > solution of differential equations and series inversion) and computable real > numbers. > > http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numeric-prelude > > > http://darcs.haskell.org/numericprelude/src/MathObj/PowerSeries/DifferentialEquation.hs > > http://darcs.haskell.org/numericprelude/docs/README > > > ___ > 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] Re: HDBC with SQL Server / OBDC
John Goerzen wrote:
On Sunday 25 May 2008 11:24:20 am Morten Holm Pedersen wrote:
am trying to do a simple DB connection from Haskell to a SQL Server 2005
(on Windows obviously). The DSN name ("Nylon") works from C++ but when
running the below example (or any other I can think of) ghci crashes.
Does anyone know a resolution for this or where the problem can possible
be ?
First off, I'd suggest separating out the steps in your do block to
individual pieces so you can isolate where the crash is. Also, what sort of
error message do you get when the crash occurs? And are you using a MingW
GHC?
-- John
I am running it in plain Windows (from cmd). The text in the mail is the
full communication from the system - ie. just stops without any message.
Sometimes Windows gives an errors a well.
The do was just an attemp to illustrate. Really I just need to do
con=connectODBC "DSN=Nylon"
and then write "con" on the GHCi prompt to crash the system.
Morten
___
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]
On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <[EMAIL PROTECTED]> wrote: > 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). > Nice. That's the first time any of this really made sense to me. Is it possible to construct valid argument for that function? -- Darrin ___ 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] Re: Aren't type system extensions fun? [Further analysis]
2008/5/27 Andrew Coppin <[EMAIL PROTECTED]>: > Gleb Alexeyev wrote: >> >> foo :: (forall a . a -> a) -> (Bool, String) >> foo g = (g True, g "bzzt") > > 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. No, this is a flaw in the type inferencer, but simply adding the Rank-N type to our type system makes type inference undecidable. I would argue against the "obviously perfectly type-safe" too since most type system don't even allow for the second case. > 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! None of the possible choice would be type-safe. This type means : whatever the type a, function of type (a -> a) to a pair (Char, Bool) But the type a is unique while in the body of your function, a would need to be two different types. > Interestingly, if you throw in the undocumented "forall" keyword, everything > magically works: > > (forall x. x -> x) -> (Char, Bool) > > Obviously, the syntax is fairly untidy. And the program is now not valid > Haskell according to the written standard. And best of all, the compiler > seems unable to deduce this type automatically either. As I said, the compiler can't deduce this type automatically because it would make type inference undecidable. > 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. So far, the only really plausible theory I have been > able to come up with is this: Rank-N type aren't a "hack", they're perfectly understood and fit nicely into the type system, their only problem is type inference. > yada yada, complicated theory... cut What you don't seem to understand is that "(x -> x) -> (Char, Bool)" and "(forall x. x -> x) -> (Char, Bool)" are two very different beasts, they aren't the same type at all ! Taking a real world situation to illustrate the difference : Imagine you have different kind of automatic washer, some can wash only wool while others can wash only cotton and finally some can wash every kind of fabric... You want to do business in the washing field but you don't have a washer so you publish an announce : If your announce say "whatever the type of fabric x, give me a machine that can wash x and all you clothes and I'll give you back all your clothes washed", the customer won't be happy when you will give him back his wool clothes that the cotton washing machine he gave you torn to shreds... What you really want to say is "give me a machine that can wash any type of fabric and your clothes and I'll give you back your clothes washed". The first announce correspond to "(x -> x) -> (Char, Bool)", the second to "(forall x. x -> x) -> (Char, Bool)" > - Why are top-level variables and function arguments treated differently by > the type system? They aren't (except if you're speaking about the monomorphism restriction and that's another subject entirely). > - Why do I have to manually tell the type checker something that should be > self-evident? Because it isn't in all cases to a machine, keep in mind you're an human and we don't have real IA just yet. > - Why is this virtually never a problem in real Haskell programs? Because we seldom needs Rank-2 polymorphism. > - Is there ever a situation where the unhacked type system behaviour is > actually desirably? Almost everytime. Taking a simple example : map If the type of map was "(forall x. x -> x) -> [a] -> [a]", you could only pass it "id" as argument, if it was "(forall x y. x -> y) -> [a] -> [b]", you couldn't find a function to pass to it... (No function has the type "a -> b") > - Why can't the type system automatically detect where polymorphism is > required? It can and does, it can't detect Rank-N (N > 1) polymorphism because it would be undecidable but it is fine with Rank-1 polymorphism (which is what most people call polymorphism). > - 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? Maybe this should suggest to you that it is rather your understanding of the question that is flawed... Haskell's type system is a fine meshed mechanism that is soundly grounded in logic and mathematics, it is rather unlikely that nobody would have noted the problem if it was so important... -- Jedaï
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
andrewcoppin: > Gleb Alexeyev wrote: > >foo :: (forall a . a -> a) -> (Bool, String) > >foo g = (g True, g "bzzt") > > 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. I'm sorry you are still confused, Andrew. This is documented rather nicely in section 8.7.4.2 of the GHC user's guide. In particularly, you'll want to not ethat arbitrary rank type inference is undecidable, so GHC imposes a simple rule requiring you to annotate those polymorphic parameters of higher rank you want. See here http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id408394 Read this carefully, and then read the references. > Interestingly, if you throw in the undocumented "forall" keyword, > everything magically works: > > (forall x. x -> x) -> (Char, Bool) > > Obviously, the syntax is fairly untidy. And the program is now not valid > Haskell according to the written standard. And best of all, the compiler > seems unable to deduce this type automatically either. Please read the above link. In particular, pay attention to the word "undecidable". Reading and comprehending Odersky and Laufer's paper, "Putting type annotations to work", will explain precisely why you're butting your head up against deciability. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Gleb Alexeyev wrote:
foo :: (forall a . a -> a) -> (Bool, String)
foo g = (g True, g "bzzt")
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.
Interestingly, if you throw in the undocumented "forall" keyword,
everything magically works:
(forall x. x -> x) -> (Char, Bool)
Obviously, the syntax is fairly untidy. And the program is now not valid
Haskell according to the written standard. And best of all, the compiler
seems unable to deduce this type automatically either.
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. So far, the only really plausible theory I have
been able to come up with is this:
- A function starts out with a polymorphic type, such as 'x -> x'.
- Each time the function is called, all the type variables have to be
locked down to real types such as 'Int' or 'Either (Maybe (IO Int))
String' or something.
- By the above, any function passed to a high-order function has to have
all its type variables locked down, yielding a completely monomorphic
function.
- In the exotic case above, we specifically WANT a polymorphic function,
hence the problem.
- The "forall" hack somehow convinces the type checker to not lock down
some of the type variables. In this way, the type variables relating to
a function can remain unlocked until we reach each of the call sites.
This allows the variables to be locked to different types at each site
[exactly as they would be if the function were top-level rather than an
argument].
This is a plausible hypothesis for what this language feature actually
does. [It is of course frustrating that I have to hypothesise rather
than read a definition.] However, this still leaves a large number of
questions unanswered...
- Why are top-level variables and function arguments treated differently
by the type system?
- Why do I have to manually tell the type checker something that should
be self-evident?
- Why do all type variables need to be locked down at each call site in
the first place?
- Why is this virtually never a problem in real Haskell programs?
- Is there ever a situation where the unhacked type system behaviour is
actually desirably?
- 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?
Unfortunately, the GHC manual doesn't have a lot to say on the matter.
Reading section 8.7.4 ("Arbitrary-rank polymorphism"), we find the
following:
- "The type 'x -> x' is equivilent to 'forall x. x -> x'." [Um... OK,
that's nice?]
- "GHC also allows you to do things like 'forall x. x -> (forall y. y ->
y)'." [Fascinating, but what does that MEAN?]
- "The forall makes explicit the universal quantification that is
implicitly added by Haskell." [Wuh??]
- "You can control this feature using the following language options..."
[Useful to know, but I still don't get what this feature IS.]
The examples don't help much either, because (for reasons I haven't
figured out yet) you apparently only need this feature in fairly obscure
cases.
The key problem seems to be that the GHC manual assumes that anybody
reading it will know what "universal quantification" actually means.
Unfortunately, neither I nor any other human being I'm aware of has the
slightest clue what that means. A quick search on that infallable
reference [sic] Wikipedia yields several articles full of dense logic
theory. Trying to learn brand new concepts from an encyclopedia is more
or less doomed from the start. As far as I can comprehend it, we have
existential quantification = "this is true for SOMETHING"
universal quantification = "this is true for EVERYTHING"
Quite how that is relevant to the current discussion eludes me.
I have complete confidence that whoever wrote the GHC manual knew
exactly what they meant. I am also fairly confident that this was the
same person who implemented and
