Changes between Version 2 and Version 3 of NewtypeWrappers

Jan 15, 2013 11:12:27 AM (3 years ago)



  • NewtypeWrappers

    v2 v3  
    44indended to make newtypes more flexible and useful.  It tackles head-on
    55the problem underlying #7542 and #2110.
     7Email thread [ here].
    79== The problem ==
     100== Abstraction ==
     102Suppose we have
     104        module Map( ... ) where
     105          data Map a b = ...blah blah...
     107        module Age( ... ) where
     108          newtype Age = MkAge Int
     110Now suppose we want a newtype wrapper like this
     112        import Map
     113        import Age
     115        newtype wrap foo :: Map Int Bool -> Map Age Bool
     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`.
     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.
     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.
     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.
     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. 
     127But that's not very satisfactory either. 
     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.
     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`.
     137 * The criterion must be recursive.  For example if we had
     139         data Map a b = MkMap (InternalMap a b)
     141  it's no good being able to see the data constructor `MkMap`; you need to
     142  see the constructors of `InternalMap` too.
     144The 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.
     146More thought required.
    99148== Type soundness ==