A Modest Records Proposal

[Ben Franksen]

ROTFL!

Ben

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?
> 
>     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.