Re: [Caml-list] Late adding of type variable constraints

[Mikhail Mandrykin <mandrykin@ispras.ru>]

On Friday, September 11, 2015 11:56:33 AM Markus Mottl wrote:
> But wouldn't this require making Newtype1 a generative
> functor (i.e. adding "()")?  Otherwise the type "t" could be seen as
> equivalent if Newtype1 is applied to the same module more than once,
> which would allow for more than one "Mk" case and could hence cause a
> runtime match error.

Yes, indeed.

module T : sig type t = int end;;
module N1 = Newtype0(T);;
module N2 = Newtype0(T);;
# N1.prj @@ N2.inj 0;;
Exception: Match_failure ("//toplevel//", 10, 10).

With generative functors this causes a typing error.  In this case it's also 
possible to use even simpler encoding without open types (`('a, ... ('z, nil) 
app) ...) app) t'):

type ('p, 'f) app = App of 'p * 'f
type nil

module Newtype1 (T : sig type 'a t end) =
struct
  type 'a t = Mk : 'a T.t -> (('a, nil) app) t
  let inj v = Mk v
  let prj (Mk v) = v
end

-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru