[Caml-list] Reifying types

[Caml-list] Reifying types

[oleg]

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

[Caml-list] Re: Reifying types

[Gabriel Scherer]

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
>
>
>