Quantcast

A Modest Records Proposal

classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

A Modest Records Proposal

Gershom Bazerman
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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

Gregory Collins-3
Whoosh? :-)

On Sun, Apr 1, 2012 at 3:54 PM, Greg Weber <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



--
Gregory Collins <[hidden email]>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

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 <[hidden email]> wrote:

> Whoosh? :-)
>
> On Sun, Apr 1, 2012 at 3:54 PM, Greg Weber <[hidden email]> 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 <[hidden email]> 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
>> > [hidden email]
>> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
>
>
> --
> Gregory Collins <[hidden email]>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

Alp Mestanogullari
Lesson learned: for next year, write a Haskell program that tells if a given -cafe thread or reddit discussion is a April Fool's joke or not.

On Sun, Apr 1, 2012 at 7:10 PM, Christopher Done <[hidden email]> wrote:
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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



--
Alp Mestanogullari

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

Michael Snoyman
On Mon, Apr 2, 2012 at 3:38 PM, Alp Mestanogullari <[hidden email]> wrote:
> Lesson learned: for next year, write a Haskell program that tells if a given
> -cafe thread or reddit discussion is a April Fool's joke or not.

import Data.Time

main = do
    now <- getCurrentTime
    let (_, month, day) = toGregorian $ utctDay now
    putStrLn $
        if month == 4 && day == 1
            then "It's a joke"
            else "It's real"

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

Christopher Done
On 2 April 2012 14:41, Michael Snoyman <[hidden email]> wrote:
> import Data.Time
>
> main = do
>    now <- getCurrentTime
>    let (_, month, day) = toGregorian $ utctDay now
>    putStrLn $
>        if month == 4 && day == 1
>            then "It's a joke"
>            else "It's real"

import Data.Time
main = do
   now <- getCurrentTime
   let (_, month, day) = toGregorian $ utctDay now
   putStrLn $
       if month == 4 && day == 1
           then "It's a joke"
           else "It's real. (This output is not a joke. But run this
program again to be sure.)"

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

Evan Laforge
In reply to this post by Michael Snoyman
On Mon, Apr 2, 2012 at 5:41 AM, Michael Snoyman <[hidden email]> wrote:

> On Mon, Apr 2, 2012 at 3:38 PM, Alp Mestanogullari <[hidden email]> wrote:
>> Lesson learned: for next year, write a Haskell program that tells if a given
>> -cafe thread or reddit discussion is a April Fool's joke or not.
>
> import Data.Time
>
> main = do
>    now <- getCurrentTime
>    let (_, month, day) = toGregorian $ utctDay now
>    putStrLn $
>        if month == 4 && day == 1
>            then "It's a joke"
>            else "It's real"

My strategy next year will be to not read any email on the 1st.  I'll
just wait until the 2nd to read it all.  Foolproof!

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: A Modest Records Proposal

Kyle Murphy-2
On Mon, Apr 2, 2012 at 16:30, Evan Laforge <[hidden email]> wrote:
> On Mon, Apr 2, 2012 at 5:41 AM, Michael Snoyman <[hidden email]> wrote:
>> On Mon, Apr 2, 2012 at 3:38 PM, Alp Mestanogullari <[hidden email]> wrote:
>>> Lesson learned: for next year, write a Haskell program that tells if a given
>>> -cafe thread or reddit discussion is a April Fool's joke or not.
>>
>> import Data.Time
>>
>> main = do
>>    now <- getCurrentTime
>>    let (_, month, day) = toGregorian $ utctDay now
>>    putStrLn $
>>        if month == 4 && day == 1
>>            then "It's a joke"
>>            else "It's real"
>
> My strategy next year will be to not read any email on the 1st.  I'll
> just wait until the 2nd to read it all.  Foolproof!

Hmm, nope, still failed. I was following along until it got to HERP at which point I scrolled back up to see that it was sent on the 1st and then continued to read and LOL.

-R. Kyle Murphy
--
Curiosity was framed, Ignorance killed the cat.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Loading...