Changes between Version 1 and Version 2 of ExposingNewtypeCoercions


Ignore:
Timestamp:
Jun 26, 2013 10:23:54 PM (2 years ago)
Author:
nomeata
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ExposingNewtypeCoercions

    v1 v2  
    1 This is a write-down of a discussion between me (nomeata) and SPJ at TLCA 2013, but my memory might have tricked me and I might have filled in some bits myself, so beware. It should enable to solve (parts of) #2110. 
    2  
    3 == Goal == 
    4  
    5 The programmer expects zero-cost conversions between a newtypes ''N'' and the type ''T'' it is based on. We want to allow the programmer to have zero-cost conversions between ''C N'' and ''C T''. Requirements: 
    6  * It should be sound, i.e. have an implementation in Core with existing coercions, without new coercions or `unsafeCoerce`. 
    7  * It should respect module boundaries, i.e. not allow the user to create a function which he could not write using plain Haskell (and non-zero cost). 
    8  * (desirable:) It should be exportable and composable, i.e. the module of ''N'' should be able to specify that a conversion between ''N'' and ''T'' is allowed (or not), and the module of ''C'' should be able to specify if a coercion can be lifted (or not), and if both allow it, the user should be able to combine that even if the modules of ''N'' and ''T'' are independent. 
    9  * (desirable:) It should be possible to use such a coercion in one module in internal code, but not export it. 
    10  * (desirable:) It should be possible to add REWRITE rules that turn, for example `map N` into the zero-cost conversion from ''C T'' to ''C N''. 
    11  
    12 == Use cases == 
    13  
    14 To clarify these requirements, here some benchmarks; feel free to expand if you have further needs. 
    15  
    16  * Allow the user to define a function of type `C N -> C T` with a zero-cost model. 
    17  * Allow the author of `Data.Set` prevent a coercion `Set N -> Set T` (as it would break internal invariants). 
    18  * Allow the author of a escaping-ensuring `newtype HTML = HTML String` to use the coercion `[String] -> [HTML]` internally, but prevent the user of the library from doing that. 
    19  
    20 == Suggested interface == 
    21  
    22 === Abstract `NT` type === 
    23  
    24 There is a module provided by GHC with these definitions 
    25 {{{ 
    26 data NT a b -- abstract 
    27 coerce :: NT a b -> a -> b 
    28 refl :: NT a a 
    29 sym :: NT a b -> NT b a 
    30 trans :: NT a b -> NT b c -> NT a c 
    31 }}} 
    32 and the intention that `NT a b` is a witness that `a` and `b` have the same representation and that `coerce n` has zero runtime cost. 
    33  
    34 Besides the trivial `refl` values, values of type `NT` cannot be created by the user, but only by a special `deriving` statement giving the type of a function that creates `NT` values, but without a definition, e.g. 
    35 {{{ 
    36 deriving nt :: NT N T 
    37 deriving list :: NT a b -> NT [a] [b] 
    38 }}} 
    39  
    40 The compiler either rejects the declaration or creates an implementation automatically. It should only create an implementation if a non-zero-cost-implementation could be written by the user instead. (I expect that this means that the constructors of the return type are in scope.) 
    41  
    42 === `NT` type class === 
    43  
    44 An earlier variant of the idea introduced a type type class for coercions, e.g. 
    45 {{{ 
    46 class NT a b where 
    47   coerce :: a -> b  
    48 }}} 
    49  
    50 This would allow an interface more in line with existing features, i.e. one would simply list this class in the `derving` clause of `newtype` definitions, or use `deriving instance NT a b => NT [a] [b]`. See also [comment:29:ticket:2110 this comment by sweirich]. Unfortunately, type classes leak, so it would be possible to use the machinery in internal modules but not have it available to users of the library. 
    51  
    52 Of course with an `NT` data type, it is possible to define this type class, e.g. 
    53 {{{ 
    54 class NT' a b where 
    55   theNT :: NT a b 
    56 coerce' :: NT' a b => a -> b 
    57 coerce' = coerce theNT 
    58 }}} 
    59 and use it where more convenient than the function-based variant. 
    60  
    61 == Implementation == 
    62  
    63 Quite naively, I expect that the definition of `NT` and related function in terms of Core is straight-forward (`newtype NT a b = a ~_R b`). 
    64  
    65 The code that does the `deriving` is maybe non-trivial, as it has to build the term from available newtype axioms (where the constructor is in scope), coercions given as parameters and the application of type constructors to coercions (again, where the data constructors are in scope).  
     1Merged into NewtypeWrappers (this page can be deleted).