[Caml-list] Re: Reifying types

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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égoire 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,  <oleg@okmij.org> 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 =
>           | 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 Yallop
>    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 =
>   (Ctype.repr (Ctype.expand_head_opt env (Ctype.correct_levels ty))).desc
>
> let has_int_type exp =
>   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
>
>
>