Re: [Haskell-cafe] Packed String parameters
Hello Chad, Thursday, January 19, 2006, 1:09:38 AM, you wrote: SC parameter. The input file is over 1 million lines long. Any ideas? see at the BlockIO and FastIO libraries http://cryp.to/blockio/blockio-2004-10-10.tar.gz http://www.isi.edu/~hdaume/haskell/FastIO.tar.gz -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (no subject)
___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Simple IO Regions
Andrew Pimlott wrote: liftR :: (InRegion mark marks) = (h - m a) - Private mark h - Region marks m a liftR f (Private h) = Region $ f h This is not as safe. Try modifying your test2. Okay, I missed this... Have renamed the function unsafeLiftR... As you say still useful for building libraries provided you do not export the region code from the library that uses it. Of course an alternative is just to have an opaque/abstract handle, and not export the data-constructor. Keean. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Packed String parameters
Thanks, Bulat. Taking a look at Hal's FastIO library now... Hal, it looks like your library could be helpful, especially if there is a way to construct a FastIO.Handle from stdin. Can this be done, or do I need to start with an actual file? Thanks, Chad Hello Chad, Thursday, January 19, 2006, 1:09:38 AM, you wrote: SC parameter. The input file is over 1 million lines long. Any ideas? see at the BlockIO and FastIO libraries http://cryp.to/blockio/blockio-2004-10-10.tar.gz http://www.isi.edu/~hdaume/haskell/FastIO.tar.gz -- Best regards, Bulatmailto:bulatz at HotPOP.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] Simple IO Regions
Brandon Moore [EMAIL PROTECTED] writes: (snip) The term I've heard is skolem constant, which is a freshly invented thing distinct from everything else. (snip) There's a nice easy-going example in chapter 8 of http://www.cl.cam.ac.uk/Teaching/2000/LogicProof/notes.pdf where quantifiers are removed from first-order formulae. (this aside moved from haskell to haskell-cafe) -- Mark ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type Eigenvariable [was: Simple IO Regions]
On Thu, 2006-01-19 at 19:18 -0800, [EMAIL PROTECTED] wrote: . . . _variables_. The paper argues, btw, for the separation of those senses and for a new quantifier to mean uniqueness only. In short, when we write forall x. forall y. body then x may well be equal to y (in body). And so, forall x. forall y. B[x,y] forall z. B[z,z] OTH, when we write |nabla x. nabla y. body| then x and y are guaranteed to be different, and so the implication above no longer holds. OK, I gotta ask: is |nabla x, nabla y. phi(x,y)| logically equivalent to |forall x, forall y. x y only-if phi(x,y)|? I use |P only-if Q| for |P materially implies Q|. -- Bill Wood ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Type Eigenvariable
Bill Wood wrote: is |nabla x, nabla y. phi(x,y)| logically equivalent to |forall x, forall y. x y only-if phi(x,y)|? I use |P only-if Q| for |P materially implies Q| First of all, I should remark that Miller and Tiu introduce two calculi (with names that are hardly speakable, even in TeX). One of them is the sequent calculus with globally and locally scoped eigen-variables and the _open_ world of predicates. The other, calculus of definitions, uses the _closed_ world of predicates (the authors neglect to emphasize the closedness, btw). Universal and existentials quantifiers deal with eigenvariables of the global scope; only nabla can affect the locally scoped eigen variables. Also, the only rules that can irrevocable destroy/create locally scoped variables are False -- X and X -- True. Because of these properties, nabla quantification in the open world neither implies nor implied by the universal quantification (ditto for the existential). So, the answer to your question for the open world calculus is no. In the closed world, the matters are muddier and depend on the predicates in the closed world. If we manage to reduce our sequent to the form, X -- Y where X has no definition, then, by closed world property, we proved the sequent (regardless of how many locally-scoped variables we have there). So, we can in some cases replace quantifiers. I must acknowledge Chung-chieh Shan for helpful discussions on these matters. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
