# Define and use an abstract list type constructor. # This is from scratch, without benefit of the builtin List type. # This may appear convoluted, because Ambidexter does not have explicit recursion # in type definitions. Nevertheless, _fix together with Ambidexter's powerful # quantified types (and type constructors!) is up to the task. # Note that as this program is in the by-name aspect, all of the types are dual to how # they are used. # Thus, all L. some T.(|L T| T <+ L T <+ L T |L T<+~Boolean| L T<+(&~True&T&) | L T<+(&~True&L T&)|) # is in effect, some L. all T.(&L T& T -> L T -> L T &L T->~Boolean& L T->(|~True|T|) & L T->(|~True|L T|)&) [{ [ [ \pkg # abstract list package supplied by _fix, # and used to recursively define our list package <+ [ ret -> ( # Give the name LList to the supplied abstract type constructor. @LList:> ( llistpkg # name the supplied packaged, generic LList <+ # returning the package (ret :all L. some T.(|L T| T <+ L T <+ L T |L T<+~Boolean| L T<+(&~True&T&) | L T<+(&~True&L T&)|)) $ # the recursively defined abstract list package [ # the concrete type constructor used to represent L: # Note the reference to the _fix-supplied type LList. @\T.(&~True&(|T|LList T|)&):>c-> c $ [ # Use T to name the element type of the list package being defined. @T<: # Instantiate the element type of the supplied list package to T. [llistpkg [\@T<:p<+p ]] [ # names for the supplied list functions # At last, the list functions themselves can be defined recursively. \|nil|cons|null|car|cdr|<+[|[&a&_& -> a $ [()]] # nil |[ \n<+\ns<+[ # definition of cons ret-> (&(()<+ret$[&_&x&->x$[|n|nil|]]) # case with ns empty &(|k|ks|<+ret$[&_&x&->x$[|n|ks k cons|]]) # case with ns occupied &)$ns ]] |[\x<+[demand -> (&(()<+demand$_true) # definition of null, empty case &(|_|_|<+demand$_false) # non-empty case, ignore contents &)$x]] |[\x<+[demand -> (&(()<+demand$[&x&_&->x$[()]]) # definition of car, empty case &(|k|ks|<+demand$[&_&x&->x$k]) # non-empty case &)$x :(&~True&T&)]] |[\x<+[demand -> (&(()<+demand$[&x&_&->x$[()]]) # definition of cdr, empty case &(|k|ks|<+demand$[&_&x&->x$[ret -> (&(()<+ret$[&x&_&->x$[()]]) # car ks is empty & (kshead<+(&(()<+ret$[&x&_&->x$[()]]) # cdr ks is empty also &(kstail<+ret$[&_&x&->x$[|kshead|kstail|]]) &)$[ks cdr]) &)$[ks car] # non-empty case ]]) &)$x]] |] ] ] # type of the package : all L. some T.(| L T | T<+ L T <+ L T | L T<+~Boolean | L T <+ (&~True&T&) | L T <+(&~True&L T&) |) ] ) ) $ [pkg : all L. some T.(|L T | T <+ L T <+ L T | L T <+ ~Boolean | L T <+(&~True&T&) | L T <+(&~True&L T&) |)] ] ] _fix [\@f<+f] ] _be [\@b<+b] =: list_package; [ ret-> ( # Give the name LList to the packaged abstract type constructor. @LList:> ( # Instantiate the element type to ~Integer, and name the public members. @~Integer<:|nil|cons|null|car|cdr| <+ ret $ [{ # The demonstration: # Form an example list. [[nil 1 cons] 2 cons] _be [\@b<+b] =: alist; # Display the first element of the list. [ret-> (&(()<+ret$["error" _put])&(n<+ret$[{[[n _show_integer] _put]; _put_newline}]) &)$[alist car]]; # Display the second element of the list. [ret-> (&(()<+ret$["error" _put])&( acdr<+(&(()<+ret$["error" _put])&(n<+ret$[{[[n _show_integer] _put]; _put_newline}]) &)$[acdr car]) &)$[alist cdr]] } ] ) ) $ [list_package : all L. some T.(| L T | T <+ L T <+ L T | L T <+~Boolean | L T <+(&~True&T&) | L T <+(&~True& L T &) |)] ] } ]