[newbie] Define and use records in sum types

[newbie] Define and use records in sum types

[David Mentré]

Hello dear camlists,

I have problems with basic record and sum types use.

I would like to define a sum type with records as constructor
parameters, records with the same field names. 

I have tried the follwing definition:

<ocaml>
# type asp = A of { name : string } | B of { name : string ; ext : int };;
                  -
Syntax error
</ocaml>

However, I can use intermediate names:

<ocaml>
# type a_rec = { name : string };;
type a_rec = { name : string; } 
# type b_rec = { name : string ; ext : int };;
type b_rec = { name : string; ext : int; } 
# type asp = A of a_rec | B of b_rec ;;
type asp = A of a_rec | B of b_rec
</ocaml>

It *seems* to work but, in fact, the a_rec definition is masked by b_rec
definition:

<ocaml>
# let a_b = B({name = "n" ; ext=3 }) ;;
val a_b : asp = B {name="n"; ext=3}
# let an_a = A({name="n"});;
               ----------
Some record field labels are undefined
</ocaml>

So my question is: is it possible to define a sum of records with the
same field names? 


The rationale behind this question: I find records more clear that
tuples in source code.


Best regards,
david
-- 
 David.Mentre@irisa.fr -- http://www.irisa.fr/prive/dmentre/
 Opinions expressed here are only mine.

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

[Markus Mottl]

On Tue, 11 Jul 2000, David Mentré wrote:
> I would like to define a sum type with records as constructor
> parameters, records with the same field names. 

It is unfortunately not possible to use records with the same names at the
same time without putting them into separate modules.

> It *seems* to work but, in fact, the a_rec definition is masked by b_rec
> definition:

Exactly: names of record fields get overridden by subsequent definitions.
There is no way to get the "old" meaning back without the use of modules.

> The rationale behind this question: I find records more clear that
> tuples in source code.

Using records makes sources more readable and also easier to maintain. For
example, the "with" statement as in

  { some_record with some_field = some_value; ... }
  
allows adding fields to records without breaking code.

Best regards,
Markus Mottl

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

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

[Jean-Christophe Filliatre]

> I have problems with basic record and sum types use.
> 
> I would like to define a sum type with records as constructor
> parameters, records with the same field names. 
> 
> I have tried the follwing definition:
> 
> <ocaml>
> # type asp = A of { name : string } | B of { name : string ; ext : int };;
>                   -
> Syntax error
> </ocaml>

I don't know what you want to do exactly, but I applied to following
idea (which you can find in the ocaml sources) for AST tagged with
common informations:

type t = { name : string; info : u }
 and u = A
       | B of int

(in the case of AST, t and u are really mutually recursive, with
occurrences of t in the arguments of u's constructors)

Then you can still make pattern-matching like this
 
   match x.info with A -> ... | B n -> ...

and still access the name field with x.name.

Hops this helps,
-- 
Jean-Christophe Filliatre    
  Computer Science Laboratory   Phone (650) 859-5173
  SRI International             FAX   (650) 859-2844
  333 Ravenswood Ave.           email filliatr@csl.sri.com
  Menlo Park, CA 94025, USA     web   http://www.csl.sri.com/~filliatr

  

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

[Markus Mottl]

On Wed, 19 Jul 2000, John Gerard Malecki wrote:
> Many of the professional programmers I show ocaml to like it very much
> but are annoyed by this behavior.  Maybe there is a reasonable work
> around?  The normal solution for the behavior of ocaml records is to
> prepend the record name to the field name.  For example,
> 
> 	type male = { male_name : string; male_salary : int }
> 	type female = { female_name : string; female_salary : float }

Ahem, do you want to express with this example that women earn so little in
your company as compared to men that you need floats to express their
salary? ;-)  (only joking!)

Well, anyway, modules solve the problem quite well - why not use them?  The
effort is hardly worth mentioning.

