JWC@IDA.LiU.SE (Jonas Wallgren) (10/31/89)
I would like to get a description or an example of what is lost in the ML type system et al when only allowing quantifiers "at top" (shallow types). In his classical paper "A Theory of Type Polymorphism in Programming" R. Milner says that his choice avoids some difficulties. Which difficulties? Eg. in what cases is there any difference between two types like (FORALL a.(FORALL b.(a->b))) and ((FORALL a.a)->(FORALL b.b)). Maybe it depends on different kinds of semantics for types, but in what way? ------------------------------------------------------------------------------- Jonas Wallgren | JWC@IDA.LiU.SE Department of Computer and Information Science | Linkoping University |------------------------------- SE-581 83 Linkoping | Sweden |(\x.xx)(\x.x):(forall a.(a->a)) -------------------------------------------------------------------------------