caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Oleg <>
Subject: Re: [Caml-list] Breaking type abstraction of modules
Date: Sat, 27 Feb 2021 19:50:13 +0900	[thread overview]
Message-ID: <20210227105013.GA2146@Melchior.localnet> (raw)
In-Reply-To: <>

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

  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}

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

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

   let _ = match teq A1.AT Int with
           | Some Refl -> (!ar : int list) 
           | _ -> assert false

- : int list = [2; 1]

  reply	other threads:[~2021-02-27 10:45 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 [this message]
2021-02-27 11:37     ` Leo White
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:

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

  git send-email \
    --in-reply-to=20210227105013.GA2146@Melchior.localnet \ \ \ \
    --subject='Re: [Caml-list] Breaking type abstraction of modules' \

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

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).