[TYPES] recursive data types with negative occurrence (besides higher-order abstract syntax)

[Eijiro Sumii]

Dear all,

Below is a summary of replies to my question about examples of
recursive data types with negative occurrence.  It looks like they may
be summarized as follows:

 - HOAS and variants
 - object encodings
 - semantic domains in denotational interpreters
 - Y-combinator
 - a few others

As for the question in my "P.S." (how to convert HOAS into de Bruijn
index), Prof. Hongwei Xi gave the following code (a little modified
for brevity).

  type 'a hlam =
    | HVar of 'a
    | HLam of ('a hlam -> 'a hlam)
    | HApp of 'a hlam * 'a hlam
  
  type ilam =
    | IVar of int
    | ILam of ilam
    | IApp of ilam * ilam
  
  let rec hlam2ilam' i = function
    | HVar x -> IVar (i - x)
    | HLam f -> ILam (hlam2ilam' (i + 1) (f (HVar (i + 1))))
    | HApp(t1, t2) -> IApp(hlam2ilam' i t1, hlam2ilam' i t2)
  let hlam2ilam = hlam2ilam' 0
  
  (*
  # hlam2ilam (HLam(fun x -> HLam(fun y -> HApp(y, x)))) ;;
  - : ilam = ILam (ILam (IApp (IVar 0, IVar 1)))
  *)

Thanks to everybody!

	Eijiro

From: "Eijiro Sumii" <sumii at saul.cis.upenn.edu>
> I'm looking for examples (as many as possible) of recursive data
> types with negative occurrence, like
> 
>   type lam = Lam of (lam -> lam) | App of lam * lam
> 
> for instance.  So far, I've only found higher-order abstract syntax
> and its variants (including the "universal domain").  If somebody
> knows any other example, please drop me a message!  I'll post a
> summary later to this list.

From: Dan Grossman <djg at cs.washington.edu>
> Don't you need it to encode the Y combinator in "System F plus mu"?
> I'd argue recursion doesn't naturally fit in hoas or a
> universal-domain.

From: Johan Glimming <glimming at kth.se>
> I have some examples of such datatypes in relation to some work I am
> doing on recursion on object types. Why are you interested in this?
> What are you currently doing? Maybe our work coincides.

From: anton setzer <a.g.setzer at swansea.ac.uk>
> The Mahlo universe is an interesting example, see the article
> "Extending Martin-Löf Type Theory by one Mahlo-Universe" on my
> homepage,
> <http://www-compsci.swan.ac.uk/%7Ecsetzer/articles/mahlo.dvi>
> http://www.cs.swan.ac.uk/~csetzer/

From: Hongwei Xi <hwxi at cs.bu.edu>
> How about this:
> 
> datatype name = A | B | C | D | ...
> 
> datatype object = OBJ of (msg -> unit)
>      and msg = MSG of name * object list

From: Richard Nathan Linger <rlinger at cse.ogi.edu>
> Sava Krstic and John Launchbury have published a few things on
> Hyperfunctions.  A Hyperfunction from a to b is a member of the 
> recursive datatype
> 
> 	  H a b = H b a -> a
> 
> They use this type to model coroutines and derive a build-cata law for 
> the zip function
> 
> 	  zip :: a list -> b list -> (a,b) list
> 
> Check it out at	http://www.cse.ogi.edu/~krstic/psfiles/folds.ps
> More papers on the same topic are at	http://www.cse.ogi.edu/~krstic/

From: Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
> Semantics-based interpreters where the denotational semantics would
> involve reflexive domain equations gives rise to the use of such
> datatypes. I'm not an expert on this (Olivier Danvy could probavbly
> provide loads of examples), but I did come across quite a nice example,
> generated to illustrate the usefulness of Fresh O'Caml
> <www.freshml.org/foc>, namely "normalization by evaluation": see
> 
> <www.cl.cam.ac.uk/users/amp12/research/freshml/foc-examples/nbe.ml.html>
> for the case of untyped lambda calculus
> 
> and
> 
> <www.cl.cam.ac.uk/users/amp12/research/freshml/foc-examples/plc-nbe.ml.html>
> for the case of polymorphic lambda calculus.

