Changes between Version 12 and Version 13 of NewtypeWrappers

Jul 26, 2013 9:17:28 AM (4 years ago)



  • NewtypeWrappers

    v12 v13  
     1[[PageOutline(1-100,Page Contents,inline)]]
    13= Newtype wrappers =
    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''.
    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.
    143 == Abstraction ==
    145 Suppose we have
    146 {{{
    147         module Map( ... ) where
    148           data Map a b = ...blah blah...
    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
    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`.
    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.
    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.
    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.
    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. 
    170 But that's not very satisfactory either. 
    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.
    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`.
    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.
    187 The right thing is probably to use kinds, and all this is tantalisingly close to the system suggested in [ 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.
    189 More thought required.
     145=== Status ===
     147Joachim started to implement this approach. TODO:
     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.
     155Warts and issues:
     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
     162Code not yet pushed anywhere.
    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).
     213Implementation started at [].
    240215It was [ later argued] that the benefits over the type-class apporoach (Approach 2) do not warrant the extra syntactical complexity.