[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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: jm...@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: j...@litech.org Message-ID: <ap8m2k$1d1$2...@puck.litech.org> References: <ap809l$sldec$1...@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: j...@litech.org (Jeffrey M. Vinocur) In article <ap809l$sldec$1...@id-100778.news.dfncis.de>, John S. Novak, III <j...@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