Jose Pedro Magalhaes wrote:
From what I understand, you are using a list of integers to encode a path to a subterm. This is a practical and lightweight implementation, but less type-safe: it is easy to encode annotations that do not correspond to any value. Also, it cannot guarantee, with types alone, that every subterm is annotated.
Let us consider the type safety closely. Let us assume a very simple data type: lists of integers of length 10. Suppose we want to add string annotations to the elements. In my solution, I create an IntMap whose key is an integer 0..9 (the index in the original list) and the value is the string annotation. It is true that the type system does not prevent me from adding an annotation for key 11 (which corresponds to no element in the original list) or from forgetting to add annotation for key 7. As I understand it, your approach is to transform the original list of integers into the list of (Int,String) pairs. Now we are sure that each element is paired with an annotation and there are no orphan annotations. The annotation process creates this new list of pairs and returns it. However, how do you get _the type checker_ to ensure that the annotated list does correspond to the original list? That all old elements are present in the annotated list, and in the same order? It all boils down to enforcing the invariant proj al == l where l is the original list, al is the annotation list, and proj is the operation that removes annotations. It is true that my lightweight method generally cannot, in type system, enforce that invariant. (I can still enforce it if I design an appropriate security kernel and prove, _offline_, its correctness). But how could you enforce that invariant *in the type system*?