Re: [Caml-list] Snd question

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

skaller wrote:
> Jay's Functorial ML describes how to do this properly: 
> map, fold, etc, can be applied to any
> polynomial type (a type built out of sums, products,
> and induction). This is polyadic = functorially polymorphic,
> not ad hoc.

Just a minor terminological remark:

A polynomial functor (functor in the sense of category theory) is
a functor built from sums, products, arrow types and type constants,
where the lhs of an arrow must be constant, e.g.

  P(x) = a * x + (b -> x) + c

Contrary to what skaller says, no inductive types are allowed in a
polynomial functor. Side remark: the fully general definition of a
polynomial functor allows an arbitrary dependend sum, not just a finite
one, so we get the general form P(x) = sum_{y : a} (b(y) -> x), where b
is a type dependent on a.

An inductive type is the initial solution to a fixed-point equation,

 t = F(t)

for some functor F. In case F is a polynomial functor, the inductive
type t is called a w-type, or a well-founded type. Such types are well
understood and have accompanying induction and recursion principles from
which various operations (map, fold, etc.) can be built systematically.

Best regards,

Andrej