Hello,

The general functionality for this seems useful, but we should be careful exactly what types we allow in the 'newtype wrap/unwrap' declarations. For example, would we allow something like this:

newtype wrap cvt :: f a -> f (Dual a)

If we just worry about what's in scope, then it should be accepted, however this function could still be used to break the invariant on `Set` because it is polymorphic.

In general, I was never comfortable with GHC's choice to add an axiom equating a newtype and its representation type, because it looks unsound to me (without any type-functions or newtype deriving).

For example, consider:

newtype T a = MkT Int

Now, if this generates an axiom asserting that `froall a. T a ~ Int`, then we can derive a contradiction:

T Int ~ Int ~ T Char, and hence `Int ~ Char`.

It looks like what we need is a different concept: one that talks about the equality of the representations of types, rather then equality of the types themselves.

-Iavor

On Mon, Jan 14, 2013 at 10:09 AM, Simon Peyton-Jones <simonpj@microsoft.com> wrote:

Friends

I’d like to propose a way to “promote” newtypes over their enclosing type. Here’s the writeup

          http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers

Any comments? Below is the problem statement, taken from the above page.

I’d appreciate

·         A sense of whether you care. Does this matter?

·         Improvements to the design I propose

Simon

The problem

Suppose we have
newtype Age = MkAge Int
Then if n :: Int, we can convert n to an Age thus: MkAge n :: Age. Moreover, this conversion is a type conversion only, and involves no runtime instructions whatsoever. This cost model -- that newtypes are free -- is important to Haskell programmers, and encourages them to use newtypes freely to express type distinctions without introducing runtime overhead.

Alas, the newtype cost model breaks down when we involve other data structures. Suppose we have these declarations
data T a   = TLeaf a     | TNode (Tree a) (Tree a)
data S m a = SLeaf (m a) | SNode (S m a) (S m a)
and we have these variables in scope
x1 :: [Int]
x2 :: Char -> Int
x3 :: T Int
x4 :: S IO Int
Can we convert these into the corresponding forms where the Int is replaced by Age? Alas, not easily, and certainly not without overhead.

For x1 we can write map MkAge x1 :: [Age]. But this does not follow the newtype cost model: there will be runtime overhead from executing the map at runtime, and sharing will be lost too. Could GHC optimise the map somehow? This is hard; apart from anything else, how would GHC know that map was special? And it it gets worse.

For x2 we'd have to eta-expand: (\y -> MkAge (x2 y)) :: Char -> Age. But this isn't good either, because eta exapansion isn't semantically valid (if x2 was bottom, seq could distinguish the two). See #7542 for a real life example.

For x3, we'd have to map over T, thus mapT MkAge x3. But what if mapT didn't exist? We'd have to make it. And not all data types have maps. S is a harder one: you could only map over S-values if m was a functor. There's a lot of discussion abou this on #2110.
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users