Re: Potential GSoC proposal: Reduce the speed gap between 'ghc -c' and 'ghc --make'

2012-04-01 Thread Evan Laforge
> 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'

2012-04-01 Thread Mikhail Glushenkov
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

2012-04-01 Thread Christopher Done
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

2012-04-01 Thread Greg Weber
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

2012-04-01 Thread Greg Weber
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