E.g.:

  module Male = struct
    type t = { name : string; salary : int }
    let raise_salary p n = { p with salary = p.salary + n }
  end

  module Female = struct
    type t = { name : string; salary : float }
    let raise_salary p n = { p with salary = p.salary +. n }
  end

  let _ =
    let male = { Male.name = "Albert"; Male.salary = 1000 }
    and female = { Female.name = "Berta"; Female.salary = 1000.0 } in
    let happy_male = Male.raise_salary male 100
    and happy_female = Female.raise_salary female 100.0
    and other_female = { female with Female.name = "Caroline" } in
    ()

> but then reference
> 
> 	 { male:salary = x }

The module version nearly looks the same ("." instead of ":" and capital
letter). Additionally, it forces people to introduce some modularity into
the program, which is hardly a drawback.

> The idea is to allow the disambiguation to be optional.  It may
> confuse novices but ...

I'd opt against this: to me, modules already provide a regular way to
organize namespaces - no need to add even further constructs to the
language...

Best regards,
Markus Mottl

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

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

[David Mentré]

Jean-Christophe Filliatre <filliatr@csl.sri.com> writes:

> type t = { name : string; info : u }
>  and u = A
>        | B of int

Many thanks to all people that kindly respond. It was pretty much the
solution I took.

d.
-- 
 David.Mentre@irisa.fr -- http://www.irisa.fr/prive/dmentre/
 Opinions expressed here are only mine.

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

[Frank Atanassow]

Markus Mottl writes:
 > On Wed, 19 Jul 2000, John Gerard Malecki wrote:
 > > 	type male = { male_name : string; male_salary : int }
 > > 	type female = { female_name : string; female_salary : float }
 > [..]
 > Well, anyway, modules solve the problem quite well - why not use them?  The
 > effort is hardly worth mentioning.
 > 
 > E.g.:
 > 
 >   module Male = struct
 >     type t = { name : string; salary : int }
 >     let raise_salary p n = { p with salary = p.salary + n }
 >   end
 > 
 >   module Female = struct
 >     type t = { name : string; salary : float }
 >     let raise_salary p n = { p with salary = p.salary +. n }
 >   end

I used to do this. (Actually, in this case I would have used a functor to
capture the commonality.) But I stopped because inevitably, after some
development, the type t becomes recursive, and you cannot have recursive types
spanning modules, so I would have to go back to the straightforward method.

 > > The idea is to allow the disambiguation to be optional.  It may
 > > confuse novices but ...
 > 
 > I'd opt against this: to me, modules already provide a regular way to
 > organize namespaces - no need to add even further constructs to the
 > language...

I disagree. In fact, I think one should divorce the type abstraction and
namespace-handling aspects of modules. It's true that the uses often coincide,
but I think it obscures the issues. In particular, I think it encourages
programmers to conflate syntactic information-hiding (like not exporting some
constructors or functions) with type-theoretic information-hiding (like
abstracting a type with a functor). The first ought to be considered only as
an engineering technique to reduce complexity. The second OTOH is a logical
technique to increase flexibility of implementation.

As it stands, though, I realize that the current module system is far too
entrenched to change, so I would be happy if we could just qualify constructor
and field labels by their type constructor's name, so that this would
typecheck:

  type r1 = { name: int }
  type r2 = { name: float }
  type t1 = A of int
  type t2 = A of float
  let (r2,t2) : r2 * t2 = { name = 1.0 }, A 2.0
  let (r1,t1) : r1 * t2 = { r1.name = 1 }, t1.A 2

I believe this issue came up a few months ago...

-- 
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791

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

[Markus Mottl]

On Fri, 21 Jul 2000, Frank Atanassow wrote:
> Markus Mottl writes:
>  >   module Male = struct
>  >     type t = { name : string; salary : int }
>  >     let raise_salary p n = { p with salary = p.salary + n }
>  >   end
>  > 
>  >   module Female = struct
>  >     type t = { name : string; salary : float }
>  >     let raise_salary p n = { p with salary = p.salary +. n }
>  >   end

> I used to do this. (Actually, in this case I would have used a functor to
> capture the commonality.)

