Snd question
[
Home
]
[ Index:
by date

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