Changes between Version 12 and Version 13 of NewtypeWrappers


Ignore:
Timestamp:
Jul 26, 2013 9:17:28 AM (2 years 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