Re: [newbie] Define and use records in sum types

[Markus Mottl <mottl@miss.wu-wien.ac.at>]

On Sun, 23 Jul 2000, Frank Atanassow wrote:
> So the type-theoretic role of the signature restriction is to do
> existential quantification (or something close to it), and delimit the
> scope of the quantification on types and values.

The abstract type refers to a specific representation (you can't mix
different ones - quantification on type), but also does not allow you to
use datastructures of the same representation that were not created by the
"right" functions (= quantification on values). That's at least what I
think you mean - I am not a type-theorist.

> However, there is no reason why it needed to hide, e.g.,
> ListSet.removeDup. It could have also added removeDup to Set also,
> without breaking abstraction, as long as it weren't included in the scope
> of the quantification. Then Set.removeDup would have type 'a list -> 'a
> list, so you couldn't apply it to sets, so there is no problem.

Right: you can make *some* functions available this way, but not all! There
may be functions that are not defined (crash, loop, whatever) for all
values, only for ones for which some semantic property holds. However, it
may not even be the case that it holds for the abstract type itself, but
only for the specific way in which the function is called internally, i.e.
the precondition for the function to work correctly is stronger. You
therefore still need means to hide such functions.

In fact, I use your "trick of revelation" in some projects to export the
internal representation of the abstract types safely and without
computational costs.  E.g. with the set-example

  val list_of_set : 'a set -> 'a list

This could be the identity function internally. If I change the
representation, I'd only have to write a conversion function. Of course,
one shouldn't do such things with mutable values...

> BTW, if you are familiar with category theory, then you will know that
> all this stuff, even the binding syntax for quantification and
> abstraction, can be translated into a purely semantic, variable-free
> form. Ipso facto, you don't need syntactic notions like names or
> name-hiding to express it.

Well, category theory is on my "to-learn-list" ;)

I understand only some basic notions that allow me to make practical use of
them (e.g. partial evaluation of strict languages with effects (impure
functions, non-termination) using monads to handle the effect stuff).

> Nono, identity is important. I'm just saying identifier visibility and
> renaming should have nothing to do with semantics. (Scope is important,
> though. By "visibility doesn't matter", I guess I mean you should never need
> to _remove_ an identifier from the set of free variables in a subterm.)

Ok, I see what you mean (meant).

> Well, I disagree that nothing can be done about it. Personally, I wouldn't
> mind so much if shadowing were outlawed entirely, but a less drastic solution
> is the one adopted by Haskell and Mercury, in which one distinguishes
> top-level bindings from local ones, and "lazily" disallow shadowing at the
> top level. This means that you can import distinct values with the same name,
> but you only get an error if the name is actually used somewhere in the
> module.

Ok, this is a reasonable way to do it: I'd also like to be "kicked" by the
compiler when I open several modules that have common names and when I
indeed use one of them. This is bad style - other readers might become
confused about what the program means (not everybody likes reading 1000
lines to find out about the order of import). So using this "lazy boot" to
kick me would be fine.

Maybe there could be a warning option for this in OCaml?

> But that's just FYI; I'm not suggesting that Ocaml's shadowing rules be
> changed in any way.

This would also surely break tons of code (legacy is a burden). But I don't
consider it to be so bad at all...

> Frankly, I think Ocaml's perspective, that top-level value bindings are
> treated essentially the same way as local bindings, is nicely consistent in
> its own way, though. (However, it arguably causes problems too, since
> side-effects at the top level makes module-linking order significant.)

Well, there are also other reasons having to do with "shadowing module
names" during linking...

I don't know whether this "shadowing feature" is so useful at all. It just
provokes bad style where a functor would be more appropriate.

If we take out this feature and only allow side effecting value definitions
in one module (better: compilation unit), then we could finally end up with
a much nicer linking semantics (-> commuting module names! Great!).

>  > Then it might be a bit more convenient to have an initial declaration that
>  > tells the compiler what kind of record you are talking about instead of
>  > inventing new names for records. A rather statistical question...
> 
> What sort of declaration?

I don't want to write

  { t1.v1 = x; t1.v2 = y; ... }

but something similar to:

  { t1 | v1 = x; v2 = y; ... }

However, maybe there could be a solution that makes use of the type system?
(Though, I fear that this would require very incompatible changes).

Could mandatory type annotations help here? I think there are several
occasions where they might help, but I am not an expert here - maybe
someone else can tell us more about this.

If I am not mistaken, this could help solve this problem besides
polymorphic recursion and maybe also remove the need for type coercions for
objects (e.g. when you put several ones of different type into a list).

> But this construct is closely analogous to the existing dot-notation for
> modules. For all we know, it may turn out that some programmers actually
> mistakenly assume it already exists.

This may be true - or not: I don't know. As I said: if enough people say
"this is intuitive", I wouldn't be opposed to it. I don't feel annoyed by
such a feature, but that's not enough to add it, because there are a
zillion things that do not annoy me...

> However, it occurs to me now that my syntax would bring type names into the
> same namespace as field labels. The reason is because of the ambiguity: does
> "m.t.x" mean "the field x of the t-record m", or "the field x of the field t
> of the record m"? I guess having type names and labels in the same namespace
> is bad, so you would want a different syntax, maybe "m:t.x" for selection and
> 
>   { x = ... } : t
> 
> for building. I guess that makes it essentially the same as SML's records.

Well, we are already nearly at mandatory type annotations ;-)

Let's wait and see what people think of this problem in general. If it is
important enough to them, they will say so...

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl