From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by sympa.inria.fr (Postfix) with ESMTPS id 979387F1C3
	for <caml-list@sympa.inria.fr>; Tue, 27 Nov 2012 15:08:08 +0100 (CET)
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  garrigue@math.nagoya-u.ac.jp) identity=pra;
  client-ip=133.6.130.5;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="garrigue@math.nagoya-u.ac.jp";
  x-sender="garrigue@math.nagoya-u.ac.jp";
  x-conformance=sidf_compatible
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  garrigue@math.nagoya-u.ac.jp) identity=mailfrom;
  client-ip=133.6.130.5;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="garrigue@math.nagoya-u.ac.jp";
  x-sender="garrigue@math.nagoya-u.ac.jp";
  x-conformance=sidf_compatible
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo;
  client-ip=133.6.130.5;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="garrigue@math.nagoya-u.ac.jp";
  x-sender="postmaster@mailhost.math.nagoya-u.ac.jp";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ap0EAO/HtFCFBoIF/2dsb2JhbAA7CcEwgh8BBScTCQE1Ag4LDiYSVwYTiAytAoMtgRAChjSJAQeMRYNOYYhfjSWQRIJ+
X-IronPort-AV: E=Sophos;i="4.83,328,1352070000"; 
   d="scan'208";a="163970083"
Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 27 Nov 2012 15:08:06 +0100
Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1])
	by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 7F09F6015;
	Tue, 27 Nov 2012 23:08:02 +0900 (JST)
Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1])
	by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 0E8AC251D;
	Tue, 27 Nov 2012 23:08:02 +0900 (JST)
DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha
Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157])
	by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id BA7B72503;
	Tue, 27 Nov 2012 23:08:01 +0900 (JST)
Content-Type: text/plain; charset=us-ascii
Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\))
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <87ip8rwbsc.fsf@golf.niidar.ru>
Date: Tue, 27 Nov 2012 23:08:00 +0900
Cc: caml-list@inria.fr
Content-Transfer-Encoding: 7bit
Message-Id: <1F656500-76AC-482F-BA08-A9BB8250D904@math.nagoya-u.ac.jp>
References: <87ip8rwbsc.fsf@golf.niidar.ru>
To: Ivan Gotovchits <ivg@ieee.org>
X-Mailer: Apple Mail (2.1499)
Subject: Re: [Caml-list] phantom types and identity function

On 2012/11/27, at 20:00, Ivan Gotovchits <ivg@ieee.org> wrote:

> 
> Hello,
> 
> These simple signature 
> 
>   module type T = sig
>       type 'a t constraint 'a = [< `A | `B ]
>       val init: [`A] t
>       val f: [`A] t -> [`B] t
>   end
> 
> can be used to constrain the following module
> 
>   module T : T = struct
>       type 'a t = unit constraint 'a = [< `A | `B]
>       let init = ()
>       let f x = x
>   end
> 
> where identity function successfully satisfies the constraint
> 
>   [`A] t -> [`B] t
> 
> but in the following module 
> 
>   module T : T = struct
>       type 'a t = {x:int} constraint 'a = [< `A | `B]
>       let init = {x=0}
>       let f x = x
>   end
> 
> the same identity function doesn't satisfy.

In the first case, a type abbreviation is used.
Since ('a t) expands to (unit), the parameter is completely
ignored, so that you can replace it by anything.

In the second case, you define a concrete type,
so that the parameter is not forgotten.
Note that you cannot even use subtyping for that:
  let f x = (x : [`A] t :> [`B] t)
fails too.
But there is an easy workaround, defining in two steps:
  type u = {x:int}
  type 'a t = u constraint 'a = [< `A | `B]

Jacques Garrigue