Well, there is not so much commonality to catch in the upper example:
to me, a functor would be a bit overkill here if the only thing you want
to do is having a separate namespace. Unless you really see a longterm
benefit in some abstraction, it's not a good idea to make the code more
complex with functors.

> But I stopped because inevitably, after some development, the type t
> becomes recursive, and you cannot have recursive types spanning modules,
> so I would have to go back to the straightforward method.

Inevitably? Why? At least in the cases where I found a problem with
building modules, I always discovered an easy (and generally much
cleaner) way to restructure the design to get around it. In fact, such
problems point me to design errors. (Yes, there are rare examples, where
redesigning does not help, but I never felt the need to implement one
for real purposes).

> I disagree. In fact, I think one should divorce the type abstraction and
> namespace-handling aspects of modules.

I agree.

> It's true that the uses often coincide,
> but I think it obscures the issues. In particular, I think it encourages
> programmers to conflate syntactic information-hiding (like not exporting some
> constructors or functions) with type-theoretic information-hiding (like
> abstracting a type with a functor). The first ought to be considered only as
> an engineering technique to reduce complexity. The second OTOH is a logical
> technique to increase flexibility of implementation.

But how about "capturing logical invariants"? You need both ways of
information hiding there: restricting the number of exported functions
*and* restricting their types! Otherwise there could be ways to destroy
the invariant.

> As it stands, though, I realize that the current module system is far too
> entrenched to change, so I would be happy if we could just qualify constructor
> and field labels by their type constructor's name, so that this would
> typecheck:
> 
>   type r1 = { name: int }
>   type r2 = { name: float }
>   type t1 = A of int
>   type t2 = A of float
>   let (r2,t2) : r2 * t2 = { name = 1.0 }, A 2.0
>   let (r1,t1) : r1 * t2 = { r1.name = 1 }, t1.A 2

I'd rather use different namings like "r1_name" and "r2_name" for the
field: although this requires me to always include the name of the type,
one cannot get confused either: it makes the sources easier to understand.

Best regards,
Markus Mottl

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

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

[Frank Atanassow]

[reusing record labels by putting them in different modules]

Markus Mottl writes:
 > On Fri, 21 Jul 2000, Frank Atanassow wrote:
 > > But I stopped because inevitably, after some development, the type t
 > > becomes recursive, and you cannot have recursive types spanning modules,
 > > so I would have to go back to the straightforward method.
 > 
 > Inevitably? Why?

Because non-recursive datatypes are trivial, and baby programs are trivial,
but they grow up into non-trivial adults.

 > At least in the cases where I found a problem with building modules, I
 > always discovered an easy (and generally much cleaner) way to restructure
 > the design to get around it. In fact, such problems point me to design
 > errors. (Yes, there are rare examples, where redesigning does not help, but
 > I never felt the need to implement one for real purposes).

Let's not get into discussions about refactoring or recursive modules.

The fact is that in your example you used only the namespace-handling aspect
of modules to achieve field label overloading. The restriction against modules
being recursive has nothing to do with their namespace-handling aspect, but
rather implementation and type-theoretic issues. If you had opted to solve the
problem by just adding a prefix to the labels (or used my proposed
mechanism), and kept them in the same module, then you would not have had to
appeal to (largely unrelated) issues like refactoring, and would have happily
let there be recursive dependencies among the types in question, if the
situation warranted it.

What I'm saying is that, because the module system treats both the
namespace-handling aspect and the type-theoretic aspects in one language
construct, the restrictions on one aspect carry over to the other. Therefore,
if you use the module system solely for namespace-handling, it's liable to
bite you in the end.

Of course for something like salary records, you aren't likely to engender
any recursion no matter how long you develop the program; my objection is to
the general applicability of the technique.

 > > It's true that the uses often coincide, but I think it obscures the
 > > issues. In particular, I think it encourages programmers to conflate
 > > syntactic information-hiding (like not exporting some constructors or
 > > functions) with type-theoretic information-hiding (like abstracting a
 > > type with a functor). The first ought to be considered only as an
 > > engineering technique to reduce complexity. The second OTOH is a logical
 > > technique to increase flexibility of implementation.
 > 
 > But how about "capturing logical invariants"? You need both ways of
 > information hiding there: restricting the number of exported functions
 > *and* restricting their types! Otherwise there could be ways to destroy the
 > invariant.

