Re: [Haskell-beginners] References for Tarski's High School Algebra Problem, was Re: Cartesian Product in Standard Haskell Libraries

26 Dec 2012

      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  wrote:
...
On Mon, 24 Dec 2012, Jay Sulzberger wrote:
...
On Mon, 24 Dec 2012, Kim-Ee Yeoh  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_problemhttp://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.htmlhttp://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.pdfhttp://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.htmlhttp://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.pdfhttp://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.pdfhttp://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.htmlhttp://math.ucr.edu/home/baez/trimble/holodeck.html
http://math.ucr.edu/home/baez/**week240.htmlhttp://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é <
chaddai.fouche@gmail.com>**wrote:
On Mon, Dec 24, 2012 at 8:01 AM, Jay Sulzberger  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
Beginners@haskell.org
http://www.haskell.org/**mailman/listinfo/beginnershttp://www.haskell.org/mailman/listinfo/beginners
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://www.haskell.org/mailman/listinfo/beginners