[Haskell-cafe] Re: Tiger compiler in Haskell: annotating abstract

[oleg at okmij.org]

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