[Ur] Repeated datatype declarations

[Adam Chlipala]

Ron de Bruijn wrote:
> Op 12-10-11 09:41, Gergely Buday schreef:
>>> Why do datatype declarations have to be repeated in the 
>>> implementation file
>>> (.ur) when they are already specified in the interface file (.urs)?
>>
>> They serve different purposes, in the .urs file they are interface
>> declarations, in the .ur file they are implementation declarations,
>> this is how I see them.
>>
>> - Gergely
> If that would be the case there would be a mechanism to mark some 
> datatypes as being exported and some others as not exported. 
> Currently, 'marking' is copying the whole datatype definition, which 
> is completely against http://en.wikipedia.org/wiki/Don't_repeat_yourself .

True in a sense, but it doesn't bother me so much.  Datatypes can be 
repeated with different types between implementation and interface; for 
instance, the interface can use an abstract type where the 
implementation uses a concrete type.

You also have the option of defining datatypes in .ur files without .urs 
files, and you can even import these datatypes into other modules with 
the [datatype foo = datatype M.bar] form.

Filling in datatype definitions for implementations would complicate the 
language, and the real practical win seems small, so it's not on my 
to-do list.  I would consider carefully a patch someone contributed 
adding the sort of functionality you suggest.

> (Also, just because Standard ML does it in this way, doesn't mean it 
> is the best known way to do it. )

True, but I don't hear ML programmers (including OCaml, too) complaining 
about it, which may provide evidence that you'll get used to it and 
actually like it as a simplification of the semantics.  Haskell does not 
have a solution to the problem, because its "module system" is so 
inexpressive.  It is not obvious to me how to follow your suggestion in Ur.