Below is a small interaction with the top-level.
- Fisrt define a witness for the integer type.
- Then define the type for dynamically typed values.
- Next provide a dynamically typed integer for evaluation.
# type _ ty = Int : int ty;;
# type dyn = Dyn : 'a ty * 'a -> dyn;;
# Dyn (Int, 3);;
- : dyn = Dyn (Int, <poly>)
Dyn has one existential type that occurs twice, as
'a ty * 'a. Why the top-level prints
Int but fails to print
'a ty and
'a are not at all the same types! You cannot show anything about a value of type
'a without knowing the type. On the other hand, with your current definition of
'a ty, you don’t need to know
'a to print the values of type
'a ty. If you had, say,
type 'a ty = Int : int ty | Weird : 'a list -> 'a ty
Dyn (Weird [2; 3], 4) would probably show something like
Weird [<poly>; <poly>] in the first argument.
It seems that the top-level does not do any type inference before printing. Otherwise, when printing
Dyn(Int, 3) it would first determine that the first argument of
Int, which has type
int ty; then from the type of
Dyn it infers that the second argument of
Dyn has type
The toplevel performs a limited form of type inference, propagating type information from a constructor to each of its argument – a simple form of (bi)directional type inference. Your idea requires a more sophisticated form of inference indeed.
How would it work in the case
Dyn : 'a * 'a ty -> dyn, where the type-information-providing tag comes after the value? I guess one could first traverse the value in full, to compute a (bottom-up) type derivation with general unification, and then print it.
This sounds doable, but also a complex change to the printing logic. Is there evidence that this is important in practice?
A complex printer may not be that important.
My question arose when I was testing functions that process dynamically typed values (e.g. convert between a dynamic product and a list of dynamic values that are the product entries).
I use the top level to observe the result of these functions. Although the printer does not print existential types as expected, I can still do my test in other ways, such as using polymorphic comparison (=) to check if the function output is structurally equal to the expected value, instead of printing the output on the top-level and see if it is the expected value.