[Rseend: I got no response first time round]
On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote:
> Since I began using HOL88 many years ago, I have always heard that the
> logic of HOL was "higher order logic,"
> ...
However, when reading both of these, I see that in neither case does the
> type system proposed contain type variables within the logic. They both
> use type variables as meta-variables, e.g. when describing an infinite
> class of related axioms, but they do not express such a notion as a single
> axiom using a type variable within the logic.
>
> It appears from checking page 11 of the HOL4 LOGIC manual, that the
> inventor of this idea was Robin Milner:
>
> 1. *Type variables: *these stand for arbitrary sets in the universe. In
> Church's original
>
> formulation of simple type theory, type variables are part of the
> meta-language
>
> and are used to range over object language types. Proofs containing type
> variables
>
> were understood as proof schemes (i.e. families of proofs). To support such
>
> proof schemes *within *the HOL logic, type variables have been added to the
> object
>
> language type system.2
> ...
> ________________
>
> 2This technique was invented by Robin Milner for the object logic PP of
> his LCF system.
>
> I am very curious about this addition. This is actually an idea of great
> and subtle power, and I think it was a really significant innovation. It
> allows for simple but powerful types such as I:'a -> a' and map:('a -> 'b)
> -> ('a list -> 'b list) which I use all the time. In fact, one wonders if
> the popularity of HOL would have been as wide without this key idea.
>
> I have several questions about this. First, what is the proper terminology
> to refer to both systems, with or without type variables? Second, how
> should credit be given for this innovation? Third, is there any more
> information about this invention by Robin Milner, ie. did he ever publish a
> paper about this? Given the surpassing practical benefit of type
> variables, this seems a remarkably unremarked jewel of type theory history.
Roger Hindley's book "Basic Simple Type Theory" has some historical background
and references including Milner's 1978 "A theory of type polymorphism in
programming". However, the ideas predate Milner's contribution: Hindley cites
Curry & Feys as having sketched the principal-type algorithm in their 1958
book "Combinatory Logic".
Hindley's 1969 "The principal type-scheme of an object in combinatory logic"
presents a system with polymorphic constants and polymorphic axioms that can
be instantiated. He compares earlier formulations with infinite families of
monomorphic constants/axioms with formulations with a finite set of
polymorphic constants/axioms.
Regards,
Rob.
-------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