From: Reynald Affeldt <affeldt at yl.is.s.u-tokyo.ac.jp>
[snipping some notes in Japanese...]
> http://www1.elsevier.com/gej-ng/31/29/23/125/50/29/70.2.007.pdf

From: Andreas Abel <abel at informatik.uni-muenchen.de>
> The classical example is Mads Tofte's breadth-first flattening algorithm 
> using a negative datatype (see attachment).  Martin Hofmann turned this 
> into an algorithm using a doubly-negative, hence, non-strictly positive 
> type (see his posting on TYPES 1993, attachment).

From: Thorsten Altenkirch <txa at cs.nott.ac.uk>
> You get those when implementing "Normalisation by Evaluation" in a
> simply typed language. Examples are the normalizers in the appendix
> of the CTCS 95 paper (see
> http://www.cs.nott.ac.uk/~txa/publ/ctcs95.pdf) which I wrote with
> Martin Hofmann and Thomas Streicher or more recently the FLOPS 04
> paper (http://www.cs.nott.ac.uk/~txa/publ/flops04.pdf) which is a
> joint production with Tarmo UUstalu.
> 
> In all these cases you get a negative domain equation from a
> "universe" construction in Type Theory, where all functions are
> total. E.g. in Epigram (http://www.dur.ac.uk/CARG/epigram/) you can
> define
> 
> -----------------------------------------------------------------------------
> 					 (  s, t : Type   !
> data (----------!  where nat : Type ;  !----------------!
>      ! Type : * )                      ! arr s t : Type )
> -----------------------------------------------------------------------------
>      ( sigma : Type  !                      
> let  !---------------!                      
>      ! Val sigma : * )                      
> 					      
>      Val sigma <= rec sigma                 
>      { Val x <= case x                      
> 	 { Val nat => Nat                     
> 	   Val (arr s t) => (Val s) ->(Val t)
> 	 }                                    
>      }   
> -----------------------------------------------------------------------------
> 
> However, if we map Val into a simply typed language we get
> 
> Val = Nat | Val -> Val
> 
> It is my impression that all sensible uses of negative domain
> equation can be explained in *total* Type Theory with strictly
> positive Types. Having simple types is like having dirty glasses,
> you can't see the types well enough and you everything gets
> partial...

From: Frank Atanassow <franka at cs.uu.nl>
> Are you aware that your type lam below admits non-lambda terms? For
> example:
> 
>    Lam (function Lam f -> ... | App f1 f2 -> ...)
> 
> There are a couple of different approaches that try to restrict this
> in ways that only admit lambda-terms. I think in at least two of
> them (Gabbay-Pitts, and Fiore et al.), lam doesn't occur in any
> negative positions.

From: Marino Miculan <miculan at dimi.uniud.it>
> Since you mentioned HOAS, likely you already known the so called "weak 
> HOAS" approach - which is a bit different from "full HOAS".  The basic 
> idea is to have "open" types in negative positions, that is types 
> without constructors.  Representation techniques for weak HOAS have 
> been deeply studied in my PhD thesis [Mic97].
> One problem arising from weak HOAS approach is that usual type theories 
> do not have the necessary expressive power for proving some important 
> properties, like higher-order recursion and induction, equivariance of 
> predicates and so on.  A possible solution we have devised in 
> [HMS01a,HMS01b] is to add three key properties of HOAS encodings as 
> axioms (the so called "Theory of Contexts").  These have been proved 
> sufficient for developing a large amount of theory about datatypes with 
> negative occurrences, such as the derivation of higher-order induction 
> principles.  However, there are still some limitations on the 
> functional level: since the model behind the Theory of Contexts does 
> not allow for the Axiom of Unique Choice, there are some functional 
> predicates (e.g., one to one relations) for which there does not exist 
> the corresponding function.
> 
> [Mic97] M. Miculan. Encoding Logical Theories of Programs. Ph.D. Thesis 
> TD-7/97, March 1997. Dipartimento di Informatica, Universitˆ di Pisa.
> [HMS01a] F.Honsell, M.Miculan, I.Scagnetto. An axiomatic approach to 
> metareasoning on systems in higher-order abstract syntax.  In 
> Proceedings of ICALP'01, Number 2076 in Lecture Notes in Computer 
> Science, pages 963-978, 2001
> [HMS01b] F.Honsell, M.Miculan, I.Scagnetto. ¹-calculus in (Co)Inductive 
> Type Theories. In Theoretical Computer Science, 253(2), pages 239-285, 
> 2001.

From: Keith Wansbrough <Keith.Wansbrough at cl.cam.ac.uk>
> See my thesis,
> 
> http://www.cl.cam.ac.uk/~kw217/research/phd/index.html
> 
> pages 157-158.  I list these examples, in Haskell notation:
> 
> (Thanks for these examples to members of the Haskell list
> haskell at haskell.org, 4 July, 2001: Sebastien Carlier, Koen Claessen,
> Ralf Hinze, Lars Mathiesen, and Mark Shields.)
> 
> Parsers and other continuation-passing styles are one example:
> an LR parser might use a data type like the following:
> 
>   data State = MkState (Sym                       -- next symbol
> 			  -> List (Pair State Sym)  -- stack
> 			  -> List Sym               -- input
> 			  -> Sym)                   -- result
> 
> Another example is Fix, used to encode the Y-combinator in Haskell
> [MH95]:
> 
>   data Fix a = F (Fix a -> a)
> 
>   fix :: (a -> a) -> a
>   fix f = (\ (F x) -> f (x (F x))) (F (\ (F x) -> f (x (F x))))
> 
> Other examples come from object encodings, higher-order abstract
> syntax, and domain encodings.
> 
> A particularly elegant combination of negative and non-uniform
> recursion occurs in hyperfunctions, used in [LKS00] for zip fusion:
> 
>   data H a b = Cont (H b a -> b)
> 
> Here a occurs only negatively and b only positively, thus sidestepping
> the usual problems of bivariance in negatively-recursive data types.
> 
> 
> @InCollection{
>     MH95,
>     author = "Erik Meijer and Graham Hutton",
>     title = "Bananas in Space: Extending Fold and Unfold to Exponential Types",
>     crossref="ACM95:FPCA",
>     month="jun",
>     pages = "324--333",
>     year = "1995",
> }
> 
> @UnPublished{
>    LKS00,
>    author="John Launchbury and Sava Krsti{\'c} and Timothy E. Sauerwein",
>    title="Zip Fusion with Hyperfunctions",
>    note="Available \url{http://www.cse.ogi.edu/~krstic/}",
>    year="2000",
>    documentURL="http://www.cse.ogi.edu/~krstic/",
> }

From: Alan Jeffrey <ajeffrey at cs.depaul.edu>
> Recursive datatypes with negative occurrences come up quite naturally in
> OO programs, for example:
> 
>   interface List {
>     Object head ();
>     List tail ();
>     ...
>     List append (List other);
>   }
> 
> the append method is both covariant and contravariant in the recursive
> List datatype.

From: Chung-chieh Shan <ccshan at post.harvard.edu>
> In a draft paper at http://www.eecs.harvard.edu/~ccshan/recur/ , I show
> how "dynamic" control operators for delimited continuations (such as
> Felleisen's control and prompt) can be expressed in terms of "static"
> ones (such as Danvy and Filinski's shift and reset), in Felleisen's
> sense of macro-expressivity (Science of Computer Programming 1991).
> 
> One way to think of this result is that it implements control and
> prompt in a monad.  In Haskell syntax, the monad is defined by M in
> 
>     newtype C ans val  =  C (val -> Maybe (C ans ans) -> ans)
>     newtype M ans val  =  M (C ans val -> ans)
> 
> Here "C" is a recursive data type with negative occurrence.