Equal existential types are not printed equally by the top-level?

Learning
, ,
1

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

The constructor Dyn has one existential type that occurs twice, as'a in 'a ty * 'a. Why the top-level prints Int but fails to print 3?

2

'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

then printing Dyn (Weird [2; 3], 4) would probably show something like Weird [<poly>; <poly>] in the first argument.

3

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 Dyn is Int, which has type int ty; then from the type of Dyn it infers that the second argument of Dyn has type int.

4

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?

5

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.