Re: [isabelle] Polymorphism and simple type



Isabelle's lambda calculus is in between simply typed and ML-style
polymorphic (with type classes thrown in). It is simply typed because
the types are built up from base types by means of =>. It resembles
ML-style polymorphism because it has type variables, too (and thus
simply-typed is an understatement). The difference to ML-style
polymorphism is that it has no let construct for defining a polymorphic
constant locally inside a term. This has to be done at the declaration
level, i.e. gobally. It shares the absence of explicit type quantifiers
with Milner's original paper, where he even managed to have a
let-construct without making the quantifiers explicit.

Tobias

Steve W schrieb:
> Hi,
> 
> I have a question about Isabelle's polymorphism. Since Isabelle has a
> simply-typed lambda calculus, how come the meta-logic is polymorphic?
> Polymorphism is not typically considered simple, right?
> 
> Regards
> Steve





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.