
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_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�
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/beginners