Where are higher-rank and existential types used?

[Ken Shan]

Hello,

Norman Ramsey and I are looking for examples of where higher-rank
polymorphism and existential types are useful.  Can anyone think of
uses besides the following?

Higher-rank types are used in:

  - Deforestation

    Andrew Gill, John Launchbury, and Simon L. Peyton Jones. 1993.  A
    short cut to deforestation.  In _Functional programming languages
    and computer architecture: 6th conference_, 223-232. New York: ACM
    Press.

  - Lazy functional state threads

    John Launchbury and Simon L. Peyton Jones. 1994.  Lazy functional
    state threads.  In _PLDI '94: Proceedings of the ACM conference on
    programming language design and implementation_, vol. 29(6) of _ACM
    SIGPLAN Notices_, 24-35. New York: ACM Press.

  - Generic (polytypic) programming

    Ralf Hinze. 2000.  A new approach to generic functional programming.
    In _POPL '00: Conference record of the annual ACM symposium on
    principles of programming languages_, 119-132. New York: ACM Press.

    Ralf Lämmel and Simon L. Peyton Jones. 2003.  Scrap your
    boilerplate: A practical design pattern for generic programming.  In
    _Proceedings of the 2003 ACM SIGPLAN international workshop on types
    in languages design and implementation_, 26-37. New York: ACM Press.

  - Data type invariants

    Chris Okasaki. 1999.  From fast exponentiation to square matrices:
    An adventure in types.  In _ICFP '99: Proceedings of the ACM
    international conference on functional programming_, vol. 34(9) of
    _ACM SIGPLAN Notices_, 28-35. New York: ACM Press.

    Ralf Hinze. 2001.  Manufacturing datatypes.  _Journal of Functional
    Programming_ 11(5): 493-524.

    Richard Bird and Ross Paterson. 1999. de Bruijn notation as a nested
    datatype.  _Journal of Functional Programming_ 9(1): 77-91.

Existential types are used in:

  - Object-oriented programming

    Benjamin C. Pierce and David N. Turner. 1994.  Simple type-theoretic
    foundations for object-oriented programming.  _Journal of Functional
    Programming_ 4(2): 207-247.

    Konstantin Läufer. 1996.  Type classes with existential types.
    _Journal of Functional Programming_ 6(3): 485-517.

  - Abstract data types

    John C. Mitchell and Gordon D. Plotkin. 1988.  Abstract types have
    existential type.  _ACM Transactions on Programming Languages and
    Systems_ 10(3): 470-502.

Any pointers or technique descriptions would be highly appreciated!  If
there are many contributions, I will post an updated version of this
list.

	Ken

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
United Nations Day is 24 October. http://www.un.org/events/unday/
The Lost Voice of Radio Beijing http://www.milinfoserv.net/lvrb.html
Write letters!  We got half of New Testament that way.