Whoosh? :-)<br><br><div class="gmail_quote">On Sun, Apr 1, 2012 at 3:54 PM, Greg Weber <span dir="ltr"><<a href="mailto:greg@gregweber.info">greg@gregweber.info</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Gershom,<br>
<br>
This sounds very interesting even if I have no idea what you are<br>
talking about :)<br>
Please create a proposal linked from this page:<br>
<a href="http://hackage.haskell.org/trac/ghc/wiki/Records" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/Records</a><br>
The first thing you should probably do is explain the programmer's<br>
point of view. That ensures that we are all going through the<br>
requirements phase correctly.<br>
I can assure you that haskell prime would not accept a records change<br>
until it is first implemented in GHC or another Haskell compiler.<br>
<br>
Thanks,<br>
Greg Weber<br>
<div><div class="h5"><br>
On Sat, Mar 31, 2012 at 11:14 PM, Gershom B <<a href="mailto:gershomb@gmail.com">gershomb@gmail.com</a>> wrote:<br>
> The records discussion has been really complicated and confusing. But<br>
> I have a suggestion that should provide a great deal of power to<br>
> records, while being mostly[1] backwards-compatible with Haskell 2010.<br>
> Consider this example:<br>
><br>
> data A a = A{a:a, aa::a, aaa :: a -> A (a -> a)}<br>
> data B a = B{aaa :: a -> A (a -> a), a :: A}<br>
><br>
> Now what is the type of this?<br>
><br>
> aaaa aaaaa a aa = aaaaa{a = a, aaa = aa}<br>
><br>
> Using standard Haskell typeclasses this is a difficult question to<br>
> answer. The types of aaaa for A and B do not unify in an obvious way.<br>
> However, while they are intensionally quite distinct, they unify<br>
> trivially extensionally. The obvious thing to do is then to extend the<br>
> type system with extensional equality on record functions.<br>
><br>
> Back when Haskell was invented, extensional equality was thought to be<br>
> hard. But purity was thought to be hard too, and so were Monads. Now,<br>
> we know that function existentionality is easy. In fact, if we add the<br>
> Univalence Axiom to GHC[2], then this is enough to get function<br>
> existensionality. This is a well-known result of Homotopy Type<br>
> Theory[3], which is a well-explored approach that has existed for at<br>
> least a few years and produced more than one paper[4]. Homotopy Type<br>
> Theory is so sound and well understood that it has even been<br>
> formalized in Coq.<br>
><br>
> Once we extend GHC with homotopies, it turns out that records reduce<br>
> to mere syntactic sugar, and there is a natural proof of their<br>
> soundness (Appendix A). Furthermore, there is a canonical projection<br>
> for any group of fields (Appendix B). Even better, we can make "."<br>
> into the identity path operator, unifying its uses in composition and<br>
> projection. In fact, with extended (parenthesis-free) section rules,<br>
> "." can also be used to terminate expressions, making Haskell friendly<br>
> not only to programmers coming from Java, but also to those coming<br>
> from Prolog!<br>
><br>
> After some initial feedback, I'm going to create a page for the<br>
> Homotopy Extensional Records Proposal (HERP) on trac. There are really<br>
> only a few remaining questions. 1) Having introduced homotopies, why<br>
> not go all the way and introduce dependent records? In fact, are HERP<br>
> and Dependent Extensional Records Proposal (DERP) already isomorphic?<br>
> My suspicion is that HERP is isomorphic, but DERP is not. However, I<br>
> can only get away with my proof using Scott-free semantics. 2) Which<br>
> trac should I post this too? Given how well understood homotopy type<br>
> theory is, I'm tempted to bypass GHC entirely and propose this for<br>
> haskell-prime. 3) What syntax should we use to represent homotopies?<br>
> See extend discussion in Appendix C.<br>
><br>
> HTH HAND,<br>
> Gershom<br>
><br>
> [1] To be precise, 100% of Haskell 2010 programs should, usually, be<br>
> able to be rewritten to work with this proposal with a minimal set of<br>
> changes[1a].<br>
><br>
> [1a] A minimal set of changes is defined as the smallest set of<br>
> changes necessary to make to a Haskell 2010 program such that it works<br>
> with this proposal. We can arrive at these changes by the following<br>
> procedure: 1) Pick a change[1b]. 2) Is it minimal? If so keep it. 3)<br>
> are we done? If not, make another change.<br>
><br>
> [1b] To do this constructively, we need an order. I suggest the lo<br>
> mein, since noodles give rise to a free soda.<br>
><br>
> [2] I haven't looked at the source, but I would suggest putting it in<br>
> the file Axioms.hs.<br>
><br>
> [3] <a href="http://homotopytypetheory.org/" target="_blank">http://homotopytypetheory.org/</a><br>
><br>
> [4] <a href="http://arxiv.org/" target="_blank">http://arxiv.org/</a><br>
><br>
><br>
> *Appendix A: A Natural Proof of the Soundness of HERP<br>
><br>
> Take the category of all types in HERP, with functions as morphisms.<br>
> Call it C. Take the category of all sound expressions in HERP, with<br>
> functions as morphisms. Call it D. Define a full functor from C to D.<br>
> Call it F. Define a faithful functor on C and D. Call it G. Draw the<br>
> following diagram.<br>
><br>
> F(X)----F(Y)<br>
> | |<br>
> | |<br>
> | |<br>
> G(X)----G(Y)<br>
><br>
> Define the arrows such that everything commutes.<br>
><br>
><br>
> *Appendix B: Construction of a Canonical Projection for Any Group of Fields.<br>
><br>
> 1) Take the fields along the homotopy to an n-ball.<br>
> 2) Pack them loosely with newspaper and gunpowder.<br>
> 3) Project them from a cannon.<br>
><br>
> In an intuitionistic logic, the following simplification is possible:<br>
><br>
> 1) Use your intuition.<br>
><br>
><br>
> *Appendix C: Homotopy Syntax<br>
><br>
> Given that we already are using the full unicode set, what syntax<br>
> should we use to distinguish paths and homotopies? At first, I thought<br>
> we could avoid providing any syntax for homotopies at all. Haskell is<br>
> a language with type inference, so we should just be able to infer<br>
> paths and homotopies behind the scenes by adding homotopies to the<br>
> type system. That's a very nice answer in theory. But in the real<br>
> world, when we're writing code that solves actual problems,<br>
> theoretical niceties break down. What if a user wants to use a<br>
> nonstandard homotopy?<br>
><br>
> Why should we stop them just because we're too lazy to come up with a<br>
> good syntax? I then realized that we keep running out of syntax<br>
> because we've limited ourselves to unicode. Instead, I propose we add<br>
> a potentially infinite universe of identifiers: youtube videos. For<br>
> example, the higher inductive type for a circle can be written as:<br>
><br>
> homotopyType <a href="http://www.youtube.com/watch?v=dQw4w9WgXcQ" target="_blank">http://www.youtube.com/watch?v=dQw4w9WgXcQ</a> where<br>
> Base ::: <a href="http://www.youtube.com/watch?v=dQw4w9WgXcQ" target="_blank">http://www.youtube.com/watch?v=dQw4w9WgXcQ</a><br>
> Loop ::: <a href="http://www.youtube.com/watch?v=J---aiyznGQ" target="_blank">http://www.youtube.com/watch?v=J---aiyznGQ</a> Base Base<br>
><br>
> Note that the urls do not use SSL. For portability reasons, I propose<br>
> that SSL only be enabled as an optional extension.<br>
><br>
> _______________________________________________<br>
</div></div>> Glasgow-haskell-users mailing list<br>
> <a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br>Gregory Collins <<a href="mailto:greg@gregorycollins.net" target="_blank">greg@gregorycollins.net</a>><br>