Changes between Version 2 and Version 3 of NewtypeWrappers


Ignore:
Timestamp:
Jan 15, 2013 11:12:27 AM (3 years 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 ==