Quantifiers in types

Article View: comp.lang.misc

Article #752

#752

From: Jonas Wallgren
Date: Mon, 30 Oct 1989 23:51

17 lines
1434 bytes

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))
-------------------------------------------------------------------------------

Technical Details

Message-ID: <1411@majestix.ida.liu.se>

Path:

arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!cs.utexas.edu!ginosko!samsung!brutus.cs.uiuc.edu!lll-winken!uunet!mcsun!sunic!liuida!JWC

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!cs.utexas.edu!ginosko!samsung!brutus.cs.uiuc.edu!lll-winken!uunet!mcsun!sunic!liuida!JWC
From: JWC@IDA.LiU.SE (Jonas Wallgren)
Newsgroups: comp.lang.misc
Subject: Quantifiers in types
Message-ID: <1411@majestix.ida.liu.se>
Date: 30 Oct 89 23:51:54 GMT
Sender: jonwa@majestix.ida.liu.se
Lines: 17
Organisation: CIS Dept, Univ of Linkoping, Sweden