Extensional models for polymorphism