[Prev][Next][Index][Thread]

Non Strictly Positive Datatypes in System F



Non Strictly Positive Datatypes for Breadth First Search
--------------------------------------------------------

It is known that in system F weak initial T-algebras for any
internally describable functor exist. For example natural numbers,
lists and trees can be coded that way. However, not only these
"algebraic" datatypes exist, but also the somewhat pathological ones
whose signature contains the recursive type variable in a doubly
negated position. An example is the following datatype

datatype R = C of (R->bool)->bool

or in system F

R = All C. (((C->bool)->bool)->C) -> C

where 

bool = All C. (C->C)->C

which Reynolds and Plotkin [ReyPlo] use in their proof of the
nonexistence of set-theoretic models for system F.

It seems to be widely believed that such positive but not strictly
positive datatypes are of no real use but the construction of
counterexamples. Consequently in various approaches to adding
inductive types to F or CoC they have been ruled out [CoqMoh].

Now, however, I've found a (sort of) reasonable program making
nontrivial use of the 

datatype 'a cont = D | C of (('a cont) -> 'a list) -> 'a list

or in F

cont = All X.X -> ((((X -> list) -> list) -> X) -> X) -> X

where 

list = All X.X -> (A->X->X) -> X

The program computes the list of entries of a binary labelled tree in
the breadth first order. In Lego notation in looks as follows. It can
be executed on Lego "as is". (NOTE CONTINUES AFTER THE PROGRAM)

(* Start of Program *)

[A:Prop];
[o[A,B,C|Prop][g:B->C][f:A->B] = [x:A]g (f x)];

(** Encoding of lists **)
[list = {C|Prop} C -> (A->C->C) -> C];
[nil : list  = [C|Prop][z:C][_:A->C->C] z];
[cons [a:A][l:list] : list  = [C|Prop][z:C][c:A->C->C] c a (l z c)];

(** Encoding of trees **)
[tree = {C|Prop} (A->C) -> (A->C->C->C) -> C];
[L[a:A] : tree = [C|Prop][l:A->C][_:A->C->C->C] l a];
[N[a:A][le,ri:tree] : tree = [C|Prop][l:A->C][n:A->C->C->C]
                                n a (le l n) (ri l n)];

(** Encoding of cont **)
[cont = {C|Prop} C -> (((C -> list) -> list) -> C) -> C];
[D : cont = [C|Prop][d:C][_:((C->list)->list)->C] d];
[C [f:(cont->list)->list] : cont = [X|Prop][d:X][c:((X->list)->list) -> X]
            c ([xl:X->list]f ([k:cont]xl (k d c)))];


(** apply : cont -> (cont->list) -> list **)
[apply[k:cont] = k ([g:cont->list]g D)
                   ([H:(((cont->list)->list)->list)->list]
                        [g:cont->list]H ([f:(cont->list)->list]g (C f)))];


(** breadth : tree -> cont -> cont **)
[breadth[t:tree] = t
  ([a:A][now:cont]C ([later:cont->list]cons a (apply now later)))
  ([a:A][brl,brr:cont->cont][now:cont]
                  C ([later:cont->list]cons a (apply now (o later (o brl brr)))))];

(** extract : cont -> list **)
[extract[k:cont] = k
  nil
  ([f:(list->list)->list]f ([l:list]l))];

(** run : tree -> list **)
[run[t:tree] = extract (breadth t D)];

(** some identifiers **)
[a,b,c,d,e,f,g,h,i,j,k,l,m,n:A];

(** an example tree **)
[t = N a 
        (N b 
           (N d (L h)(L i))
           (N e (L j)(L k)))
        (N c
           (L f)
           (N g (L l)(L m)))];

(Normal (run t));

(** Gives the following system F term 

[C|Prop][nl:C][cns:A->C->C]
cns a (cns b (cns c (cns d (cns e (cns f 
  (cns g (cns h (cns i (cns j (cns k (cns l (cns m nl))))))))))))

End of Program **)

LEGO NOTATION: {A:Prop} and {A|Prop} denote universal type
quantification. [C:Prop] and [C|Prop] denote type abstraction. [x:A]
is ordinary abstraction. An abstraction [A:Prop] outside an actual
term is a variable declaration.


ACKNOWLEDGEMENT: The above program is a transformation of an ML
program invented by Mads Tofte and verified by John Longley. This
original program uses a negative datatype

          datatype 'a cont = D | C of 'a cont -> 'a list

which is not amenable to translation into system F. Thanks to John for
providing the original program to me and for giving some hints as to how it
works. (I still haven't quite understood that.)


Martin Hofmann         	

Laboratory for Foundations of Computer Science 	      	
The King's Buildings, Mayfield Rd
Edinburgh EH9 3JZ    Phone 650 5188


BIBLIOGRAPHY

[CoqMoh]
  AUTHOR    	= "T. Coquand and C. Paulin-Mohring",
  TITLE     	= "Inductively defined types",
  BOOKTITLE 	= "LNCS 389",
  PUBLISHER 	= "Springer",
  YEAR      	= "1989",
             	)

[ReyPlo]
  AUTHOR =    "John C. Reynolds and Gordon D. Plotkin",
  TITLE =     "On Functors Expressible in the Polymorphic Typed
               Lambda Calculus",
  INSTITUTION = "University of Edinburgh",
  YEAR =      "1988",
  number =    "ECS-LFCS-88-53",
  month =     "May"
}