The Evil Value Restriction and Lisp Macros

One of the more annoying features of the HM type system is how it interacts poorly with imperative features. Every few weeks I completely forget these limitations and try to do something that in any other language would be completely natural, and get bit again.

The heart of the problem is exposed by the idea of using a mutable list datatype. When you create an empty list ('nil'), it has type "list 'a" - in other words, 'nil' can take on any type you like.

In Irken, as long as you stick with the datatype constructors themselves, this works. You can create lists of different types right next to each other and have all the type safety you like.

But as soon as you try to wrap that up - for example, into a stack ADT - you hit the value restriction.

In OCaml, this problem manifests as 'weak' type variables - e.g., " list '_a ", which just records the fact that '_a is currently unknown, and will instantiate to only one type.

One reason this keeps biting me unexpectedly is that I've changed the compiler to (by default) only type the program after inlining. This make copies of smaller polymorphic functions/interfaces, thereby side-stepping the problem with the value restriction - instead of making one copy of a function that works at multiple types, inlining causes that code to be duplicated at each site. I only notice VR problems when I force it to type twice, or turn off inlining.

I'm wondering: as a practical matter, maybe I should just embrace this. I'm not qualified to invent a new type system that's going to fix all this. But a 'stupid' substitution system (like C++ templates or lisp macros) makes the problem go away, and that's good enough for me.

AFAIK none of the ML's have a macro system. Is this perhaps a side-effect of ML fans' universal hatred of Lisp?

How might macros interact with HM? For example, could we design a 'polymorphic class' that would essentially copy the code at each use site?