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

[Eijiro Sumii]

Dear all,

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.

--
Eijiro Sumii (http://www.cis.upenn.edu/~sumii/)
Department of Computer and Information Science, University of Pennsylvania

P.S. I'm also interested in how to convert higher-order abstract
syntax into "de Bruijn index" syntax _without_ going through
first-order abstract syntax (or a straightforward deforestation of
doing so).  Please let me know, too, if there is a better way to do
this.