Newtype wrappers

[Simon Peyton-Jones]

| If you as the library writer don't want to allow unsafe things, then
| don't export the constructor.  Then no one can break your invariants,
| even with newtype malarky.  If you as the the library user go and
| explicitly import the bare Set constructor from (theoretical)
| Data.Set.Unsafe, then you are in the position to break Set's internal
| invariants anyway, and have already accepted the great power / great
| responsibility tradeoff.

I think that there are two separate things going on here, and that's why the discussion is confusing.

Suppose we have

	module Map( ... ) where
	  data Map a b = ...blah blah...

	module Age( ... ) where
	  newtype Age = MkAge Int

Now suppose we want a newtype wrapper like this

	import Map
	import Age

	newtype wrap foo :: Map Int Bool -> Map Age Bool

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. In my earlier brief message I was only thinking about the 'Age' type, and forgetting about 'Map'.

- 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.

- 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.

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.

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.  

But that's not very satisfactory either.  

* There are some times (like IO) where it *does* make perfect sense 
  to lift newtypes, but where we really don't want to expose 
  the representation. 

* Actually 'Map' is also a good example: while Map Age Bool should 
  not be converted to Map Int Bool, it'd be perfectly fine to convert 
  Map Int Age to Map Int Int.

* The criterion must be recursive.  For example if we had
	 data Map a b = MkMap (InternalMap a b)
  it's no good being able to see the data constructor MkMap; you need to
  see the constructors of InternalMap too.

The 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" (http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/).  Maybe we should be able to *declare* Map to be indexed (rather than parametric) in its first parameter.

Interesting stuff.

Simon