On Thu, 2005-08-18 at 10:20 +0200, Andrej Bauer wrote: > Contrary to what skaller says, no inductive types are allowed in a > polynomial functor. This isn't contrary to what I said: I didn't say inductive types were allowed, I said the polynomial could be built *using* induction. EG: 1 is a list, if L is a list then T * L is a list. It follows T is a list, T * T is a list .. etc, and so a list is given by the polynomial 1 + T + T * T + T * T * T + ... I accept this may not be the most general definition. You said later: "Such types are well understood and have accompanying induction and recursion principles from which various operations (map, fold, etc.) can be built systematically." and I wonder why no production languages actually do that... -- John Skaller