Re: Potential GSoC proposal: Reduce the speed gap between 'ghc -c' and 'ghc --make'
> Questions: > > Would implementing this optimisation be a worthwhile/realistic GSoC project? > What are other potential ways to bring 'ghc -c' performance up to par > with 'ghc --make'? I implemented a ghc server that runs several persistent ghcs, and distributes compiles among them. It seemed to work, but the speed gains weren't what I'd hoped for. But perhaps I was doing something dumb that hurt performance. I'd be happy to upload the source if you're interested. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Potential GSoC proposal: Reduce the speed gap between 'ghc -c' and 'ghc --make'
Hi all, [Hoping it's not too late.] During my work on parallelising 'ghc --make' [1] I encountered a stumbling block: running 'ghc --make' can be often much faster than using separate compile ('ghc -c') and link stages, which means that any parallel build tool built on top of 'ghc -c' will be significantly handicapped [2]. As far as I understand, this is mainly due to the effects of interface file caching - 'ghc --make' only needs to parse and load them once. One potential improvement (suggested by Duncan Coutts [3]) is to produce whole-package interface files and load them in using mmap(). Questions: Would implementing this optimisation be a worthwhile/realistic GSoC project? What are other potential ways to bring 'ghc -c' performance up to par with 'ghc --make'? [1] https://github.com/23Skidoo/ghc-parmake [2] https://gist.github.com/1360470 [3] http://www.reddit.com/r/haskell/comments/qwj5j/the_cabal_of_my_dreams/c41a5gx -- () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] A Modest Records Proposal
I actually read the first couple paragraphs and thought “sounds interesting I'll read it later”. After reading it properly, I lol'd. > After some initial feedback, I'm going to create a page for the > Homotopy Extensional Records Proposal (HERP) on trac. There are really > only a few remaining questions. 1) Having introduced homotopies, why > not go all the way and introduce dependent records? In fact, are HERP > and Dependent Extensional Records Proposal (DERP) already isomorphic? > My suspicion is that HERP is isomorphic, but DERP is not. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] A Modest Records Proposal
Obviously Gregory is not familiar with Homotopy. In fact, its isomorphism predicts that if someone named Greg is involved in a discussion, someone named Gregory will also become involved. Or that is what I get for responding to an e-mail without reading it on April 1st :) On Sun, Apr 1, 2012 at 7:40 AM, Gregory Collins wrote: > Whoosh? :-) > > On Sun, Apr 1, 2012 at 3:54 PM, Greg Weber wrote: >> >> Hi Gershom, >> >> This sounds very interesting even if I have no idea what you are >> talking about :) >> Please create a proposal linked from this page: >> http://hackage.haskell.org/trac/ghc/wiki/Records >> The first thing you should probably do is explain the programmer's >> point of view. That ensures that we are all going through the >> requirements phase correctly. >> I can assure you that haskell prime would not accept a records change >> until it is first implemented in GHC or another Haskell compiler. >> >> Thanks, >> Greg Weber >> >> On Sat, Mar 31, 2012 at 11:14 PM, Gershom B wrote: >> > The records discussion has been really complicated and confusing. But >> > I have a suggestion that should provide a great deal of power to >> > records, while being mostly[1] backwards-compatible with Haskell 2010. >> > Consider this example: >> > >> > data A a = A{a:a, aa::a, aaa :: a -> A (a -> a)} >> > data B a = B{aaa :: a -> A (a -> a), a :: A} >> > >> > Now what is the type of this? >> > >> > a a aa = a{a = a, aaa = aa} >> > >> > Using standard Haskell typeclasses this is a difficult question to >> > answer. The types of for A and B do not unify in an obvious way. >> > However, while they are intensionally quite distinct, they unify >> > trivially extensionally. The obvious thing to do is then to extend the >> > type system with extensional equality on record functions. >> > >> > Back when Haskell was invented, extensional equality was thought to be >> > hard. But purity was thought to be hard too, and so were Monads. Now, >> > we know that function existentionality is easy. In fact, if we add the >> > Univalence Axiom to GHC[2], then this is enough to get function >> > existensionality. This is a well-known result of Homotopy Type >> > Theory[3], which is a well-explored approach that has existed for at >> > least a few years and produced more than one paper[4]. Homotopy Type >> > Theory is so sound and well understood that it has even been >> > formalized in Coq. >> > >> > Once we extend GHC with homotopies, it turns out that records reduce >> > to mere syntactic sugar, and there is a natural proof of their >> > soundness (Appendix A). Furthermore, there is a canonical projection >> > for any group of fields (Appendix B). Even better, we can make "." >> > into the identity path operator, unifying its uses in composition and >> > projection. In fact, with extended (parenthesis-free) section rules, >> > "." can also be used to terminate expressions, making Haskell friendly >> > not only to programmers coming from Java, but also to those coming >> > from Prolog! >> > >> > After some initial feedback, I'm going to create a page for the >> > Homotopy Extensional Records Proposal (HERP) on trac. There are really >> > only a few remaining questions. 1) Having introduced homotopies, why >> > not go all the way and introduce dependent records? In fact, are HERP >> > and Dependent Extensional Records Proposal (DERP) already isomorphic? >> > My suspicion is that HERP is isomorphic, but DERP is not. However, I >> > can only get away with my proof using Scott-free semantics. 2) Which >> > trac should I post this too? Given how well understood homotopy type >> > theory is, I'm tempted to bypass GHC entirely and propose this for >> > haskell-prime. 3) What syntax should we use to represent homotopies? >> > See extend discussion in Appendix C. >> > >> > HTH HAND, >> > Gershom >> > >> > [1] To be precise, 100% of Haskell 2010 programs should, usually, be >> > able to be rewritten to work with this proposal with a minimal set of >> > changes[1a]. >> > >> > [1a] A minimal set of changes is defined as the smallest set of >> > changes necessary to make to a Haskell 2010 program such that it works >> > with this proposal. We can arrive at these changes by the following >> > procedure: 1) Pick a change[1b]. 2) Is it minimal? If so keep it. 3) >> > are we done? If not, make another change. >> > >> > [1b] To do this constructively, we need an order. I suggest the lo >> > mein, since noodles give rise to a free soda. >> > >> > [2] I haven't looked at the source, but I would suggest putting it in >> > the file Axioms.hs. >> > >> > [3] http://homotopytypetheory.org/ >> > >> > [4] http://arxiv.org/ >> > >> > >> > *Appendix A: A Natural Proof of the Soundness of HERP >> > >> > Take the category of all types in HERP, with functions as morphisms. >> > Call it C. Take the category of all sound expressions in HERP, with >> > functions as morphisms. Call it D. Define a full functor from C to D. >> > Call it F. D
Re: A Modest Records Proposal
Hi Gershom, This sounds very interesting even if I have no idea what you are talking about :) Please create a proposal linked from this page: http://hackage.haskell.org/trac/ghc/wiki/Records The first thing you should probably do is explain the programmer's point of view. That ensures that we are all going through the requirements phase correctly. I can assure you that haskell prime would not accept a records change until it is first implemented in GHC or another Haskell compiler. Thanks, Greg Weber On Sat, Mar 31, 2012 at 11:14 PM, Gershom B wrote: > The records discussion has been really complicated and confusing. But > I have a suggestion that should provide a great deal of power to > records, while being mostly[1] backwards-compatible with Haskell 2010. > Consider this example: > > data A a = A{a:a, aa::a, aaa :: a -> A (a -> a)} > data B a = B{aaa :: a -> A (a -> a), a :: A} > > Now what is the type of this? > > a a aa = a{a = a, aaa = aa} > > Using standard Haskell typeclasses this is a difficult question to > answer. The types of for A and B do not unify in an obvious way. > However, while they are intensionally quite distinct, they unify > trivially extensionally. The obvious thing to do is then to extend the > type system with extensional equality on record functions. > > Back when Haskell was invented, extensional equality was thought to be > hard. But purity was thought to be hard too, and so were Monads. Now, > we know that function existentionality is easy. In fact, if we add the > Univalence Axiom to GHC[2], then this is enough to get function > existensionality. This is a well-known result of Homotopy Type > Theory[3], which is a well-explored approach that has existed for at > least a few years and produced more than one paper[4]. Homotopy Type > Theory is so sound and well understood that it has even been > formalized in Coq. > > Once we extend GHC with homotopies, it turns out that records reduce > to mere syntactic sugar, and there is a natural proof of their > soundness (Appendix A). Furthermore, there is a canonical projection > for any group of fields (Appendix B). Even better, we can make "." > into the identity path operator, unifying its uses in composition and > projection. In fact, with extended (parenthesis-free) section rules, > "." can also be used to terminate expressions, making Haskell friendly > not only to programmers coming from Java, but also to those coming > from Prolog! > > After some initial feedback, I'm going to create a page for the > Homotopy Extensional Records Proposal (HERP) on trac. There are really > only a few remaining questions. 1) Having introduced homotopies, why > not go all the way and introduce dependent records? In fact, are HERP > and Dependent Extensional Records Proposal (DERP) already isomorphic? > My suspicion is that HERP is isomorphic, but DERP is not. However, I > can only get away with my proof using Scott-free semantics. 2) Which > trac should I post this too? Given how well understood homotopy type > theory is, I'm tempted to bypass GHC entirely and propose this for > haskell-prime. 3) What syntax should we use to represent homotopies? > See extend discussion in Appendix C. > > HTH HAND, > Gershom > > [1] To be precise, 100% of Haskell 2010 programs should, usually, be > able to be rewritten to work with this proposal with a minimal set of > changes[1a]. > > [1a] A minimal set of changes is defined as the smallest set of > changes necessary to make to a Haskell 2010 program such that it works > with this proposal. We can arrive at these changes by the following > procedure: 1) Pick a change[1b]. 2) Is it minimal? If so keep it. 3) > are we done? If not, make another change. > > [1b] To do this constructively, we need an order. I suggest the lo > mein, since noodles give rise to a free soda. > > [2] I haven't looked at the source, but I would suggest putting it in > the file Axioms.hs. > > [3] http://homotopytypetheory.org/ > > [4] http://arxiv.org/ > > > *Appendix A: A Natural Proof of the Soundness of HERP > > Take the category of all types in HERP, with functions as morphisms. > Call it C. Take the category of all sound expressions in HERP, with > functions as morphisms. Call it D. Define a full functor from C to D. > Call it F. Define a faithful functor on C and D. Call it G. Draw the > following diagram. > > F(X)F(Y) > | | > | | > | | > G(X)G(Y) > > Define the arrows such that everything commutes. > > > *Appendix B: Construction of a Canonical Projection for Any Group of Fields. > > 1) Take the fields along the homotopy to an n-ball. > 2) Pack them loosely with newspaper and gunpowder. > 3) Project them from a cannon. > > In an intuitionistic logic, the following simplification is possible: > > 1) Use your intuition. > > > *Appendix C: Homotopy Syntax > > Given that we already are using the full unicode set, what syntax > should we use to distinguish paths and homotopi