Changes between Version 2 and Version 3 of NewtypeWrappers


Ignore:
Timestamp:
Jan 15, 2013 11:12:27 AM (15 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewtypeWrappers

    v2 v3  
    44indended to make newtypes more flexible and useful.  It tackles head-on  
    55the problem underlying #7542 and #2110. 
     6 
     7Email thread [http://www.haskell.org/pipermail/glasgow-haskell-users/2013-January/023455.html here]. 
    68 
    79== The problem == 
     
    9698}}} 
    9799 
     100== Abstraction == 
     101 
     102Suppose we have 
     103{{{ 
     104        module Map( ... ) where 
     105          data Map a b = ...blah blah... 
     106 
     107        module Age( ... ) where 
     108          newtype Age = MkAge Int 
     109}}} 
     110Now suppose we want a newtype wrapper like this 
     111{{{ 
     112        import Map 
     113        import Age 
     114 
     115        newtype wrap foo :: Map Int Bool -> Map Age Bool 
     116}}} 
     117Could 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`.  
     118 
     119 * 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. 
     120 
     121 * 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. 
     122 
     123Invariants 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. 
     124 
     125One 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.   
     126 
     127But that's not very satisfactory either.   
     128 
     129 * There are some times (like `IO`) where it *does* make perfect sense 
     130   to lift newtypes, but where we really don't want to expose 
     131   the representation.  
     132 
     133 * Actually `Map` is also a good example: while `Map Age Bool` should 
     134   not be converted to `Map Int Bool`, it'd be perfectly fine to convert 
     135   `Map Int Age` to `Map Int Int`. 
     136 
     137 * The criterion must be recursive.  For example if we had 
     138{{{ 
     139         data Map a b = MkMap (InternalMap a b) 
     140}}} 
     141  it's no good being able to see the data constructor `MkMap`; you need to 
     142  see the constructors of `InternalMap` too. 
     143 
     144The 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. 
     145 
     146More thought required. 
    98147 
    99148== Type soundness ==