[TYPES] breaking abstraction with ML exceptions

[Oleg]

I'm in agreement with Derek. In OCaml at least, one can quickly gets
used to the fact that an abstract type does not mean a fresh or a
globally unique type. An abstract type may turn out equal to something
rather concrete. If one needs something globally unique, one should
use generative functors (and extensible data types, as Gabriel indicated).

Your example is a good illustration, in case of exceptions. But I would
not blame exceptions per se: for example, references may just as well
reveal the identity of what looks like an abstract type.

A side remark first: I would find your example more compelling
(at least in OCaml) in a slightly re-written form:

exception C
module F(S:sig exception A end) = struct
  let r = try raise S.A with C -> 42
end
let module M = F(struct exception A = C end) in M.r  (* 42 *)

The body of the functor receives some abstract exception A, and is
able to find out it is being equal to something concrete.

Here is the similar example with references:

let x = ref 100
module F(S:sig type t val y:t ref end) = struct
  let r =
        let xold = !x in
        x := xold + 1;
        let ynew = !S.y in
        x := xold;
        if not (!S.y = ynew) then print_string "t was int"
end
;;
let module M = F(struct type t = int let y = x end) in M.r;;

Again, the body of the functor was able to find out that the abstract
type t is actually an int. So, if the test comes out positive, by
assigning to S.y (and then reading from x), the functor can find the
`true' value of any value of the supposedly abstract type t.


I have learned of this trick from a rather old message, which I
append for the sake of history. That message showed the SML code.


> From: jmv16 at cornell.edu (Jeffrey M. Vinocur)
Newsgroups: comp.lang.functional
Subject: Re: Type Identification in ML
Date: Thu, 24 Oct 2002 11:37:56 +0000 (UTC)
Organization: Cornell University
Sender: jeff at litech.org
Message-ID: <ap8m2k$1d1$2 at puck.litech.org>
References: <ap809l$sldec$1 at ID-100778.news.dfncis.de>
X-Trace: puck.litech.org 1035459476 1441 208.48.41.224 (24 Oct 2002 11:37:56 GMT)
NNTP-Posting-Date: Thu, 24 Oct 2002 11:37:56 +0000 (UTC)
X-Newsreader: trn 4.0-test76 (Apr 2, 2001)
Originator: jeff at litech.org (Jeffrey M. Vinocur)


In article <ap809l$sldec$1 at ID-100778.news.dfncis.de>,
John S. Novak, III <jsn at cegt201.bradley.edu> wrote:
>Is there, in ML a way to define a function which, if given an int,
>returns true, but given anything else returns false?  Likewise, is there
>a way to define a function which, if given a list (of any type, or of a
>specified type) returns true, but given anything else returns false?

Nope.  No way to provide a type for such a function.

Practical people can stop reading here.

However, there is the following interesting bit which has the
remarkable behavior that it can distinguish between types in a
contrived circumstance.  (A 'a ref * int ref -> bool function
would be "expected" to be ignoring its first argument.)


fun g (x:'a ref, y:int ref) : bool =
  let
    val () = y := 0
    val z  = !x
    val () = y := 1
    val () = x := z
  in
    !y = 0
  end

- g(ref "hi", ref 3);
val it = false : bool
- val x = ref 3;
val x = ref 3 : int ref
- g(x,x);
val it = true : bool