Version française
Home     About     Download     Resources     Contact us    
Browse thread
Snd question
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Andrej Bauer <Andrej.Bauer@a...>
Subject: Re: [Caml-list] Snd question
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