Can you be more specific about "capturing logical invariants"? I don't know
quite what you mean.

An instance I can think of where access to names could have semantic
significance is if it has to do with generativity. I hate generativity with a
passion, but eliminating it from ML modules would require a wholesale revision
of the module system, which it is not my object to propose here. So, I will
concede that generativity may cause name access to acquire semantic
significance. (But I hope you agree that it is at least desirable that names
and namespaces should have no semantic significance whatsoever.)

BTW, I inadvertantly omitted the most important reason for namespace-handling
constructs: to prevent conflicts and unwanted shadowing arising when you use
modules developed by different people.

 > > As it stands, though, I realize that the current module system is far too
 > > entrenched to change, so I would be happy if we could just qualify
 > > constructor and field labels by their type constructor's name, so that
 > > this would typecheck:
 > > 
 > >   type r1 = { name: int } type r2 = { name: float } type t1 = A of int
 > >   type t2 = A of float let (r2,t2) : r2 * t2 = { name = 1.0 }, A 2.0 let
 > >   (r1,t1) : r1 * t2 = { r1.name = 1 }, t1.A 2
 > 
 > I'd rather use different namings like "r1_name" and "r2_name" for the
 > field: although this requires me to always include the name of the type,
 > one cannot get confused either: it makes the sources easier to understand.

I don't find that argument very convincing; Ocaml _already_ allows type, value
and field label definitions to shadow each other, which many people consider a
cognitive burden. I don't have an opinion on that issue; I'm just trying to be
consistent with the way Ocaml treats bindings currently, and add a little bit
more flexibility.

In fact, I don't see how this makes programs any less readable.

If you don't add this mechanism, then the rule remains, "an identifier X
refers to the last definition of X in scope".

If you do add this mechanism, then that doesn't change (since the identifier
[path] "t.x" is still distinct from "x").

The only problem I see is that for the toplevel you will lose the ability to
throw away bindings that got shadowed by newer definitions, even if they never
appear inside some existing binding. But as far as I know, Ocaml's top-level
doesn't garbage collect old bindings anyway, so it's a non-issue for now
(unless the implementors intend to change this detail in the future).

-- 
Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14,
PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31
(030) 251-3791

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

[Markus Mottl]

On Sat, 22 Jul 2000, Frank Atanassow wrote:
>  > But how about "capturing logical invariants"? You need both ways of
>  > information hiding there: restricting the number of exported functions
>  > *and* restricting their types! Otherwise there could be ways to destroy the
>  > invariant.
> 
> Can you be more specific about "capturing logical invariants"? I don't know
> quite what you mean.

If you have axioms that specify invariant properties about the types and
functions in question. E.g. that removing an element from a set results
in a set that does not contain it and that this is true for all sets.

Exporting auxiliary functions from the module might allow the programmer
to violate this condition. The same is true for not restricting the types
of the functions. Therefore, you need both means of information hiding to
guarantee correctness (i.e. the properties in question).

> An instance I can think of where access to names could have semantic
> significance is if it has to do with generativity. I hate generativity with a
> passion, but eliminating it from ML modules would require a wholesale revision
> of the module system, which it is not my object to propose here. So, I will
> concede that generativity may cause name access to acquire semantic
> significance. (But I hope you agree that it is at least desirable that names
> and namespaces should have no semantic significance whatsoever.)

I guess you mean that it is only the structure of the module that counts
and not the naming? But how about ambiguities then? You need a way to
refer to the right function, whatever, if it has the same signature as
another one.

>  > I'd rather use different namings like "r1_name" and "r2_name" for the
>  > field: although this requires me to always include the name of the type,
>  > one cannot get confused either: it makes the sources easier to understand.
> 
> I don't find that argument very convincing; Ocaml _already_ allows type, value
> and field label definitions to shadow each other, which many people consider a
> cognitive burden. I don't have an opinion on that issue; I'm just trying to be
> consistent with the way Ocaml treats bindings currently, and add a little bit
> more flexibility.

