I would like to be able to say that [ ] is one symbol denoting different values of different types and that the compiler picks which value it denotes given the context. But the example program disallows that--which is how I came up with the example in the first place.


xs is not bound to a value with a concrete type (like [Int] or [Char]) at compile time. Even after compilation xs :: [a].

To say that [ ] is a value having many different types seems to be saying more or less the same thing, namely that compilation doesn't pick a particular concrete type.

So what are the other options? I still like the idea of saying that [ ] is a function that takes a type as an argument and generates a value. (I believe this was your explanation at one point.) I realize that it isn't a function at the Haskell level. But it makes intuitive sense to say that the compiler generates such a function, which is what is bound to xs. It is that function that gets executed when the program is run. I know that for optimization purposes it may be compiled down past that interpretation and I also know that this function isn't a Haskell function.  But if one were giving an operational semantics for what's going on (which I guess is what the Core effectively is) that seems to be the most transparent explanation.