Loading ...
Sorry, an error occurred while loading the content.

const like type qualifier ?

Expand Messages
  • rixed@happyleptic.org
    Hello ! Suppose I m writing a module signature for a data structure, let s say a set : module type SET = sig type a t val is_empty : a t - bool val insert :
    Message 1 of 2 , Dec 4, 2010
    • 0 Attachment
      Hello !

      Suppose I'm writing a module signature for a data structure, let's say
      a set :

      module type SET =
      sig
      type 'a t
      val is_empty : 'a t -> bool
      val insert : 'a t -> 'a -> 'a t
      (* etc... *)
      end

      How could I specify that the set implementation must be persistent ?
      I'd ideally like something like :

      val insert : const 'a t -> 'a -> 'a t

      that states explicitly that the given set is not supposed to be altered.
      Of course such a keyword would not be a good idea since we what we really
      want is the set items to be the same (but the implementation is allowed
      to update the set for efficiency, for instance if it's a tree it's allowed
      to rebalance it as long as the observable properties of the set are preserved).
      I know there is no such const keyword but maybe there is a well known
      trick or convention to specify that an implementation must be persistent
      (and ideally having the compiler enforce this in some way) ?
    • vincent
      Hi, the simplest and most natural way to have a set that must be persistent is to define its type without using any reference or record with mutable field.
      Message 2 of 2 , Dec 4, 2010
      • 0 Attachment
        Hi,

        the simplest and most natural way to have a set that must be persistent is to define its type without using any reference or record with mutable field. Then of course your set cannot be modified! Now I don't think you can impose this in the interface.

        Then if you even want to have a much higher-level semantics such as "it can be equal up to rebalancing", this seems to me as clearly impossible for the compiler. How could it check that an implementation matches an interface? This requires very complex reasoning, far beyond what the compiler is able to achieve (and probably far beyound any reasonably defined computable function...).

        If you really really want to enforce this, you can do it at runtime.
        More precisely you could require SET to provide a function "eq_up_to_rebalancing" (or just "eq" if this equality should be the standard one) and a function "copy" that returns a copy of a given set (of course this function would be trivial if the datatype is really immutable) and then implement a functor taking the candidate implementation of SET and returning a "verified" version of it as follows:

        module CheckSet(S: SET) =
        struct
        include S

        let insert x y =
        let x' = S.copy x in
        let res = S.insert x y in
        if S.eq_up_to_rebalancing x x' then res else failwith "Non persistent function detected"
        end

        Then you can be sure that CheckSet(MySetImplementation) has the property that you want. But I guess your need of safety won't go until such heaviness, am I right? :)

        Cheers,
        V.

        --- In ocaml_beginners@yahoogroups.com, rixed@... wrote:
        >
        > Hello !
        >
        > Suppose I'm writing a module signature for a data structure, let's say
        > a set :
        >
        > module type SET =
        > sig
        > type 'a t
        > val is_empty : 'a t -> bool
        > val insert : 'a t -> 'a -> 'a t
        > (* etc... *)
        > end
        >
        > How could I specify that the set implementation must be persistent ?
        > I'd ideally like something like :
        >
        > val insert : const 'a t -> 'a -> 'a t
        >
        > that states explicitly that the given set is not supposed to be altered.
        > Of course such a keyword would not be a good idea since we what we really
        > want is the set items to be the same (but the implementation is allowed
        > to update the set for efficiency, for instance if it's a tree it's allowed
        > to rebalance it as long as the observable properties of the set are preserved).
        > I know there is no such const keyword but maybe there is a well known
        > trick or convention to specify that an implementation must be persistent
        > (and ideally having the compiler enforce this in some way) ?
        >
      Your message has been successfully submitted and would be delivered to recipients shortly.