There's not much you can do about shadowing of value bindings unless you
prohibit it which would cause other problems: you'd have to invent a new
name each time even if you just want to "transform" a value using the same
name - this could cause horror if you wanted to add such a transformation
in the middle of a function body...

What concerns type names: I guess this is a consequence of having
an "open"-statement for modules, which shadows previous type
declarations. Otherwise, forbidding it would probably be a good idea
since its scope is the whole module from the point of definition.

Now, accessing fields more flexibly is surely possible. The question is
whether adding this feature is really of so much help: the only case
where it pays off is when you have large records which share a great
deal of names. 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...

> In fact, I don't see how this makes programs any less readable.

It adds another construct that people have to learn. Reading constructs
that you are not familiar with is confusing. I bet that there are plenty
of people who do not even know about the "with"-construct for records...

> If you don't add this mechanism, then the rule remains, "an identifier X
> refers to the last definition of X in scope".

Yes.

> If you do add this mechanism, then that doesn't change (since the identifier
> [path] "t.x" is still distinct from "x").

Right. But you have to invent additional syntax for doing this. Even
though it seems to be a rather marginal addition, it also adds to making
the language more complex. I haven't felt the need for it so far, but
if other people have other requirements, they are free to ask for it...

Regards,
Markus Mottl

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

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

[Frank Atanassow]

Markus Mottl writes:
 > > Can you be more specific about "capturing logical invariants"? I don't
 > > know quite what you mean.
 > 
 > If you have axioms that specify invariant properties about the types and
 > functions in question. E.g. that removing an element from a set results in
 > a set that does not contain it and that this is true for all sets.
 > 
 > Exporting auxiliary functions from the module might allow the programmer to
 > violate this condition. The same is true for not restricting the types of
 > the functions. Therefore, you need both means of information hiding to
 > guarantee correctness (i.e. the properties in question).

I don't think that has anything to do with hiding values, or if it does, it
needn't. Suppose I want to define a type of sets, but I don't want to reveal
the fact that I'm using lists to do it.

  module type SET =
    sig
      type 'a set
      val union : 'a set -> 'a set -> 'a set
    end

  module ListSet =
    struct
      type 'a set = 'a list
      let removeDup m = ...
      let union m n = removeDup (m
      @ n)
    end

  module Set = ListSet : SET

(removeDup doesn't break the abstraction since it's the identity on sets, but
for the sake of brevity suppose it did.)

Here is my rendition of what the signature restriction to SET is doing:

  1) It existentially introduces a new type 'a Set.set, whose witness is 'a
     list, and at the same time introduces a new value Set.union, with
     occurrences of 'a ListSet.list replaced by 'a Set.set in its type, whose
     witness is ListSet.union.

  2) It hides all the names defined in ListSet. This includes ListSet.union as
     well as ListSet.removeDup (and ListSet.set).

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

I think that this is close to what Ocaml does, though I wouldn't swear to it.

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.

 > I guess you mean that it is only the structure of the module that counts
 > and not the naming? But how about ambiguities then? You need a way to refer
 > to the right function, whatever, if it has the same signature as another
 > one.

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

 > >  > I'd rather use different namings like "r1_name" and "r2_name" for the
 > >  > field: although this requires me to always include the name of the
 > >  > type, one cannot get confused either: it makes the sources easier to
 > >  > understand.
 > > 
 > > I don't find that argument very convincing; Ocaml _already_ allows type,
 > > value and field label definitions to shadow each other, which many people
 > > consider a cognitive burden. I don't have an opinion on that issue; I'm
 > > just trying to be consistent with the way Ocaml treats bindings
 > > currently, and add a little bit more flexibility.
 > 
 > There's not much you can do about shadowing of value bindings unless you
 > prohibit it which would cause other problems: you'd have to invent a new
 > name each time even if you just want to "transform" a value using the same
 > name - this could cause horror if you wanted to add such a transformation
 > in the middle of a function body...

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.

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

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

 > Now, accessing fields more flexibly is surely possible. The question is
 > whether adding this feature is really of so much help: the only case where
 > it pays off is when you have large records which share a great deal of
 > names.

