Re: [Sml-implementers] Structure sharing and type abbreviations

[Dave B. <da...@ta...>]

At 10:09 17/09/2001, Matthias Blume wrote:
>I disagree with this view.  If you prohibit redefinitions of names, you get 
>a serious modularity problem:   Any program that has a global or local name
>"foo" can no longer be linked with a library that exports a binding under the
>name "foo".  

I'm assuming that each library is a separate namespace.  Clearly we need a
way to distinguish a binding in one library from that in another.

>As for the interactive toplevel:  I agree with you that having it is pretty 
>useless for anyone outside the theorem-proving community.  
>
>On the other hand, I do not agree with your assessment that there is 
>something fundamentally flawed about the way the interactive toplevel
works in ML.

I think your first statement is a strong counter-argument to your second.
I would like a system that allows interactive program development, not just
a shell for theorem provers.  But tastes differ.

>Anyway, I can live with the idea of not having an interactive toplevel. On 
>the other hand, not being able to redefine (locally or at the
(non-interactive)
>toplevel) a globally bound name is absolutely unacceptable IMO.

Please note that I explicitly stated that rebindings at inner scope would
be permitted.  I didn't mention libraries, but it is certainly my intention
to allow an identifier to be defined in different libraries.

Dave.