Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. References for Tarski's High School Algebra Problem, was Re:
Cartesian Product in Standard Haskell Libraries (Jay Sulzberger)
2. Re: References for Tarski's High School Algebra Problem, was
Re: Cartesian Product in Standard Haskell Libraries (Kim-Ee Yeoh)
3. Re: References for Tarski's High School Algebra Problem, was
Re: Cartesian Product in Standard Haskell Libraries (Jay Sulzberger)
----------------------------------------------------------------------
Message: 1
Date: Tue, 25 Dec 2012 17:56:04 -0500 (EST)
From: Jay Sulzberger <[email protected]>
Subject: [Haskell-beginners] References for Tarski's High School
Algebra Problem, was Re: Cartesian Product in Standard Haskell
Libraries
To: beginners <[email protected]>
Message-ID: <[email protected]>
Content-Type: TEXT/PLAIN; charset=X-UNKNOWN; format=flowed
On Mon, 24 Dec 2012, Jay Sulzberger wrote:
>
>
> On Mon, 24 Dec 2012, Kim-Ee Yeoh <[email protected]> wrote:
>
>>> the result is of type [()] but for a cartesian n-product, you would like
>> [[a]]
>>
>> Right. So what we have here is a product over a count of 0 sets, which is
>> isomorphic to the function space that has the null set as domain. The
>> latter has exactly one element: the trivial function.
>>
>> My apologies for misreading what OP wrote:
>>
>>> This looks to me to be a violation of the rule that the Cartesian
>>> product of an empty list of lists is a list with one element in
>>> it.
>>
>> I thought he meant something along the lines of sequence ["","x"].
>>
>>
>> -- Kim-Ee
>
> Thanks, Kim-Ee!
>
> Your answer and also Chaddai's are very helpful.
>
> I hope to post more in this thread.
>
> oo--JS.
Kim-Ee, I started to write a response answering your first post
in this thread, but then I saw your second. My intended answer
started by defining some old classic functions, such as binary
append of lists, binary cartesian product of lists, binary + of
non-negative integers, binary * of non-negative integers, and
extending these four binary operations by using fold to get the
usual n-ary extensions of these four operations. Then I started
to list the most well known identities amongst the four
operations, and the four extended operations, including
identities using various functors defined using the fundamental
map card: FSets -> NNIntegers, where FSets is the collection of
finite sets, ah, this should be length: FLists -> NNIntegers
where FLists is the collection of finite lists and NNIntegers is
the set of non-negative integers. This morning, I realized I was
headed for a wonderful old problem, which we now see as a
question in New Crazy Types theory: Tarski's High School Algebra
Problem. Here is some stuff on the problem:
http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem
[page was last modified on 3 May 2012 at 07:37]
A note by John Baez which also gives some references:
http://math.ucr.edu/home/baez/week172.html
A paper by Roberto Di Cosmo and Thomas Dufour which proves that
Tarski High School Algebra is decidable but not finitely axiomatizable:
http://www.pps.univ-paris-diderot.fr/~dufour/zeronfa.pdf
Some notes from 1999 by R. Di Cosmo,
with pointer to his book on the problem:
http://www.dicosmo.org/Tarski/Tarski.html
A note by Thorsten Altenkirch on one of the dependent types case:
http://www.cs.nott.ac.uk/~txa/publ/unialg.pdf
R. Gurevic's 1985 paper, which is available for free:
http://www.ams.org/journals/proc/1985-094-01/S0002-9939-1985-0781071-1/
A note by S. N. Burris and K. A. Yeats on the history of the problem:
math.sfu.ca/~kya17/papers/saga_paper4.pdf
and here are some things on zero inputs in the lambda calculus,
one by Todd Trimble, one by John Baez, and one by Peter Selinger:
http://math.ucr.edu/home/baez/trimble/holodeck.html
http://math.ucr.edu/home/baez/week240.html
http://arxiv.org/pdf/1207.6972
oo--JS.
>
>
>>
>>
>> On Mon, Dec 24, 2012 at 4:42 PM, Chadda? Fouch?
>> <[email protected]>wrote:
>>
>>> On Mon, Dec 24, 2012 at 8:01 AM, Jay Sulzberger <[email protected]> wrote:
>>>>
>>>> > sequence []
>>>> []
>>>> it :: [()]
>>>>
>>>> This looks to me to be a violation of the rule that the Cartesian
>>>> product of an empty list of lists is a list with one element in
>>>> it. It looks to be a violation because "[]" looks like a name
>>>> for an empty list. But we also have
>>>>
>>>> > length (sequence [])
>>>> 1
>>>> it :: Int
>>>>
>>>> which almost reassures me.
>>>>
>>>
>>> Well the type of the first response is a dead give-away : the result
>>> is of type [()] but for a cartesian n-product, you would like [[a]]
>>> (with a maybe instantiated to a concrete type) ...
>>> What's happening here is that sequence is not "the cartesian
>>> n-product" in general, it is only that in the list monad but in
>>> "sequence []" there's nothing to indicate that we're in the list
>>> monad, so GHC default to the IO monad and unit () so sequence has the
>>> type "[IO ()] -> IO [()]" and there's no IO action in the list
>>> parameter, so there's nothing in the result list.
>>>
>>> Try :
>>>> sequence [] :: [[Int]]
>>> and you should be reassured.
>>>
>>> --
>>> Jeda?
>>>
>>> _______________________________________________
>>> Beginners mailing list
>>> [email protected]
>>> http://www.haskell.org/mailman/listinfo/beginners
>>>
>>
>
>
------------------------------
Message: 2
Date: Wed, 26 Dec 2012 12:05:08 +0700
From: Kim-Ee Yeoh <[email protected]>
Subject: Re: [Haskell-beginners] References for Tarski's High School
Algebra Problem, was Re: Cartesian Product in Standard Haskell
Libraries
To: Jay Sulzberger <[email protected]>
Cc: beginners <[email protected]>
Message-ID:
<capy+zds4qjvs-keppj2fmkkq0g5euip7zky7r-pxswr5dfc...@mail.gmail.com>
Content-Type: text/plain; charset="iso-8859-1"
Jay, I appreciate your references. I'm not sure whether you're asking a
question this time around.
I've skimmed some of Di Cosmo's work, and I particularly liked the type
isomorphism narrative as applied to a queryable database of functions.
Anyone who has used Hayoo or Hoogle enough encounters the problem of
non-canonicity of type signatures. Which of the following isomorphic
signatures should we search for
(a, Either a b) -> (s,c)
((a,a)->(s,c), (a,b)->(s,c))
(a->a->(s,c), a->b->(s,c))
(a->a->s, a->a->c, a->b->(s,c))
...
?
Cue Tarski's HSA problem.
-- Kim-Ee
On Wed, Dec 26, 2012 at 5:56 AM, Jay Sulzberger <[email protected]> wrote:
>
>
> On Mon, 24 Dec 2012, Jay Sulzberger wrote:
>
>
>>
>> On Mon, 24 Dec 2012, Kim-Ee Yeoh <[email protected]> wrote:
>>
>> the result is of type [()] but for a cartesian n-product, you would like
>>>>
>>> [[a]]
>>>
>>> Right. So what we have here is a product over a count of 0 sets, which is
>>> isomorphic to the function space that has the null set as domain. The
>>> latter has exactly one element: the trivial function.
>>>
>>> My apologies for misreading what OP wrote:
>>>
>>> This looks to me to be a violation of the rule that the Cartesian
>>>> product of an empty list of lists is a list with one element in
>>>> it.
>>>>
>>>
>>> I thought he meant something along the lines of sequence ["","x"].
>>>
>>>
>>> -- Kim-Ee
>>>
>>
>> Thanks, Kim-Ee!
>>
>> Your answer and also Chaddai's are very helpful.
>>
>> I hope to post more in this thread.
>>
>> oo--JS.
>>
>
> Kim-Ee, I started to write a response answering your first post
> in this thread, but then I saw your second. My intended answer
> started by defining some old classic functions, such as binary
> append of lists, binary cartesian product of lists, binary + of
> non-negative integers, binary * of non-negative integers, and
> extending these four binary operations by using fold to get the
> usual n-ary extensions of these four operations. Then I started
> to list the most well known identities amongst the four
> operations, and the four extended operations, including
> identities using various functors defined using the fundamental
> map card: FSets -> NNIntegers, where FSets is the collection of
> finite sets, ah, this should be length: FLists -> NNIntegers
> where FLists is the collection of finite lists and NNIntegers is
> the set of non-negative integers. This morning, I realized I was
> headed for a wonderful old problem, which we now see as a
> question in New Crazy Types theory: Tarski's High School Algebra
> Problem. Here is some stuff on the problem:
>
>
> http://en.wikipedia.org/wiki/**Tarski%27s_high_school_**algebra_problem<http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem>
> [page was last modified on 3 May 2012 at 07:37]
>
> A note by John Baez which also gives some references:
>
> http://math.ucr.edu/home/baez/**week172.html<http://math.ucr.edu/home/baez/week172.html>
>
> A paper by Roberto Di Cosmo and Thomas Dufour which proves that
> Tarski High School Algebra is decidable but not finitely axiomatizable:
>
> http://www.pps.univ-paris-**diderot.fr/~dufour/zeronfa.pdf<http://www.pps.univ-paris-diderot.fr/~dufour/zeronfa.pdf>
>
> Some notes from 1999 by R. Di Cosmo,
> with pointer to his book on the problem:
>
> http://www.dicosmo.org/Tarski/**Tarski.html<http://www.dicosmo.org/Tarski/Tarski.html>
>
> A note by Thorsten Altenkirch on one of the dependent types case:
>
> http://www.cs.nott.ac.uk/~txa/**publ/unialg.pdf<http://www.cs.nott.ac.uk/~txa/publ/unialg.pdf>
>
> R. Gurevic's 1985 paper, which is available for free:
> http://www.ams.org/journals/**proc/1985-094-01/S0002-9939-**
> 1985-0781071-1/<http://www.ams.org/journals/proc/1985-094-01/S0002-9939-1985-0781071-1/>
>
> A note by S. N. Burris and K. A. Yeats on the history of the problem:
>
> math.sfu.ca/~kya17/papers/**saga_paper4.pdf<http://math.sfu.ca/~kya17/papers/saga_paper4.pdf>
>
> and here are some things on zero inputs in the lambda calculus,
> one by Todd Trimble, one by John Baez, and one by Peter Selinger:
>
>
> http://math.ucr.edu/home/baez/**trimble/holodeck.html<http://math.ucr.edu/home/baez/trimble/holodeck.html>
>
>
> http://math.ucr.edu/home/baez/**week240.html<http://math.ucr.edu/home/baez/week240.html>
>
> http://arxiv.org/pdf/1207.6972
>
> oo--JS.
>
>
>
>>
>>
>>>
>>> On Mon, Dec 24, 2012 at 4:42 PM, Chadda? Fouch? <
>>> [email protected]>**wrote:
>>>
>>> On Mon, Dec 24, 2012 at 8:01 AM, Jay Sulzberger <[email protected]> wrote:
>>>>
>>>>>
>>>>> > sequence []
>>>>> []
>>>>> it :: [()]
>>>>>
>>>>> This looks to me to be a violation of the rule that the Cartesian
>>>>> product of an empty list of lists is a list with one element in
>>>>> it. It looks to be a violation because "[]" looks like a name
>>>>> for an empty list. But we also have
>>>>>
>>>>> > length (sequence [])
>>>>> 1
>>>>> it :: Int
>>>>>
>>>>> which almost reassures me.
>>>>>
>>>>>
>>>> Well the type of the first response is a dead give-away : the result
>>>> is of type [()] but for a cartesian n-product, you would like [[a]]
>>>> (with a maybe instantiated to a concrete type) ...
>>>> What's happening here is that sequence is not "the cartesian
>>>> n-product" in general, it is only that in the list monad but in
>>>> "sequence []" there's nothing to indicate that we're in the list
>>>> monad, so GHC default to the IO monad and unit () so sequence has the
>>>> type "[IO ()] -> IO [()]" and there's no IO action in the list
>>>> parameter, so there's nothing in the result list.
>>>>
>>>> Try :
>>>>
>>>>> sequence [] :: [[Int]]
>>>>>
>>>> and you should be reassured.
>>>>
>>>> --
>>>> Jeda?
>>>>
>>>> ______________________________**_________________
>>>> Beginners mailing list
>>>> [email protected]
>>>> http://www.haskell.org/**mailman/listinfo/beginners<http://www.haskell.org/mailman/listinfo/beginners>
>>>>
>>>>
>>>
>>
>>
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20121226/ba37654f/attachment-0001.htm>
------------------------------
Message: 3
Date: Wed, 26 Dec 2012 00:29:25 -0500 (EST)
From: Jay Sulzberger <[email protected]>
Subject: Re: [Haskell-beginners] References for Tarski's High School
Algebra Problem, was Re: Cartesian Product in Standard Haskell
Libraries
To: beginners <[email protected]>
Message-ID: <[email protected]>
Content-Type: TEXT/PLAIN; charset=X-UNKNOWN; format=flowed
On Wed, 26 Dec 2012, Kim-Ee Yeoh <[email protected]> wrote:
> Jay, I appreciate your references. I'm not sure whether you're asking a
> question this time around.
Thanks, Kim-Ee!
I was not directly asking a question in the post.
>
> I've skimmed some of Di Cosmo's work, and I particularly liked the type
> isomorphism narrative as applied to a queryable database of functions.
Yes. This is not stupid, and I had been thinking a bit about
such a thing before I saw Di Cosmo's stuff.
There was last semester a course at Columbia on "Big Data". I
never attended any of it but read Cathy O'Neil's blog posts about
it at
http://mathbabe.org
I thought that a good project for the class would be to attempt
to make a search engine for code. Now I'd want the search engine
to be able to classify two programs in two different programming
systems, say Basic and Scheme, or C and Haskell, as "being the
same program", even if their source code does not use the same
names for things. Of course, the general principle that gross
human language word similarities gets you a lot, will hold here
too. The interesting case would be if we stripped away all
comment, and surrounding text, and then tried to do the
grouping/indexing. Note that this does not, at least at first,
look like the sort of thing one does in, ah, econometrics, nor in
most computer helped "market research". I know that there has
been some work on the problem.
>
> Anyone who has used Hayoo or Hoogle enough encounters the problem of
> non-canonicity of type signatures. Which of the following isomorphic
> signatures should we search for
>
> (a, Either a b) -> (s,c)
> ((a,a)->(s,c), (a,b)->(s,c))
> (a->a->(s,c), a->b->(s,c))
> (a->a->s, a->a->c, a->b->(s,c))
I will have to read this carefully, but I know the general
problem ;)
> ...
>
> ?
>
> Cue Tarski's HSA problem.
Yes.
>
>
>
> -- Kim-Ee
I will attempt to post more, and this time I will put some
elementary, very elementary, Haskell code in, showing what GHCi
tells me about sequence just as you and Chaddai have said to do.
oo--JS.
>
>
> On Wed, Dec 26, 2012 at 5:56 AM, Jay Sulzberger <[email protected]> wrote:
>
>>
>>
>> On Mon, 24 Dec 2012, Jay Sulzberger wrote:
>>
>>
>>>
>>> On Mon, 24 Dec 2012, Kim-Ee Yeoh <[email protected]> wrote:
>>>
>>> the result is of type [()] but for a cartesian n-product, you would like
>>>>>
>>>> [[a]]
>>>>
>>>> Right. So what we have here is a product over a count of 0 sets, which is
>>>> isomorphic to the function space that has the null set as domain. The
>>>> latter has exactly one element: the trivial function.
>>>>
>>>> My apologies for misreading what OP wrote:
>>>>
>>>> This looks to me to be a violation of the rule that the Cartesian
>>>>> product of an empty list of lists is a list with one element in
>>>>> it.
>>>>>
>>>>
>>>> I thought he meant something along the lines of sequence ["","x"].
>>>>
>>>>
>>>> -- Kim-Ee
>>>>
>>>
>>> Thanks, Kim-Ee!
>>>
>>> Your answer and also Chaddai's are very helpful.
>>>
>>> I hope to post more in this thread.
>>>
>>> oo--JS.
>>>
>>
>> Kim-Ee, I started to write a response answering your first post
>> in this thread, but then I saw your second. My intended answer
>> started by defining some old classic functions, such as binary
>> append of lists, binary cartesian product of lists, binary + of
>> non-negative integers, binary * of non-negative integers, and
>> extending these four binary operations by using fold to get the
>> usual n-ary extensions of these four operations. Then I started
>> to list the most well known identities amongst the four
>> operations, and the four extended operations, including
>> identities using various functors defined using the fundamental
>> map card: FSets -> NNIntegers, where FSets is the collection of
>> finite sets, ah, this should be length: FLists -> NNIntegers
>> where FLists is the collection of finite lists and NNIntegers is
>> the set of non-negative integers. This morning, I realized I was
>> headed for a wonderful old problem, which we now see as a
>> question in New Crazy Types theory: Tarski's High School Algebra
>> Problem. Here is some stuff on the problem:
>>
>>
>> http://en.wikipedia.org/wiki/**Tarski%27s_high_school_**algebra_problem<http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem>
>> [page was last modified on 3 May 2012 at 07:37]
>>
>> A note by John Baez which also gives some references:
>>
>> http://math.ucr.edu/home/baez/**week172.html<http://math.ucr.edu/home/baez/week172.html>
>>
>> A paper by Roberto Di Cosmo and Thomas Dufour which proves that
>> Tarski High School Algebra is decidable but not finitely axiomatizable:
>>
>> http://www.pps.univ-paris-**diderot.fr/~dufour/zeronfa.pdf<http://www.pps.univ-paris-diderot.fr/~dufour/zeronfa.pdf>
>>
>> Some notes from 1999 by R. Di Cosmo,
>> with pointer to his book on the problem:
>>
>> http://www.dicosmo.org/Tarski/**Tarski.html<http://www.dicosmo.org/Tarski/Tarski.html>
>>
>> A note by Thorsten Altenkirch on one of the dependent types case:
>>
>> http://www.cs.nott.ac.uk/~txa/**publ/unialg.pdf<http://www.cs.nott.ac.uk/~txa/publ/unialg.pdf>
>>
>> R. Gurevic's 1985 paper, which is available for free:
>> http://www.ams.org/journals/**proc/1985-094-01/S0002-9939-**
>> 1985-0781071-1/<http://www.ams.org/journals/proc/1985-094-01/S0002-9939-1985-0781071-1/>
>>
>> A note by S. N. Burris and K. A. Yeats on the history of the problem:
>>
>> math.sfu.ca/~kya17/papers/**saga_paper4.pdf<http://math.sfu.ca/~kya17/papers/saga_paper4.pdf>
>>
>> and here are some things on zero inputs in the lambda calculus,
>> one by Todd Trimble, one by John Baez, and one by Peter Selinger:
>>
>>
>> http://math.ucr.edu/home/baez/**trimble/holodeck.html<http://math.ucr.edu/home/baez/trimble/holodeck.html>
>>
>>
>> http://math.ucr.edu/home/baez/**week240.html<http://math.ucr.edu/home/baez/week240.html>
>>
>> http://arxiv.org/pdf/1207.6972
>>
>> oo--JS.
>>
>>
>>
>>>
>>>
>>>>
>>>> On Mon, Dec 24, 2012 at 4:42 PM, Chadda? Fouch? <
>>>> [email protected]>**wrote:
>>>>
>>>> On Mon, Dec 24, 2012 at 8:01 AM, Jay Sulzberger <[email protected]> wrote:
>>>>>
>>>>>>
>>>>>> > sequence []
>>>>>> []
>>>>>> it :: [()]
>>>>>>
>>>>>> This looks to me to be a violation of the rule that the Cartesian
>>>>>> product of an empty list of lists is a list with one element in
>>>>>> it. It looks to be a violation because "[]" looks like a name
>>>>>> for an empty list. But we also have
>>>>>>
>>>>>> > length (sequence [])
>>>>>> 1
>>>>>> it :: Int
>>>>>>
>>>>>> which almost reassures me.
>>>>>>
>>>>>>
>>>>> Well the type of the first response is a dead give-away : the result
>>>>> is of type [()] but for a cartesian n-product, you would like [[a]]
>>>>> (with a maybe instantiated to a concrete type) ...
>>>>> What's happening here is that sequence is not "the cartesian
>>>>> n-product" in general, it is only that in the list monad but in
>>>>> "sequence []" there's nothing to indicate that we're in the list
>>>>> monad, so GHC default to the IO monad and unit () so sequence has the
>>>>> type "[IO ()] -> IO [()]" and there's no IO action in the list
>>>>> parameter, so there's nothing in the result list.
>>>>>
>>>>> Try :
>>>>>
>>>>>> sequence [] :: [[Int]]
>>>>>>
>>>>> and you should be reassured.
>>>>>
>>>>> --
>>>>> Jeda?
>>>>>
>>>>> ______________________________**_________________
>>>>> Beginners mailing list
>>>>> [email protected]
>>>>> http://www.haskell.org/**mailman/listinfo/beginners<http://www.haskell.org/mailman/listinfo/beginners>
>>>>>
>>>>>
>>>>
>>>
>>>
>>
>> _______________________________________________
>> Beginners mailing list
>> [email protected]
>> http://www.haskell.org/mailman/listinfo/beginners
>>
>>
>
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 54, Issue 44
*****************************************
