Changes between Version 5 and Version 6 of NewtypeWrappers


Ignore:
Timestamp:
Jun 26, 2013 10:23:13 PM (10 months ago)
Author:
nomeata
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewtypeWrappers

    v5 v6  
    3939 * For `x2` we'd have to eta-expand: `(\y -> MkAge (x2 y)) :: Char -> Age`.  But this isn't good either, because eta exapansion isn't semantically valid (if `x2` was bottom, `seq` could distinguish the two).  See #7542 for a real life example. 
    4040 
    41  * For `x3`, we'd have to map over `T`, thus `mapT MkAge x3`.  But what if `mapT` didn't exist?  We'd have to make it. And not all data types have maps. `S` is a harder one: you could only map over S-values if `m` was a functor.  There's a lot of discussion abou this on #2110. 
     41 * For `x3`, we'd have to map over `T`, thus `mapT MkAge x3`.  But what if `mapT` didn't exist?  We'd have to make it. And not all data types have maps. `S` is a harder one: you could only map over S-values if `m` was a functor.  There's a lot of discussion about this on #2110. 
     42 
     43== Goal == 
     44 
     45In summary: 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: 
     46 * It should be sound, i.e. have an implementation in Core with existing coercions, without new coercions or `unsafeCoerce`. 
     47 * 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). 
     48 * (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. 
     49 * (desirable:) It should be possible to use such a coercion in one module in internal code, but not export it. 
     50 * (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''. 
     51 
     52== Use cases == 
     53 
     54To clarify these requirements, here some benchmarks; feel free to expand if you have further needs. 
     55 
     56 * Allow the user to define a function of type `C N -> C T` with a zero-cost model. 
     57 * Allow the author of `Data.Set` prevent a coercion `Set N -> Set T` (as it would break internal invariants). 
     58 * 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. 
     59 
    4260 
    4361== The opportunity == 
     
    121139This plan requires a bit more paddling under the water on GHC's part, especially during type inference, but it looks a lot more straightforward than I first thought.  Thanks to Roman Cheplyka for advocating this solution. 
    122140 
     141One issue with type classes is that they cannot be used only internally, so the third use case above would not be possible. 
     142 
    123143== Abstraction == 
    124144 
     
    169189More thought required. 
    170190 
     191== Proposal 3 == 
     192 
     193This 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. 
     194 
     195Assume there is a module provided by GHC with these definitions 
     196{{{ 
     197data NT a b -- abstract 
     198coerce :: NT a b -> a -> b 
     199refl :: NT a a 
     200sym :: NT a b -> NT b a 
     201trans :: NT a b -> NT b c -> NT a c 
     202}}} 
     203and 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. 
     204 
     205Besides 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. 
     206{{{ 
     207deriving nt :: NT N T 
     208deriving list :: NT a b -> NT [a] [b] 
     209}}} 
     210 
     211The 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.) 
     212 
     213This solves the abstraction problem for `Data.Map`: The library author only exports `NT a b -> NT (Map k a) (Map k b)`, but not NT a b -> NT (Map a v) (Map b v)`. 
     214 
     215Of course with an `NT` data type, it is possible to define this type class, e.g. 
     216{{{ 
     217class NT' a b where 
     218  theNT :: NT a b 
     219coerce' :: NT' a b => a -> b 
     220coerce' = coerce theNT 
     221}}} 
     222and use it where more convenient than the function-based variant. 
     223 
     224As to the implementation, I quite naively expect that the definition of `NT` and related function in terms of Core to be straight-forward (`newtype NT a b = a ~_R b`). 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).  
     225 
     226 
    171227== Type soundness ==  
    172228