Re: [Caml-list] Snd question

[Andrej Bauer <Andrej.Bauer@andrej.com>]

I was hoping skaller wouldn't object to a simple terminological point.
Oh well :-)

skaller wrote:
> 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 + ...

You are confusing the interesting observation that lists can be given
both as an inductive type and a polynomial with the definition of
polynomial functors. Polynomial functors are defined without mention of
inductive types (contrary to your _definition_). Since we are discussing
a _definition_, it is irrelevant that there are inductive types which
can also be expressed as polynomial functors. If you do not believe me,
I can give you a reference.

> "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...

I believe the coq proof assistant (http://coq.inria.fr/) knows how to do
this, and quite possibly the Isabelle theorem prover, too. One could
presumably rip out this part of coq and put it in a programming language.

Best regards,

Andrej