Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Francois Pottier <francois.pottier@inria.fr>]

Hi,

> Note that Russo showed [1] that you can actually get rid of dependent
> typing and interpret ML modules (without nested signatures) as a lambda
> calculus with higher-order polymorphism (i.e., definitely not
> simply-typed). The basic idea is to view functors as functions
> polymorphic over their type arguments.

This interesting idea was also developed by Mark Jones:

  @InProceedings{jones-96,
    author       = "Mark P. Jones",
    title        = "Using Parameterized Signatures to Express Modular
		   Structure",
    booktitle    = "Proceedings of the 23rd {ACM} Symposium on Principles
		   of Programming Languages",
    publisher    = "ACM Press",
    month        = jan,
    year         = "1996",
    address      = "St. Petersburg Beach, Florida",
    note         = "\url{http://www.cse.ogi.edu/~mpj/pubs/paramsig.html}",
  }

as well as (in a couple of much more technical papers) by Zhong Shao.

> In this setting, adding abstract signatures would at least require adding
> polymorphic kinds, I believe.

What do you mean? In this encoding, modules are only records, so module types
are ordinary types, and there is no distinction between ordinary abstract
types (introduced by explicit polymorphic abstraction) and ``abstract
signatures''. There is, as far as I can tell, no need for kind polymorphism.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners