Changes between Version 9 and Version 10 of RankNTypes


Ignore:
Timestamp:
Sep 8, 2006 11:34:24 AM (9 years ago)
Author:
ross@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • RankNTypes

    v9 v10  
    2727== References ==
    2828 * [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#universal-quantification Arbitrary-rank polymorphism] in the GHC User's Guide.
    29  * [http://research.microsoft.com/Users/simonpj/papers/higher-rank/ Practical type inference for arbitrary-rank types], Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields, July 2005.
    30  * [http://research.microsoft.com/Users/simonpj/papers/boxy/ Boxy types: type inference for higher-rank types and impredicativity], Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, November 2005.
     29 * [http://research.microsoft.com/Users/simonpj/papers/higher-rank/ Practical type inference for arbitrary-rank types], Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields, July 2005.  To appear in ''Journal of Functional Programming''.
     30 * [http://research.microsoft.com/Users/simonpj/papers/boxy/ Boxy types: type inference for higher-rank types and impredicativity], Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, ICFP 2006.
    3131 * [http://www.haskell.org/onlinereport/decls.html#type-semantics Semantics of Types and Classes] in the Haskell 98 Report
    3232 * PolymorphicComponents would also be allowed higher-rank types
     
    4141The rules may also be used as a bottom-up procedure for inferring principal types, with inferred types matched against any signatures supplied, but many other traversals yield the same answer.
    4242A mixture of bottom-up inference and top-down checking often produces more informative error messages.
     43
     44=== Bidirectional type inference ===
    4345
    4446For arbitrary-rank types, a particular bidirectional traversal is specified by the type rules (see Fig. 8 on p25 of [http://research.microsoft.com/Users/simonpj/papers/higher-rank/ the arbitrary-rank paper]), to make use of programmer-supplied annotations.
     
    5658 * Both checking and inference are monotonic with respect to the generalization preorder.
    5759
     60=== Boxy types ===
     61
     62Boxy types generalize bidirectional inference, and also allow impredicative types (type variables may be instantiated to polytypes, and polytypes may occurs as arguments of type constructors).
     63
    5864== Pros ==
    5965 * More convenient than encodings using PolymorphicComponents
     
    6268 * More complex than [wiki:Rank2Types], which cover the most common cases (and can encode the rest, though clumsily).
    6369 * No clear programmer-level description of the restrictions that apply.
     70   To quote the [http://research.microsoft.com/Users/simonpj/papers/boxy/ boxy-types paper]:
     71
     72   The type system is arguably too complicated for Joe Programmer to understand, but that is true of many type systems, and perhaps it does not matter too much: in practice, Joe Programmer usually works by running the compiler repeatedly, treating the compiler as the specification of the type system. Indeed, a good deal of the complexity of the type system (especially Section 6) is there to accommodate programs that "ought" to work, according to our understanding of Joe's intuitions.