January 2006 - Haskell-Cafe

Re: Type Eigenvariable
by oleg＠pobox.com 20 Jan '06

20 Jan '06

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.

1 0

Type Eigenvariable [was: Simple IO Regions]
by oleg＠pobox.com 20 Jan '06

20 Jan '06

A good explanation is in Section `1. Eigenvariables and generic reasoning' of @inproceedings{MillerTiu, author = {Dale Miller and Alwen Fernanto Tiu}, title = {A Proof Theory for Generic Judgments: An extended abstract}, booktitle = {LICS}, year = {2003}, pages = {118-127}, url = \url{http://users.rsise.anu.edu.au/~tiu/lics03sub.pdf}, crossref = {DBLP:conf/lics/2003}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/lics/2003, title = {18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings}, booktitle = {LICS}, publisher = {IEEE Computer Society}, year = {2003}, isbn = {0-7695-1884-2}, key = {LICS}, } The section explains in which sense eigen-variables are _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. Alwen Tiu's web page http://users.rsise.anu.edu.au/~tiu/ lists the journal version of the paper.

2 1

Re: [Haskell-cafe] Packed String parameters
by Scherrer, Chad 19 Jan '06

19 Jan '06

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, Bulat mailto:bulatz at HotPOP.com

2 1

Re: [Haskell] Simple IO Regions
by mark＠ixod.org 19 Jan '06

19 Jan '06

Brandon Moore <brandonm(a)yahoo-inc.com> 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

1 0

Re: [Haskell] Simple IO Regions
by Keean Schupke 19 Jan '06

19 Jan '06

Hi Oleg, Just made a few modifications and thought it might be useful to people. I have rewritten the functions as "liftR" and "bracketR" over a "MonadIO" monad interface (allowing monad-transformers to be used). This is now usable as Region library, as you can lift any arbitrary IO function into a Region. I don't think I have overlooked anything, and I think it is as safe as the original... but perhaps you would like to check for stupid mistakes... The exported interface is intended to be "liftR", "bracketR" and "runR". See attached "MonadIORegion.hs"... Regards, Keean. oleg(a)pobox.com wrote: >This message shows a very simple implementation of Monadic Regions >(for the particular case of IO and reading the file). The technique >*statically* guarantees that neither a file handle nor any computation >involving the handle can leak outside of the region that created >it. Therefore, the handle can be safely closed (and its resources >disposed of) whenever control leaves the corresponding 'withFile' >block. Many handles can be open simultaneously, the type system >enforces the proper nesting of their regions. The technique has no >run-time overhead and induces no run-time errors. Unlike the previous >implementation of monadic regions, only the basic extensions >(higher-ranked types and one two-parameter type class) are used. No >undecidable instances, no functional dependencies (let alone >overlapping instances) are required. In fact, the implementation uses >only one trivial typeclass and one trivial instance. > >

3 7

(no subject)
by Andreas Bakurov 19 Jan '06

19 Jan '06

1 0

How to redirect a handle...
by Dimitry Golubovsky 18 Jan '06

18 Jan '06

Thanks everybody who answered. Indeed, forkProcess is something I completely overlooked... -- Dimitry Golubovsky Anywhere on the Web

1 0

Packed String parameters
by Scherrer, Chad 18 Jan '06

18 Jan '06

To read a file using a packed string, I need to use this function, right? hGetPS :: Handle -> Int -> IO PackedString What's the Int? Do you have to specify the length in advance? I don't know how packed strings are implemented, and I'm having trouble finding much documentation. I'm trying to speed up this horribly slow thing: dot :: [Double] -> [Double] -> Double dot x y = sum $ zipWith (*) x y main = getContents >>= sequence_ . map (print . dot weights . map read . words) . lines The idea is to take a dot product of each line of a file with a fixed vector of weights, and send the result to stdout. I thought PackedString's might help, but I'm not sure what to do with that parameter. The input file is over 1 million lines long. Any ideas? Thanks, Chad Scherrer Computational Mathematics Group Pacific Northwest National Laboratory "Time flies like an arrow; fruit flies like a banana." -- Groucho Marx

2 1

How to redirect a handle within a thread (GHC 6.4.1 runtime)?
by Dimitry Golubovsky 18 Jan '06

18 Jan '06

Is it possible to redirect a Handle (say stdout) somewhere only within a running thread (started with forkIO) not touching the same handle for the main and other threads? I have a lot of code written with putStr(Ln) which was used in a program acting as a filter, i. e. stdout was redirected by the invoking shell. Now I want to run this code within a thread in other program, but output must go to a file (or a pipe, or anywhere else a file descriptor may be opened for). So fdToHandle is not good because I need to modify the `stdout' only for that thread, not to create a new Handle. Rewriting the code is not a convenient way (but will be done if nothing else helps) because then I will need to pass that handle around. Running that code in a separate executable is just a bit more convenient because I need to pass many parameters via command line (a thread inherits values of them), and therefore is also desired to be avioded. Functions in System.Process deal with external executables. Does there exist anything like runInteractiveProcess, but just forking a new process (the whole memory is copied, so everything will be inherited), but executes a particular function within the parent program? I'm afraid that if I just make a foreign call to `fork', the RTS may not understand this correctly. -- Dimitry Golubovsky Anywhere on the Web

5 4

Avoiding name collisions by using value spaces instead of modules
by Brian Hulley 18 Jan '06

18 Jan '06

Hi - A main problem I've found with Haskell is that within a module, too many things are put into the same scope. For example data Tree a b = Leaf a | Node {elem::b, lhs::Tree a b, rhs::Tree a b} puts Leaf, Node, elem, lhs, and rhs, into the module's namespace, as well as Tree. This means that if you want another kind of tree in the same module you've got to try and think of another word for Leaf, or else prefix every value constructor with some prefix of the tycon to try and prevent name collisions. I propose that the above declaration should introduce a *new module* Tree, as a sub module of the containing module, and Leaf, Node, elem etc will be put into this module, and not the module containing the data declaration itself. Identifiers in this child module could then either be used qualified or unqualified as long as they don't conflict with anything in the parent (containing) module, thus in the parent module, we could have: a = Tree.Leaf 3 b = Node{elem = 6, lhs = Leaf 2, rhs = Leaf 3} c = Tree.elem b c = b^elem where ^ is just a helpful sugar which binds tighter than function application and can be used anywhere to allow an "object oriented" way of thinking where the first arg is put on the left of the function (more on this later). Also, we could generalise the GHC GADT style data declarations by allowing any declarations to appear in the where part, and allow modules to consist of a single data declaration (ie begin with the keyword data instead of module) so that the contents of the Data.Set module would instead be something like: data Ord a => Set a = .... where insert :: Set a -> a -> Set a ... This would allow Set to be imported qualified into other modules where we could refer to the Set type by the single word Set instead of Set.Set (which I always think looks very strange indeed) ie module M where import qualified Data.Set as Set f :: a -> Set a -- no longer need to write a -> Set.Set a In fact, the whole complexity asociated with hiding components of a module and allowing unqualified imports could be discarded, since the correct resolution for each identifier would be determined by its typed context, just as in OOP the resolution is determined by the type of the object. So to summarise so far, for any value f :: T0 -> T1 -> ... -> Tn, we construct the tuple (Q0, Q1, ... Qn) where for each i, Qi is obtained from Ti by ignoring all predicates and quantification and replacing each tyvar by the symbol '?'. For example, for module M where foo :: forall b. Eq a => Set (Tree a) -> Tree ([a],b) -> [Tree (a,b)] we ignore the forall and Eq, and replace tyvars and tuple the results to get: M.(Set (Tree ?), Tree ( (,) ( [] ?) ?), [] (Tree ( (,) ? ?))).foo as the fully qualified reference to the entity we've just declared. If we call the tuple (Set, ...) the "ty-tuple", which specifies a space of values (ie something that each value is considered to "belong" to - the analogue of the object in OOP), then we can define a projection from a space into a containing space as follows: 1) Let Qi == Ui Si0 Si1 ... Sik be any element of a ty-tuple P. Then we can form a new ty-tuple P' by replacing Qi by Ui. 2) Let Qi be any element of a ty-tuple P of arity n+1. Then we can form P' == (Q0, ..., Qi-1, Qi+1, ... Qn) of arity n In both cases, we can use P' to qualify the identifier to get a value reference as long as this still has enough information for disambiguating other uses of the identifier in M. Applying these transformations of the ty-tuple to the example above, any of the following could be used as a partial qualification of foo in M: (Set Tree, Tree ([],?), [Tree]).foo (Set, Tree, []).foo Tree.foo foo Rule 2 allows us to propagate identifiers back up to their ancestor modules as long as there are no conflicts along the way. The type inference algorithm could then be modified (I hope) to use the top-level annotation for a value declaration to determine the entities that identifiers refer to, by searching in the appropriate value spaces determined by the types of the args and return value. label :: Tree a -> Int -> (Tree a, Int) label (Leaf x) i = (Leaf i, i+1) The identifier Leaf is resolved in the current namespace augmented by the namespace for module Tree, thus we don't have to explicitly write Tree.Leaf even though the declaration of label occurs outside the Tree module itself. (I suggest that top-level type annotations should be mandatory since without them one just drowns in a sea of TI confusion when there is a type error. By making them mandatory the TI algorithm could make real use of them to resolve identifier bindings as in OOP) Similarly: foo :: a -> Set a foo x = singleton x There is no need to say Set.singleton x, because we know that the result of foo has type Set a therefore we search in the current module augmented by the contents of the Set module (every type is also a module) for a binding for "singleton" which maps from a to Set a. Finally (apologies for this long post), returning to the use of ^ to allow an object oriented way of thinking consider: insert :: a -> Set a -> Set a ps = singleton 3 qs = insert 4 ps rs = ps^insert 4 When resolving "insert" used in the binding for rs, the compiler should see that we are looking for some function Set Int -> Int -> Set Int, and hence will be looking in the current module augmented by the Set module. However the Set module only has a binding for insert with type a -> Set a -> Set a. So the compiler should generate a new function insert' from insert by moving the first Set a arg to the front. Summary: 1) Every value binding belongs to a value space represented by a ty-tuple which abstracts away from the details of the actual type 2) The space of ty-tuples forms a lattice, and in particular this means qualification is optional when there are no conflicts (we can use Leaf 3 instead of Tree.Leaf 3), and we can use partial qualification to supply just the disambiguation info needed. 3) The TI algorithm should use the type of the expression (generated top-down from the top-level annotation) to search in the correct value spaces to resolve identifiers 4) Record field selection doesn't need any special scoping rules, and is just one example of a general object-oriented way of thinking about function application. 5) We can get all the advantages of automatic namespace management the OOP programmers take for granted, in functional programming, by using value spaces as the analogue of objects, and can thereby get rid of complicated import/export directives and improve code readability with less typing (but making more use of typing - excuse the pun :-)) I'm in the process of trying to implement a pre-processor for Haskell which would use the algorithms sketched above (as well as fixing a few other things I think are wrong with Haskell such as the way the current layout rule allows one to write code that would break if you replaced an identifier with one that had a different number of characters in it etc), so any feedback on these ideas would be welcome. Thanks for reading so far! Brian Hulley PS Everything above is purely intended for resolving the kind of ad-hoc overloading that is not amenable to treatment by type classes (which transforms some subset of the ad-hoc-overloaded functions which share the same shape into a single function with implicit dictionary arguments (in the usual implementation)).

5 16