Three languages with polymorphic type disciplines are discussed, namely the λ-calculus with Milner's polymorphic type discipline; a language with imperative features (polymorphic references); and a skeletal module language with structures, signatures and functors. In each of the two first cases we show that the type inference system is consistent with an operational dynamic semantics. On the module level, polymorphic types correspond to signatures. There is a notion of principal signature. So-called signature checking is the module level equivalent of type checking. In particular, there exists an algorithm which either fails or produces a principal signature.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:384249 |
| Date | January 1988 |
| Creators | Tofte, Mads |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/1842/6606 |
Page generated in 0.0318 seconds