On Mon, 24 Dec 2012, Jay Sulzberger wrote:
On Mon, 24 Dec 2012, Kim-Ee Yeoh <ky3@atamo.com> 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é <chaddai.fouche@gmail.com>wrote:
On Mon, Dec 24, 2012 at 8:01 AM, Jay Sulzberger <jays@panix.com> 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
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://www.haskell.org/mailman/listinfo/beginners