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:  20050818 (08:20) 
From:  Andrej Bauer <Andrej.Bauer@a...> 
Subject:  Re: [Camllist] Snd question 
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 fixedpoint equation, t = F(t) for some functor F. In case F is a polynomial functor, the inductive type t is called a wtype, or a wellfounded 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