Guy S., Phil W.,...
I ran into exactly this problem in two different applications.
The first was the same that Guy S. points out, namely adding
arbtrirary but well-typed annotations to a parse-tree. The solution I
eventually ended up using (after discussing it with John Hughes) was
the following:
data FooTree a b = Leaf b |
Node (AnnotFooTree a b) (AnnotFooTree a b)
type AnnotFooTree a b = (a, FooTree a b)
originally I'd tried:
data FooTree a b = Leaf a | Node (a (FooTree b)) (a (FooTree b))
which was of course rejected by the Hindley-Milner typechecker.
I recall David Murphy saying that I could have done that in Isabelle
but it involved a much more powerful type-checker. BTW, Simon PJ and
David Lester hit on exactly the same solution in their paper on
fully lazy lambda-lifting so presumably they'd given this problem
some thought too.
The other application was Tries. Imagine we have some type:
data Assoc a b = ...
which maps objects of type a to objects of type b. We don't care if
it's implemented as a tree, list, array or whatever provided there's
a standard interface. Now imagine that our applications involves
keys which are variable length lists/strings of as. Using the above
type instantiating a as [a] will cause increasingly costly comparisons
as the search gets closer to its goal. Trie structures avoid this by
matching one segment of the key at a time. For instance rather than
storing the following
"guy argo"
|
"guy steele"
it's stored as:
'g' - 'u' - 'y' - ' ' - 'a' - 'r' - 'g' - 'o'
|
's' - 't' - 'e' - 'e' - 'l' - 'e'
(n.b. Compressed tries go one step further by collapsing the one-way
branching to give:
"guy " - "argo"
|
"steele")
Anyway, given the above Assoc type a very natural encoding of tries
is:
type Trie a b = Assoc a (Trie a b)
The operations on Tries can now be built out of the Assoc operations
which allows the lookup structure used at each level to be altered
without painful recoding merely by substituting a different Assoc ADT.
I mention this to support Guy S.'s point that there might be gains
from going to a more expressive type system than Hindley-Milner.
I don't know what that might be - I just know that the things that I
mentioned aren't handled as elegantly as I'd like.
My $0.02
Guy Argo
