Hi Jacques

> written in ocaml).  I would like to be able to use arbitrary ocaml
> data-structures to represent some of my terms, when these terms are known to
> come from specific theories.  For example, I would like to use Bigint to
> represent integers, but without exposing that per se.

I'm not really sure I understand exactly what problem you are trying
to solve. But if it is flexible dynamic data structure that can
optionally be associated with a type tag you can take a look at the
source Symbiosis implementation

http://dvide.com/labs/symbiosis/
http://git.dvide.com/pub/symbiosis/tree/myocamlbuild_config.ml

Most of this code is a java script object parser (JSON) which
generates an mostly untyped JSON object tree of lists and maps, but
still has basic float, int and string types.

The actual Symbiosis logic is a thin layer on top of this to access
different configuration logic.

One interesting part of this is the object navigation: each node is
represented as <node, pos> where node is one of the basic JSON types.
Any navigation into the JSON tree results in a new position, but the
position remains separate from the tree. Whenever an expected value is
not found, an exception is thrown and the position is used to report
the error location.

In some sense this attached position corresponds to dynamic type
information. You could view navigation as a computation and attach
type. For example matrix multiplying two JSON lists and attached the
resulting dimensions to the resulting JSON object tree.
I guess this can also be formulated as a monad somehow.

Perhaps this can be of some inspiration, or perhaps it is a different
problem you are trying to solve.

Regards,
Mikkel