Markus Mottl wrote:
 >
 >> Note that OCaml's type system fundamentally relies on the fact that
 >> type names cannot be shadowed in structures.
 >
 > Hm, I don't see why this should be so, can you elaborate? I don't know
 > the compiler internals about type inference, this seems like a
 > question of how types are identified internally. I make the reasonable
 > guess that it is not by names (strings) but some kind of integer id or
 > similar.

It's by paths like A.B.C, in which only A is an alpha-convertible 
identifier, the rest are labels. Now consider:

   module X =
   struct
     type t = C
     let x = C
     type t = int
   end

How would you express the type of X.x? There is no label that allows 
projecting the shadowed t.

Sure there are ways to solve this (SML allows the above, for example), 
but most likely they require deviating from, or at least extending the 
theory underlying OCaml modules at the moment (and are likely to be not 
as nice).

 > Maybe I don't see the problem, but since I feel confident that I can
 > always solve this problem manually in a fairly mechanized and
 > straightforward way, I'd be surprised if this couldn't be done by the
 > compiler. Isn't it just a normal alpha conversion problem?

Christophe TROESTLER wrote:
 >
 > The substitution in itself is nothing difficult, isn't it.  Or is it
 > because you need to "backtrack" to change the inferred sigs?  Is the
 > problem when to do it?  Do you have examples?  I do not immediately
 > see why a rule like "duplicate types/modules are forbidden in a sig
 > unless one of them is explicitely renamed" would be difficult to 
check[1].

The first problem is that this construction is a special case - you 
write a signature and it contains occurrences of shadowing. In general 
shadowed items cannot just be forgotten (see the example above), so how 
do you characterise this special case? How can the type checker 
recognise it? It would probably be pretty ad-hoc.

The obstacles are the dependencies within a signature, which prohibit 
arbitrary reordering, and the inability to alpha-rename labels. An 
algorithm that covers all possible cases where a type or module name can 
be forgotten is non-obvious (probably as difficult as identifying these 
cases in the first place). I don't think it's easily doable within the 
current theoretical framework.

Jacques pointed to a paper that seems to be solving this problem, but it 
is using an entirely different framework (and quite a baroque one, I 
have to add). Not all signatures in this framework are translatable back 
to OCaml's, e.g. they can contain mutually dependent substructures.

However, if we just want renaming, and it is explicit, then everything 
should be pretty straightforward.

 > Yes, you are correct -- I was thinking of checking the sig against a
 > given one, not to generate it.

But as is, this isn't a valid sig, so you cannot match it against 
another one.

Cheers,

   - Andreas

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

Let's get rid of those possible thingies!  -- TB