Changes between Version 9 and Version 10 of RankNTypes


Ignore:
Timestamp:
Sep 8, 2006 11:34:24 AM (8 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.