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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 791E77F7B4 for ; Mon, 10 Feb 2014 09:59:03 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.17.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.11; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At4BAJiU+FLU4xELnGdsb2JhbABZg0S6RIVfgQsWDgEBAQEBBg0JCRQogiUBAQUnCwFWCxgJHgcPBQ0bCiqHcAEDEQQJv0IfKw2IRheMZoIeFoMOgRQElj+Ba4EzhH8ShhuIcQ X-IPAS-Result: At4BAJiU+FLU4xELnGdsb2JhbABZg0S6RIVfgQsWDgEBAQEBBg0JCRQogiUBAQUnCwFWCxgJHgcPBQ0bCiqHcAEDEQQJv0IfKw2IRheMZoIeFoMOgRQElj+Ba4EzhH8ShhuIcQ X-IronPort-AV: E=Sophos;i="4.95,816,1384297200"; d="scan'208";a="57639662" Received: from mout.web.de ([212.227.17.11]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 10 Feb 2014 09:58:36 +0100 Received: from frosties.localnet ([149.172.224.32]) by smtp.web.de (mrweb001) with ESMTPSA (Nemesis) id 0MCZP8-1W4ZU91GKI-009Pvy for ; Mon, 10 Feb 2014 09:58:35 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.80) (envelope-from ) id 1WCmhG-00073L-M0 for caml-list@inria.fr; Mon, 10 Feb 2014 09:58:34 +0100 Date: Mon, 10 Feb 2014 09:58:34 +0100 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20140210085834.GC26593@frosties> References: <52F3C3A1.8060500@gmail.com> <52F3C710.4020500@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <52F3C710.4020500@gmail.com> User-Agent: Mutt/1.5.21 (2010-09-15) X-Provags-ID: V03:K0:/MO2pVtYCp7bwp2CHR5v42Au4XilrwNy6/5N8+6LmlI2hW0buMP h11c3qPGo/AxlEOZXYOV0TBHMlo/jt8cMMepoMbjd4hQzfW9BEEZ+UW98c25IiMXr2TwgPj eNOlOsYEmhtO97ILRokl8pM1yQ4qZs5hH1i8X+uhRf2dZepCXRlv/j508hsZh1NvkDnHrFJ wiidTP8t81UYOub2jL1Lg== Subject: Re: [Caml-list] Type of term On Thu, Feb 06, 2014 at 05:32:00PM +0000, Mário José Parreira Pereira wrote: > Hi Lukasz, > > Thank you for your answer but I really can't see how GADTs can help me. > > I was just simply wandering if there wasn't any OCaml function that > would work like: > type_of(let f x = x) = 'a->'a > > There is, something that would compute exactly the same outcome as > the Damas-Milner algorithm W. > > Bests, > Mário > > Em 06-02-2014 17:17, Lukasz Stafiniak escreveu: > >On Thu, Feb 6, 2014 at 6:17 PM, Mário José Parreira Pereira > >> > >wrote: > > > > Hi all, > > > > Is there any way to get the type of (part of) a program? Something > > like: > > type_of(M) = sigma > > computing the type of program M as sigma so I can pattern match it. > > > > > >No. However, if you really need this rather than being confused by > >programming patterns from Java / C# / C++, you should learn about > >GADTs. > >http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85 > > > >Cheers. # let f x = x;; val f : 'a -> 'a = # let g = (f : 'a -> 'a);; val g : 'a -> 'a = But this only unifies the types: # let f x = x + 1;; val f : int -> int = # let g = (f : 'a -> 'a);; val g : int -> int = To test for equality you need to use a module with signature (or .mli file): # module M : sig val g : 'a -> 'a end = struct let g = f end;; Error: Signature mismatch: Modules do not match: sig val g : int -> int end is not included in sig val g : 'a -> 'a end Values do not match: val g : int -> int is not included in val g : 'a -> 'a If you don't want a static compile time check then GADTs are the way to go. With GADTs you can construct runtime type informations, pass them as values and match on them. But you would have to construct the GADTs for every function you may want to type_of() or use a preprocessor module to do so implicitly. I think there is also a ocaml branch that adds such type values implicitly in the compiler. MfG Goswin