Whoosh? :-) On Sun, Apr 1, 2012 at 3:54 PM, Greg Weber <g...@gregweber.info> 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 <gersh...@gmail.com> 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? > > > > aaaa aaaaa a aa = aaaaa{a = a, aaa = aa} > > > > Using standard Haskell typeclasses this is a difficult question to > > answer. The types of aaaa 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 homotopies? At first, I thought > > we could avoid providing any syntax for homotopies at all. Haskell is > > a language with type inference, so we should just be able to infer > > paths and homotopies behind the scenes by adding homotopies to the > > type system. That's a very nice answer in theory. But in the real > > world, when we're writing code that solves actual problems, > > theoretical niceties break down. What if a user wants to use a > > nonstandard homotopy? > > > > Why should we stop them just because we're too lazy to come up with a > > good syntax? I then realized that we keep running out of syntax > > because we've limited ourselves to unicode. Instead, I propose we add > > a potentially infinite universe of identifiers: youtube videos. For > > example, the higher inductive type for a circle can be written as: > > > > homotopyType http://www.youtube.com/watch?v=dQw4w9WgXcQ where > > Base ::: http://www.youtube.com/watch?v=dQw4w9WgXcQ > > Loop ::: http://www.youtube.com/watch?v=J---aiyznGQ Base Base > > > > Note that the urls do not use SSL. For portability reasons, I propose > > that SSL only be enabled as an optional extension. > > > > _______________________________________________ > > Glasgow-haskell-users mailing list > > glasgow-haskell-us...@haskell.org > > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Gregory Collins <g...@gregorycollins.net>
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe