Re: [Caml-list] Re: Encoding "abstract" signatures

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

François,

> It would be interesting to devise a type system that has this property. Didier
> Rémy noticed the need for such a feature back in 1994 when writing `Dynamic
> typing in polymorphic languages' (see section 4.2 of the SRC tech report).

Ah, indeed, he is discussing something quite similar. Interesting.

But I strongly suspect that even a system like that wouldn't be enough
to encode OCaml's modules. Consider that higher-order type again:

    functor(Y : sig module type T end) -> functor(X : Y.T) -> ...

The idea was representing this as

    Forall k. forall T:(k->*). forall ts:k. T(ts) -> ...  (*)

But that is still not good enough, because we might apply

    T = sig module type U module type V end

The result had to be something like

    Forall k1. Forall k2. forall U:(k1->*). forall V:(k2->*). ...

so (*) is not an appropriate encoding -- application may also result in
an indefinite number of kind quantifiers. We might try to tackle that by
introducing another universe of "hyperkinds" and repeat the same trick.
But unfortunately, that just pushes the problem to yet another level --
no finite number of additional universes will help, because what OCaml
provides with nested abstract signatures is essentially Type:Type.

So I conjecture that it is impossible to faithfully encode OCaml's
modules into a non-dependent system (which comes to no surprise taking
into account that it is known to be undecidable).

-- 
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