Changes between Version 12 and Version 13 of NewtypeWrappers


Ignore:
Timestamp:
Jul 26, 2013 9:17:28 AM (12 months ago)
Author:
nomeata
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewtypeWrappers

    v12 v13  
     1[[PageOutline(1-100,Page Contents,inline)]] 
     2 
    13= Newtype wrappers = 
    24 
     
    4850 * (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. 
    4951 * (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''. 
     52 * (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''. 
    5153 
    5254== Use cases == 
     
    141143One issue with type classes is that they cannot be used only internally, so the third use case above would not be possible. 
    142144 
    143 == Abstraction == 
    144  
    145 Suppose we have 
    146 {{{ 
    147         module Map( ... ) where 
    148           data Map a b = ...blah blah... 
    149  
    150         module Age( ... ) where 
    151           newtype Age = MkAge Int 
    152 }}} 
    153 Now suppose we want a newtype wrapper like this 
    154 {{{ 
    155         import Map 
    156         import Age 
    157  
    158         newtype wrap foo :: Map Int Bool -> Map Age Bool 
    159 }}} 
    160 Could we write `foo` by hand? (This is a good criterion, I think.) Only if we could see the data constructors of ''both'' `Map` ''and'' `Age`.  
    161  
    162  * If we can't see the data constructor of `Age` we might miss an invariant that Ages are supposed to have.   For example, they might be guaranteed positive. 
    163  
    164  * If we can't see the data constructors of `Map`, we might miss an invariant of Maps. For example, maybe `Map` is represented as a list of pairs, ordered by the keys.  Then, if `Age` orders in the reverse way to `Int`, it would obviously be bad to substitute. 
    165  
    166 Invariants like these are difficult to encode in the type system, so we use "exporting the constructors" as a proxy for "I trust the importer to maintain invariants".  The "Internals" module name convention is a signal that you must be particularly careful when importing this module; runtime errors may result if you screw up. 
    167  
    168 One possible conclusion: if we have them at all, newtype wrappers should only work if you can see the constructors of ''both'' the newtype, ''and'' the type you are lifting over.   
    169  
    170 But that's not very satisfactory either.   
    171  
    172  * There are some times (like `IO`) where it '''does''' make perfect sense 
    173    to lift newtypes, but where we really '''don't''' want to expose 
    174    the representation.  
    175  
    176  * Actually `Map` is also a good example: while `Map Age Bool` should 
    177    not be converted to `Map Int Bool`, it'd be perfectly fine to convert 
    178    `Map Int Age` to `Map Int Int`. 
    179  
    180  * The criterion must be recursive.  For example if we had 
    181 {{{ 
    182          data Map a b = MkMap (InternalMap a b) 
    183 }}} 
    184   It's no good just being able to see the data constructor `MkMap`; you need to 
    185   see the constructors of `InternalMap` too. 
    186  
    187 The right thing is probably to use kinds, and all this is tantalisingly close to the system suggested in [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ Generative type abstraction and type-level computation].  Maybe we should be able to ''declare'' Map to be indexed (rather than parametric) in its first parameter. 
    188  
    189 More thought required. 
     145=== Status === 
     146 
     147Joachim started to implement this approach. TODO: 
     148 
     149* Class `IsNT concr abstr` defined in ghc-prim.GHC.NT ✓ 
     150* Deriving code added. ✓ 
     151* Check for constructor visibility. ✓ 
     152* Check for data constructor argument convertibility. ✓ (but not very elegant yet) 
     153* Think about higher-order type arguments. 
     154 
     155Warts and issues: 
     156 
     157* The deriving code works in the typechecker and has to generate `HsExpr`, but the implementation is only possible in Core. Currently, a dummy value is inserted by the deriving code and later implemented by a core-to-core pass. Better solution: Add a `HsCore` data constructor to `HsExpr`, similar to `HsCoreTy` in `HsType`? 
     158* The overlapping nature of the problem. We clearly want to have a base case `IsNT a a` so that `castNT :: (Int,a) -> (Age, a)` is possible. For that we need all instances of `IsNT` to have the incoherent flag set (✓). But that is not enough: `castNT :: (Int,[a]) -> (Age, [a])` does not work (overlapping matching instances `IsNT a a` and `IsNT [a] [a]`), while  (counterintuitively) `(castNT :: (Int,a) -> (Age, a)) :: (Int,[a]) -> (Age, [a])` works again. Possible solutions: 
     159 * Change the semantics of `IncoherentInstances` that it chooses an arbitrary, or the most specific, or the most general instance here. 
     160 * Add a flag to classes that marks them as “univalent”, telling the type checker that any instance is good and overlap should not hinder him 
     161 
     162Code not yet pushed anywhere. 
    190163 
    191164== Proposal 3 == 
     
    238211As 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).  
    239212 
     213Implementation started at [https://github.com/nomeata/nt-coerce/]. 
     214 
    240215It was [http://www.haskell.org/pipermail/ghc-devs/2013-July/001667.html later argued] that the benefits over the type-class apporoach (Approach 2) do not warrant the extra syntactical complexity. 
    241216