oleg@pobox.com wrote:
Jonathan Cast wrote:
<snip>
No. You can't define most initial models without recursive (or inductive) data types in general, because initial models are defined inductively.
<snip>
You can't define head, tail, or foldr using the MonadPlus signature (how would you define them for e.g. a backtracking parser?), which is why you do need recursive types for []
However surprising might it seem, you _can_ define head, tail, and foldr for an implementation of a backtracking transformer that it is not a list and uses no recursive (or inductive) types. In fact, it is possible to define list final algebra (complete with head and tail) in a language without recursive datatypes, only with the higher-rank one. The msplit contraption of the LogicT paper was `null', `head', and `tail' all in one. The paper specifically made a point that msplit can be defined without help from recursive data types. The brief summary of that derivation is a note `How to take a TAIL of a functional stream'
http://pobox.com/~oleg/ftp/Computation/Continuations.html#cdr-fstream
The higher-rank type is needed only to express the polymorphic answertype.
OK. Right. I forgot about the Church encoding. Bad jcast, no cookie. Jon Cast