It pays off when you have records which share names, period.

In that case it improves readability, in the sense that "r.label" is easier to
read than "r.prefix_label".

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

 > > In fact, I don't see how this makes programs any less readable.
 > 
 > It adds another construct that people have to learn. Reading constructs
 > that you are not familiar with is confusing. I bet that there are plenty of
 > people who do not even know about the "with"-construct for records...

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.

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.

-- 
Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14,
PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31
(030) 251-3791

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

[Markus Mottl]

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

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

[Frank Atanassow]

Markus Mottl writes:
 > 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.

I guess you mean a situation like this:

  module type FLAG =
    sig
      type t
      val from : bool -> t
      val to : t -> bool
    end

  module Flag3 =
   struct
     type t = On | Off | Undecided
     let from = function true -> On | false -> Off
     let to = function On -> true | Off -> false
   end

  module Flag : FLAG = Flag3    

The thinking would be, then, that with the concrete representation I could
construct a value Flag3.Undecided : Flag3.t which would cause Flag3.to to
fail, whereas with Flag I cannot ever construct an Undecided variant, so
Flag.to is effectively total. Correct?

But while Flag3.Undecided is admittedly special (being a constructor), it is
nevertheless an ordinary function. Hence it can be included in the scope of
the quantification or not. If I quantify over it, then Flag = Flag3. If I
don't quantify over it, but still include it in the signature, then
Flag.Undecided : Flag3.t, so Flag.t only exposes two variants.

Do you still think there is a situation where name-hiding is necessary in
addition to type abstraction?

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

I'm not sure I understand, but I think you are imagining a partial, auxiliary
function which is only used internally. In that case, you can always define it
locally, in the scope of a let-expression, say.

However, if you have to use this function (call it aux) multiple times in
different top-level definitions, you will end up convoluting your code.
E.g.,

  module M =
    struct
      let aux = ...
      let f1 = ... aux ...
      let f2 = ... aux ...
    end

becomes

  module M =
    struct
      let (f1,f2) =
        let aux = ...
        in  let f1 = ... aux ... in
            let f2 = ... aux ... in
            (f1, f2)
    end

which is admittedly unsavory.

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

OK, this is a situation that doesn't fit my model. If you include a function
in the scope of the quantification, you have to substitute all the occurrences
in its type signature of the concrete type with the new abstract type.

BTW, this discussion is no longer relevant to the discussion on field label
syntax, so let's take it to e-mail from now on, OK?

 > >  > 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; ... }

I see. You mean a "declaration" within the record-building syntax. Yeah, it is
better to avoid repetition, and avoid making the programmer remember which
labels are used in multiple record types.

BTW, here is the URL of a previous discussion on this subject in the archives:

  http://pauillac.inria.fr/caml/caml-list/1136.html
  http://pauillac.inria.fr/caml/caml-list/1203.html (follow the thread)

(There is also a long post somewhere by Xavier on the type inference problem
with records, but I couldn't find it.)

A solution suggested in the archives is to allow type declarations like:

  type point = Pt of { x: float; y: float }

(Incidentally, this is how it is done currently in Haskell.)

-- 
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791

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

[Alan Schmitt]

Hi,

>BTW, here is the URL of a previous discussion on this subject in the archives:
>
>  http://pauillac.inria.fr/caml/caml-list/1136.html
>  http://pauillac.inria.fr/caml/caml-list/1203.html (follow the thread)
>

Why not use the new archiving of the list:
http://pauillac.inria.fr/caml/archives/199902/msg00097.html
http://pauillac.inria.fr/caml/archives/199903/msg00049.html

>(There is also a long post somewhere by Xavier on the type inference problem
>with records, but I couldn't find it.)

This archiving system comes with a pretty good search engine:
http://pauillac.inria.fr/bin/wilma/caml-list

Alan Schmitt

--
The hacker: someone who figured things out and made something cool happen.