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

[Frank Atanassow <franka@cs.uu.nl>]

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