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

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

"Krishnaswami, Neel" wrote:
> 
> Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> > Neel Krishnaswami wrote:
> >
> > > There's no recursion in the module system because that would break
> > > the termination guarantee. If you think of modules as records, and
> > > functors as lambda abstractions, you can see that the module system
> > > defines a simply-typed lambda calculus. As you've noticed with C++,
> > > adding recursion to it would mean you can write nonterminating module
> > > expressions. (All this is wonderfully clearly explained in
> > > the paper, "A modular  module system".)
> >
> > I'm not sure about "simply-typed". Did the situation change since
> > that of http://caml.inria.fr/archives/199907/msg00027.html ?
> 
> Wow! I didn't even know that was possible. I thought that typechecking
> record subtyping was decidable...?

Well, module types are (a limited form of) dependent types. What
concretely triggers undecidability of subtyping in OCaml is the presence
of abstract module types, at least in combination with the
contravariance of higher-order functors.

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. In this setting, adding abstract
signatures would at least require adding polymorphic kinds, I believe.

[1]

@inproceedings{Russo:NonDependentTypes,
  author	= "Claudio Russo",
  title		= "Non-Dependent Types for {Standard} {ML} Modules",
  booktitle	= "International Conference on Principles and
                   Practice of Declarative Programming",
  address	= "Paris, France",
  year		= 1999,
  month		= sep,
}

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
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