caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: "Leo White" <leo@lpw25.net>
To: caml-list@inria.fr
Subject: Re: [Caml-list] Breaking type abstraction of modules
Date: Sat, 27 Feb 2021 11:37:27 +0000
Message-ID: <de6adcbd-bd7b-45b9-9d1b-e8ff5a32a4f4@www.fastmail.com> (raw)
In-Reply-To: <20210227105013.GA2146@Melchior.localnet>

Hi Oleg,

I don't really understand your unease here. Firstly, this isn't some unexpected aspect of extensible variants, it is the main reason that I proposed adding them to the language. Secondly, you can easily create similar behaviour without extensible variants. For example, here we do the same thing without extensibility (code not actually tested or even type-checked):

type (_, _) eq = Refl : ('a, 'b) eq

module Rep : sig
  type 'a t
  val int : int t
  val string : string t
  val destruct : 'a t -> 'b t -> ('a, 'b) eq option
end = struct
  type 'a rep =
    | Int : int rep
    | String : int rep
  let int = Int
  let string = String
  let destruct (type a b) (a : a t) (b : b t) =
    match a, b with
    | Int, Int -> Some Refl
    | String, String -> Some Refl
    | _, _ -> None
end

let counter = ref 0
 
module AF() : sig
  type t             (* Here, t is abstract *)
  val rep : t Rep.t
  val x : t
end = struct
  type t = int        (* Here, t is concrete int *)
  let rep = Rep.int
  let x = incr counter; !counter
end

module A1 = AF ()
module A2 = AF ()

let ar = ref [A1.x]
 
let _ =
   match Rep.destruct A1.rep A2.rep with 
    | Some Refl -> ar := A2.x :: !ar
    | _ -> assert false

Extensible variants make these kinds of type representations much more useful, but they don't change the nature of what you can do.

Regards,

Leo

On Sat, 27 Feb 2021, at 10:50 AM, Oleg wrote:
> 
> Gabriel Scherer wrote:
> 
> > Is this very different from exposing the GADT equality directly in the
> > module interface?
> >
> > module A : sig
> >   type t (* abstract *)
> >   val reveals_abstraction : (int, t) eq (* or maybe not *)
> >   val x : t
> > end
> 
> I think it is different: if you are declaring reveals_abstraction
> (that is, the witness of the type equality) in your _interface_, you are
> effectively declaring to the users that "type t = int", no? 
> 
> Thinking about this more, I come across the following example that
> better illustrates my unease. The example concerns type generativity,
> and explicit promise by generative functors to create fresh,
> incompatible types. It seems this promise has to come with some
> conditions attached.
> 
> Assuming the same preamble with teq as before, consider the following
> code
> 
>   let counter = ref 0
> 
>   module AF() : sig
>     type t             (* Here, t is abstract *)
>     type _ trep += AT : t trep
>     val x : t
>    end = struct
>     type t = int        (* Here, t is concrete int *)
>     type _ trep += AT : t trep
>     let x = incr counter; !counter
> 
>     let () = 
>      let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y -> 
>        match (x,y) with 
>        | (AT,AT) -> Some Refl 
>        | (AT,Int) -> Some Refl      (* Since t = int, it type checks *)
>        | (Int,AT) -> Some Refl
>        | _ -> None 
>     in teq_extend {teq=teq}
>   end
> 
> Here, AF is a generative functor. The type t is defined
> abstract. Hence each instantiation of AF should come with its own,
> fresh and incompatible with anything else type t. (For the same of
> example below, the value x is also made fresh).
> 
> Here are the two instances of the functor.
> 
>    module A1 = AF ()
>    module A2 = AF ()
> 
> Indeed, the types A1.t and A2.t are different: putting A1.x and A2.x
> into the same list predictably fails.
> 
>    let _ = [A1.x; A2.x]
> 
> Line 1, characters 15-19:
> 1 | let _ = [A1.x; A2.x];;
>                    ^^^^
> Error: This expression has type A2.t but an expression was expected of type
>          A1.t
> 
> 
> But now it succeeds:
> 
>    let ar = ref [A1.x]
> 
>    let _ = match (teq A1.AT Int, teq A2.AT Int) with 
>             | (Some Refl,Some Refl) -> ar := A2.x :: !ar
>             | _ -> assert false
> 
>    let _ = !ar
> - : A1.t list = [<abstr>; <abstr>]
> 
> The list in ar really has A2.x and A1.x as elements, which we can confirm
> as
> 
>    let _ = match teq A1.AT Int with
>            | Some Refl -> (!ar : int list) 
>            | _ -> assert false
> 
> - : int list = [2; 1]
>

  reply	other threads:[~2021-02-27 11:37 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-02-26 16:28 Oleg
2021-02-26 16:29 ` Gabriel Scherer
2021-02-27 10:50   ` Oleg
2021-02-27 11:37     ` Leo White [this message]
2021-03-02  8:08       ` [Caml-list] [ANN] latest batteries release: v3.3.0 Francois Berenger

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=de6adcbd-bd7b-45b9-9d1b-e8ff5a32a4f4@www.fastmail.com \
    --to=leo@lpw25.net \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list

This inbox may be cloned and mirrored by anyone:

	git clone --mirror http://inbox.vuxu.org/caml-list
	git clone --mirror https://inbox.ocaml.org/caml-list

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 caml-list caml-list/ http://inbox.vuxu.org/caml-list \
		caml-list@inria.fr
	public-inbox-index caml-list

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.caml-list


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git