I'm not sure if this is of interest to readers of this thread, but here goes:
Elements of Functional Programming, by Chris Reade (a student level textbook) has this to say, at pp 396-7: (talking about type inference) (quote) Note that in these inferences, we used T, T-1, ..., as meta type variables standing for unknown types and these unknown types may involve ordinary type variables such as \alpha, \beta, ... and so on. There is a conceptual distinction between meta variables which we use (outside the system) to stand for any type and type variables which are part of the type system and also stand for any type. However we can conveniently borrow ordinary type variables for use as meta type-variables to simplify the development of an algorithm. (end quote) Ie, the last sentence seems to say that although it is a significant conceptual distinction, it doesn't really matter. A related point: Isabelle (though not HOL) has "explicitly variable" variables (for both types and terms), ?a and ?'a, as well as "fixed" variables, a and 'a. The ? variables can be substituted for, the others can't. But when a theorem is proved, the non-? variables can be changed to ? variables. I've never really thought about it, but if you'd asked me I would have said that I suppose the non-? variables are part of the object language and the ? variables are a sort of meta level device. Which may again suggest that a conceptual distinction is not practically significant. Another related question: Peter has raised the issue of whether a type variable is a meta level or an object level notion. Does it make sense equally to consider whether a non-variable type assertion, say x : int, is an object-level assertion, or a meta-level statement about an object level term x? I would find it more natural to say the former. But does the answer to that question matter? Jeremy Dawson ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
