Changes between Version 16 and Version 17 of NewtypeWrappers


Ignore:
Timestamp:
Sep 13, 2013 9:10:54 PM (23 months ago)
Author:
nomeata
Comment:

Clean up the page a bit to keep up the signal-to-noise-level on the wiki.

Legend:

Unmodified
Added
Removed
Modified
  • NewtypeWrappers

    v16 v17  
    6060 * 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.
    6161
     62== The implementation ==
    6263
    63 == The opportunity ==
     64Core already had provided all the necessary feature; the question was just how to offer it on the Haskell level. The implementation comes in form of a `coerce :: Coercible a b -> a -> b` and a type class `Coercible` that relates two types if they have the same representation, i.e. can be related by a coercion of role Representational (see [wiki:Roles]). See the haddock documentation for `coercible` for user-level documentation and Note [Coercible Instances] for information on the implementation.
    6465
    65 Clearly what we want is a way to "lift" newtype constructors (and dually deconstructors)
    66 over arbitrary types, so that whenever we have some type `blah Int blah` we can convert it
    67 to the type `blah Age blah`, and vice versa.
     66The implementation fulfills the first goal, the second partly (`C N -> C T` is allowed even without `C`'s data constructors in scope; if `C` should be abstract the role of its argument needs to be `Nominal`. Due to the ad-hoc nature of the `Coercible` instances, the second and third goal are not achieve. No work towards the fifths goal has been done.
    6867
    69 Tantalisingly, [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ System FC], GHC's internal Core language, already has exactly this!
    70  * A newtype constructor turns into an FC cast:
    71 {{{
    72   MkAge x    turns into       x |> AgeNTCo
    73 where
    74   AgeNTCo :: Int ~ Age
    75 }}}
    76 The `|>` is a cast, and the `AgeNTCo` is a coercion axiom witnessng the equality of `Int` and `Age`.
     68== Discussion of alternatives ==
    7769
    78  * Coercions can be lifted, so that
    79 {{{
    80   [AgeNTCo]       :: [Int] -> [Age]
    81   Char -> AgeNTCo :: (Char -> Int) ~ (Char -> Age)
    82   T AgeNTCo       :: T Int ~ T Age
    83   S IO AgeNTCo    :: S IO Int ~ S IO Age
    84 }}}
     70=== Proposal 1 ===
    8571
    86 So all we need is concrete syntax to allow you to ask for these lifed coercions in Haskell. 
     72Top level declarations of coercions as functions (e.g. `newtype wrap w1 :: [Int] -> [Age]` and `newtype wrap w2 :: (Char -> Int) -> (Char -> Age)`).
    8773
    88 == Proposal 1 ==
    89 
    90 The first possiblity involves a new top-level declaration:
    91 {{{
    92   newtype wrap w1 :: [Int] -> [Age])
    93   newtype wrap w2 :: (Char -> Int) -> (Char -> Age)
    94   newtype wrap w3 :: T Int -> T Age
    95   ..etc..
    96 }}}
    97 and dually
    98 {{{
    99   newtype unwrap u1 :: [Age] -> [Int])
    100   newtype unwrap u2 :: (Char -> Age) -> (Char -> Int)
    101   ..etc...
    102 }}}
    103 This brings into scope the variables `w1`, `w2`, etc, with the declared types. Applications of these wrappers
    104 and unwrappers have the same cost model as newtype constructors themselves: they are free.
    105 
    106 More precisely
    107 
    108  * The type specified in a newtype wrap/unwrap declaration must be of the form `type1 -> type2`.
    109 
    110  * `wrap` and `unwrap` are keywords, but only when they occur right after the keyword `newtype`.
    111 
    112  * Wrappers/unwrappers can be polymorphic
    113 {{{
    114   newtype wrap foo :: [(Int,b)] -> [(Age,b)]
    115 }}}
    116 
    117  * Multiple "layers" of newtype can be wrapped at once (just as in `foreign` declarations). For example:
    118 {{{
    119   newtype Fun a = MkFun (a -> a)
    120   newtype Age = MkAge Int
    121   newtype wrap foo :: (Int -> Int) -> Fun Age
    122 }}}
     74This is close to the actual implementation, but requires giving names to the coercion and introduces new syntax.
    12375
    12476== Proposal 2 ==
    12577
    126 The second possibility is superficially simpler: just provided a new built-in constant with type
    127 {{{
    128   newtypeCast :: NTC a b => a -> b
    129 }}}
    130 Here `NTC` is a built-in type class that witnesses the (free) conversion between `a` and `b`.  Although it would not quite be implemented like this, we would have a built-in instance for each data type (but see Type Soundness below):
    131 {{{
    132   instance NTC a b => NTC [a] [b]
    133 }}}
    134 and two built-in instances for each newtype:
    135 {{{
    136   instance NTC Int b => NTC Age b
    137   instance NTC a Int => NTC a Age
    138 }}}
    139 So to solve a `NTC` constraint you unwrap all those newtypes (being careful about abstraction; see next section). 
    140 
    141 This 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.
    142 
    143 One issue with type classes is that they cannot be used only internally, so the third use case above would not be possible.
    144 
    145 === Status ===
    146 
    147 Joachim 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 * Make `IncoherentInstances` [http://www.haskell.org/pipermail/ghc-devs/2013-July/001771.html even more incoherent].
    154 * Think about higher-order type arguments.
    155 * Polish error messages.
    156 * Port to the new role-based coercion.
    157 * Add instances to base etc.
    158 
    159 Warts and issues:
    160 
    161 * 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`?
    162 
    163 Code not yet pushed anywhere.
     78(This is basically the current implementation, advocated by Roman Cheplyka.)
    16479
    16580== Proposal 3 ==
    16681
    167 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.
     82Given a module providing
    16883
    169 Assume there is a module provided by GHC with these definitions
    17084{{{
    17185data NT a b -- abstract
     
    17589trans  :: NT a b -> NT b c -> NT a c
    17690}}}
    177 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.
    17891
    179 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.
     92and additional code to derive stuff like
    18093{{{
    18194deriving nt :: NT N T
     
    18396}}}
    18497
    185 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.)
    186 
    187 The “could you write it by hand” criteria implies that the expected arguments for the nt value depends on how they type parameters are used in the data constructors, e.g:
    188 
    189 {{{
    190 data Foo a = Foo (Bar a)
    191 deriving fooNT' :: NT a b -> NT (Foo a) (Foo b) -- not ok, especially if `Bar` is abstract
    192 deriving fooNT :: NT (Bar a) (Bar b) -> NT (Foo a) (Foo b) -- ok
    193 }}}
    194 
    195 Question: `fooNT'` can be constructed from `fooNT` and a possible `barNT :: NT a b -> NT (Bar a) (Bar b)`. Should the compiler do this automatically, if `barNT` is in scope, or is that too much magic?
    196 
    197 This 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)`.
    198 
    199 All this amounts to exposing explicit System-FC coercions to the programmer; and that is precisely what we want to do.
    200  * Explicit, because `Age` and `Int` really are different types, and so we can't silently convert between them.
    201  * Explicit, so that we can control precisely which coercions are available (via export lists), and thus control abstraction.
    202 
    203 Of course with an `NT` data type, it is possible to define this type class, e.g.
    204 {{{
    205 class NT' a b where
    206   theNT :: NT a b
    207 coerce' :: NT' a b => a -> b
    208 coerce' = coerce theNT
    209 }}}
    210 and use it where more convenient than the function-based variant.
    211 
    212 As 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).
    213 
    214 Implementation started at [https://github.com/nomeata/nt-coerce/].
    215 
    216 It 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.
    217 
    218 == Type soundness ==
    219 
    220 This proposal rests on very similar foundations to the "newtype deriving" feature,
    221 and suffers from ''precisely'' the same issue with type soundness; see #1496, #5498, #4846, #7148.  For example,
    222 consider
    223 {{{
    224   type family F a
    225   type instance F Int = Int
    226   type instance F Age = Char
    227 
    228   data T a = MkT (F a)
    229 
    230   newtype wrap bad :: T Int -> T Age
    231 
    232   bogus :: Int -> Char
    233  bogus n = case (bad (MkT n)) of
    234               MkT c -> c
    235 }}}
    236 The problem is, as usual, the type function hiding inside T's definition.
    237 The solution is described in [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ Generative type abstraction and type-level computation].  It is still being implemented, alas,
    238 but adding the newtype wrappers introduces no problems that we do not already have. See [wiki:Roles] for more info.
    239 
    240 
     98One problem with this approach is that if the user can use arbitrary Haskell to mange the `NT` values, he can create bottoms. Also, additional syntax is required. It was [http://www.haskell.org/pipermail/ghc-devs/2013-July/001667.html argued] that the benefits over the type-class apporoach (Approach 2) do not warrant the extra syntactical complexity.