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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 0A4017ED5C for ; Thu, 2 Aug 2012 18:04:44 +0200 (CEST) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.54; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.54 as permitted sender) identity=mailfrom; client-ip=209.85.213.54; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-yw0-f54.google.com) identity=helo; client-ip=209.85.213.54; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-yw0-f54.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtkBAOujGlDRVdU2jWdsb2JhbABFuQQIIgEBAQEJCQsJEgYjgiABAQEEEgITGQEbHQEDDAYFCw0uIgERAQUBHBkJGYdbAQMMC54YCQOMI4JxhVIKGScNV4hxAQUMiz2HBAOITYx6gRSJeYMjPoQe X-IronPort-AV: E=Sophos;i="4.77,702,1336341600"; d="scan'208";a="152310526" Received: from mail-yw0-f54.google.com ([209.85.213.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Aug 2012 18:04:43 +0200 Received: by yhfs35 with SMTP id s35so13023065yhf.27 for ; Thu, 02 Aug 2012 09:04:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=flIZGgCksLvkyQHdC6bt8iTGRTT+jduVMY4yznApcpI=; b=jFQTs8owrMXG76XMS/0anbb+x+xC5sqUwDu1ZDvb9zQqzFrSgfWdtahdpcKRkplsC6 IDUakGioY9lyanPQd02u1TsR9TwwChKR16X9t9kv+Gj7U75i2DRz9NXRBv3FqKC/F7Qt hTlic9IUOHl50kR4Q8pNoIpwM/6EkZuJepx6wlhUVSCBglVkSwUeDr1H50KwOFxi2h7H WrIfB3V5/3uf7Ok4KmaKPzV/z0z1Ni3GmgnyAw+v67lVg45l/g00Xb3CPwLxXtOlhrvt 9ZMImCGIHY2qwY/xKUIIcoiEjem/PgyYkUxd3YzUF8VKYP0hYxI+s7Tzjl4jKqN3duLO rOzQ== Received: by 10.50.217.137 with SMTP id oy9mr4503947igc.56.1343923481682; Thu, 02 Aug 2012 09:04:41 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.94.39 with HTTP; Thu, 2 Aug 2012 09:04:00 -0700 (PDT) In-Reply-To: <20120802074653.44053.qmail@www1.g3.pair.com> References: <20120802074653.44053.qmail@www1.g3.pair.com> From: Gabriel Scherer Date: Thu, 2 Aug 2012 09:04:00 -0700 Message-ID: To: oleg@okmij.org Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Subject: [Caml-list] Re: Reifying types The 'a repr you're discussing, as a form of dynamic type information, is closely related to what Alain Frisch demonstrated in this blog post (and presentation): http://www.lexifi.com/blog/dynamic-types It is indeed a very interesting use case for GADTs, and Alain has some neat ideas on how to represent richer non-completely-structural types like records. Of course, to be convenient to use such a dynamic type representation should come with a language construct to ask the type-checker to produce it from inferred type information. Gr=E9goire Henry and Pierre Chambart have a reasonably advanced prototype implementation of this technique: http://gitorious.org/ocaml-ty They will talk about it at the OCaml Users and Developers Workshop ( http://oud.ocaml.org/2012/ ). Indeed the -bin-annot output is much more sophisticated and difficult to use correctly, and it could be interesting to provide a userland library to convert between the two representations. On Thu, Aug 2, 2012 at 12:46 AM, wrote: > > Gabriel Scherer wrote: >> The new 4.00 release has added fairly interesting feature relying on >> the compiler internals: the new -bin-annot option allowing to export >> and manipulate the typedtree of an OCaml program has already stirred >> interest among tools writers. > > That is indeed interesting! I admit I would like more, a primitive > > type_reify : 'a -> -'a repr > > which returns a representation of a type of any expression. Here > 'a repr is a representation of a type, represented as a GADT > > type _ repr =3D > | Int : int repr > | String: string repr > | Tuple : 'a repr * 'b repr -> ('a * 'b) repr > | List : 'a repr -> ('a list) repr > | Arrow : 'a repr * 'b repr -> ('a -> 'b) repr > ... > or using the representation described in the ML2010 paper with Jeremy Yal= lop > http://okmij.org/ftp/ML/first-class-modules/generics.ml > (It's best if 'a repr is non-variant or at least contra-variant to > prevent generalization). > > For example, > type_reify (1,"2") > will return a value of the type (int * string) repr. > type_reify ((fun x -> (x,"2")) (10 * 20)) > will return the same result. That is, the compiler builds the code > that, when run, constructs an 'a repr value > (describing the type of the expression at hand). > > Such type_reify function lets us do cool generic programming (as was > hinted in the generics.ml file above). We can do generic printing, > generic serialization and deserialization, etc. Incidentally, although > reifying expressions trivializes equational theory of the language (as > was first shown by Mitch Wand in his paper about fexpr), reifying > types (that is, extracting only part of the Typedtree, pertaining to > types) is safe in this respect. > > MetaOCaml has something like that: the brackets > .< exp >. : 'a code > for an expression of the type 'a. The value of 'a code is essentially > the Typedtree, from which one can extract the type information. I > always thought it would be wonderful to do generic programming in > (Meta)OCaml. I've been trying for years to get anyone interested in > this topic, without any success. BER MetaOCaml distribution does > include one example of generic programming, generic print. > http://okmij.org/ftp/ML/index.html#gprint > > The problem with using raw types from the Typedtree is the sheer > complexity of the type representation: the types contain aliases to > expand, links to chase, type variables to substitute, etc. For > example, to check if the type of an expression (a type associated with a > Typedtree node) is an int, we have to write the following incantations > > let scrape env ty =3D > (Ctype.repr (Ctype.expand_head_opt env (Ctype.correct_levels ty))).desc > > let has_int_type exp =3D > match scrape exp.exp_env exp.exp_type with > | Tconstr(p, _, _) -> Path.same p Predef.path_int > | _ -> false > > > Therefore, designing a good type representation like 'a repr will be > of great benefit. > > > Hongbo Zhang wrote: >> There are a lot of things to explore having compiler as libraries. >> (another advantage compared with Haskell) > > Perhaps you are not aware of GHC API -- which is the whole GHC > compiler available as a library. It is indeed very handy, and is used > a lot (for example, HINT -- Haskell interpreter, building module > graphs, building Intellisense, etc.). Thus OCaml and Haskell are on > par in offering compiler as a library (GHC API is must better > documented though). > > http://www.haskell.org/haskellwiki/GHC/As_a_library > http://www.haskell.org/ghc/docs/latest/html/libraries/ghc/GHC.html > http://www.haskell.org/ghc/docs/latest/html/libraries/ghc/index.html > > >