From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 80AD3800B6 for ; Tue, 3 Jan 2017 15:06:13 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nils.becker@bioquant.uni-heidelberg.de; spf=None smtp.mailfrom=nils.becker@bioquant.uni-heidelberg.de; spf=None smtp.helo=postmaster@relay.uni-heidelberg.de Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of nils.becker@bioquant.uni-heidelberg.de) identity=pra; client-ip=129.206.100.212; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nils.becker@bioquant.uni-heidelberg.de"; x-sender="nils.becker@bioquant.uni-heidelberg.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of nils.becker@bioquant.uni-heidelberg.de) identity=mailfrom; client-ip=129.206.100.212; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nils.becker@bioquant.uni-heidelberg.de"; x-sender="nils.becker@bioquant.uni-heidelberg.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@relay.uni-heidelberg.de) identity=helo; client-ip=129.206.100.212; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nils.becker@bioquant.uni-heidelberg.de"; x-sender="postmaster@relay.uni-heidelberg.de"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AvZp4gBVPFKR/7C0FkCfjrcOXEpHV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbBGCt8tkgFKBZ4jH8fUM07OQ6PG8HzVbqsvQ+Fk5M7V0Hycfjs?= =?us-ascii?q?sXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6?= =?us-ascii?q?KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG5oAnLq8Ubj4RuJ6Y1xxDUvnZGZu?= =?us-ascii?q?NayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnD?= =?us-ascii?q?VhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0ji?= =?us-ascii?q?oMKjg0+3zVhMNtlqJWuAyvqRxizYDXbo+aOvVxcb/Sc94BWWpMXNxcWzBdDo6y?= =?us-ascii?q?bYYCCfcKM+ZCr4n6olsDtQOwBQioBOP01zRFm2H50rE50+s/CwHNwQstH9QPsH?= =?us-ascii?q?TQt9X5LrwdXv6pw6nL0zrDdehb1iz86IjPaxAhvOuDXbRsccbL1EkvEQLFgkyQ?= =?us-ascii?q?qYP7PjOay/oCs2yA4OV+T+KvhHQrpBxvrTW2wMonl4rHhpoNx1zZ6yl0xJw5Kc?= =?us-ascii?q?OkREN6e9KoDYdcuz2AO4doX88uXXlktDskxrACo5K3YjQGxZU9yxLBZPGKc5KE?= =?us-ascii?q?7g/sWeufJzpzmWhrd6ilhxmo9Eit0u38Wdew0FZNtidFiMfDtnQX2B3T8MSHV/?= =?us-ascii?q?19/ka41TaPyQ/T6/xLLl4wlaXANZEh2LEwmoAOvkvdBiP2mUP2g7GKdkg85+Sk?= =?us-ascii?q?9eDqbq/4qpOANoJ4kBzyPrgylsClH+g0LxYCU3Ce+eum1b3j+UP5QK9Njv0ziq?= =?us-ascii?q?TZtpHaJcAApqKjGABazJos6xWhADe8y9kXhngHLFVceBKalYfpPU3OLOrlDfe5?= =?us-ascii?q?glSgiTdryO7HPrL8HJrNKmPMn6n7fbZy8UJT1RQ8wchF551IErEBPO7zWkjpud?= =?us-ascii?q?PEFBA5Ngi0z//jCNV8zYMeRXmCArSZMaPXqV+H/PgjI+iKZI8PuTbyMeIp5/D0?= =?us-ascii?q?jSxxpVhIN6Kg2J9SbHGjAtxnJV+YaDzimJ1JRWwDuw57SO3xlHWDVyRSbjC8Rf?= =?us-ascii?q?RvyCs8DdeADIPYDqqgi7+Mxm/vGJxSfSZMB1uPHG3AfYSDQuoFbj7UP8lg1zwJ?= =?us-ascii?q?VLSsT4Uszx7ouAKsmOkvFfbd5iBN7cGr79Ny/eCGzRw=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BnAABrr2tYh9RkzoFeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgwwBAQEBAZBTk1STDIQXhiKBSUIRAQEBAQEBAQEBAQESAQEBCgs?= =?us-ascii?q?JCR0lC4IzGIIfBCQESwwWGgImAl8NCAEBF4hNCJ8NkACBazqKcIELhTqCAgiCV?= =?us-ascii?q?4RGgkwLLYJdBZp9gXqZY4Y2kj01gSmDZQELAVOBaokvAQEB?= X-IPAS-Result: =?us-ascii?q?A0BnAABrr2tYh9RkzoFeHAEBBAEBCgEBFwEBBAEBCgEBgww?= =?us-ascii?q?BAQEBAZBTk1STDIQXhiKBSUIRAQEBAQEBAQEBAQESAQEBCgsJCR0lC4IzGIIfB?= =?us-ascii?q?CQESwwWGgImAl8NCAEBF4hNCJ8NkACBazqKcIELhTqCAgiCV4RGgkwLLYJdBZp?= =?us-ascii?q?9gXqZY4Y2kj01gSmDZQELAVOBaokvAQEB?= X-IronPort-AV: E=Sophos;i="5.33,455,1477954800"; d="scan'208";a="206809584" Received: from relay.uni-heidelberg.de ([129.206.100.212]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 03 Jan 2017 15:05:35 +0100 Received: from ix.urz.uni-heidelberg.de (cyrus-portal01.urz.uni-heidelberg.de [129.206.100.176]) by relay.uni-heidelberg.de (8.15.2/8.15.2) with ESMTP id v03E5Wev021792 for ; Tue, 3 Jan 2017 15:05:32 +0100 Received: from extmail.urz.uni-heidelberg.de (extmail.urz.uni-heidelberg.de [129.206.100.140]) by ix.urz.uni-heidelberg.de (Postfix) with ESMTPS id 7F43C21CDEF2 for ; Tue, 3 Jan 2017 15:05:32 +0100 (CET) Received: from bqdyn245_127.bioquant.uni-heidelberg.de (bqdyn245_127.bioquant.uni-heidelberg.de [129.206.245.143]) (authenticated bits=0) by extmail.urz.uni-heidelberg.de (8.15.2/8.13.1) with ESMTPSA id v03E5V06005688 (version=TLSv1.2 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Tue, 3 Jan 2017 15:05:32 +0100 X-Mozilla-News-Host: news://news.gmane.org:119 To: "caml-list@inria.fr" From: Nils Becker Message-ID: <40536bf7-5d7f-5528-80c2-45ed5d157d00@bioquant.uni-heidelberg.de> Date: Tue, 3 Jan 2017 15:05:31 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.11; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit X-Validation-by: nils.becker@bioquant.uni-heidelberg.de Subject: Re: [Caml-list] GADT+polymorphic variants quirk hi, i am the OP of the stackoverflow question referred to by anton. > I would suggest avoid using polymorphic variants here, using rather > a simple encoding: > > type whole = Whole > type general = General > > type _ num = > | I : int -> _ num > | F : float -> general num i tried this simpler proposal and it does seem to work nicely. however, what i'm really interested in is encoding somewhat more elaborate subtyping relationships. for example, how would you handle the case where there is a 'rational' number type inbetween integers and reals? i don't see how your proposal can be generalized to that? i tried to generalize the solution proposed by anton like this: type integer = [ `Integer ] type rational = [ integer | `Rational ] type real = [ rational | `Real ] type _ num = | N : int -> [> integer ] num | Q : int * int -> [> rational ] num | R : float -> real num and then a generalized module implementation like this: module M : sig val mult : ([< real] as 'a) num -> 'a num -> 'a num val to_int : integer num -> int val to_num_denom : rational num -> int * int val to_float : real num -> float end = struct let mult : type a. a num -> a num -> a num = fun a b -> match a, b with | _, N m -> (match a with | N n -> N (n * m) | R n -> R (n *. float_of_int m) | Q (n, n') -> Q (n * m, n')) | _, R m -> (match a with | N n -> R (float_of_int n *. m) | R n -> R (n *. m) | Q (n, n') -> R (float_of_int n /. float_of_int n' *. m)) | _, Q (m, m') -> (match a with | N n -> Q (n * m, m') | R n -> R (n *. float_of_int m /. float_of_int m') | Q (n, n') -> Q (n * m, n' * m')) let to_int : integer num -> int = fun (N n) -> n let to_num_denom : rational num -> int * int = function | N n -> (n, 1) | (Q (n, n')) -> (n, n') let to_float = function | N n -> float_of_int n | Q (n, n') -> float_of_int n /. float_of_int n' | R n -> n end where i tried to replicate the sub-case matching to work around the type-checker's limitations. unfortunately this does not typecheck; in the same way that was described above: Error: This expression has type real num but an expression was expected of type a num Type real = [ `Integer | `Rational | `Real ] is not compatible with type a = [> `Integer ] The second variant type does not allow tag(s) `Rational, `Real so it seems that it's not really viable to try to build something along these lines. is there a better way to do this kind of subtyping in current ocaml? n.