Sounds amazing Joachim -- great work.
| Consider
| data Foo a = MkFoo (a,a).
| The (virtual) instance
| instance Coercible a b => Coercible (Foo a) (Foo b)
| can only be used when MkFoo is in scope, as otherwise the user could
| break abstraction barriers. This is enforced.
Whoa! Where did this instance come from? I thought that we generated
precisely two (virtual) instances for Foo:
instance Coercible a (b,b) => Coercible a (Foo b)
instance Coercible (a,b) b => Coercible (Foo a) b
and no others. That it. Done. That was precisely the payload of my message
of 2 August, attached.
Each of the two is valid if the data constructor MkFoo is in scope. No other
checks are needed.
| Assume MkFoo is not in scope. Then the user could
| define
| data Hack a = MkHack (Foo a)
| and use the (virtual) instance
| instance Coercible a b => Coercible (Hack a) (Hack b)
No no no! The virtual instances are
instance Coercible (Foo a) b => Coercible (Hack a) b
instance Coercible a (Foo b) => Coercible a (Hack b)
and now the difficulty you describe disappears.
| But it might, in corner cases, be too strict. Consider
| data D a b = MkD (a, Foo b)
| now the programmer might expect that, even without MkFoo in scope, that
| instance Coercible a b => Coercible (D a c) (D b c)
The two instances are
instance Coercible (a, Foo b) x => Coercible (D a b) x
instance Coercible x (a, Foo b) => Coercible x (D a b)
Now can I prove (Coercible (D a c) (D b c))?
Use the above rules twice; I then need
Coercible (a, Foo c) (b, Foo c)
and yes I can prove that if I have (Coerciable a b).
In short, I think that if you use the approach I outlined, all these problems
go away. Am I wrong?
Simon
--- Begin Message ---
Joachim
I was talking to Stepanie about newtype wrappers, and realised that
a) there are two very different ways to use type classes to
implement the feature, one good and one bad
b) the one I thought we were using is the Bad One
c) the one on the wiki page is sketched in far too little detail
but is the Good One
http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers
Also, there's an interaction with "roles" which Richard is on the point of
committing.
Below are some detailed notes.
Before too long, could you refresh the wiki page to:
* demote rejected ideas
* explain the accepted plan in more detail
* discuss implementation aspects
Thanks
Simon
Bad version
~~~~~~~~~~~
class NT a b
rep :: NT a b => a -> b
wrap :: NT a b => b -> a
Then for each newtype
newtype Age = Int
we generate
axiom axAge :: Age ~ Int
instance NT Age Int
and for data types
data (a,b) = (a,b)
we generate
instance (NT a a', NT b b') => NT (a,b) (a',b')
Internally (NT a b) is implemented as a simple boxing of a
representational equality:
data NT a b = MkNT (a ~#R b)
There are many problems here
- It's tiresome for the programmer to remember whether
to use rep or wrap
- Many levels of newtype would require repeated application
of rep (or wrap). But if I say (rep (rep x)) I immediately
get ambiguity, unless I also supply a type sig for each
intermediate level.
Good version (this may be what you are doing already)
~~~~~~~~~~~~
class NT a b
ntCast :: NT a b => a -> b
Notice only one ntCast, which will work both ways.
Then for each newtype
newtype Age = Int
we generate
axiom axAge :: Age ~ Int
instance NT Int b => NT Age b
instance NT a Int => NT b Age
Notice *two* instances
For data types, same as before
data (a,b) = (a,b)
we generate
instance (NT a a', NT b b') => NT (a,b) (a',b')
And we have instance NT a a.
Now try this
f :: (Age, Bool, Int) -> (Int, Bool, Age)
f x = ntCast x
>From the ntCast we get the wanted constraint
NT (Age,Bool,Int) (Int,Bool,Age)
Then we simplify as follows
NT (Age,Bool,Int) (Int,Bool,Age)
---> by instance decl for (,,)
NT Age Int, NT Bool Bool, NT Int Age
---> by instance NT a a, solves NT Bool Bool
NT Age Int, NT Int Age
---> by instance NT Int a => NT Age a
NT Int Int, NT Int Age
---> by instance NT a a, solves NT Int Int
NT Int Age
...and so on...
In effect, we normalise both arguments of the NT independently
until they match (are equal, or have an outermost list). This
will even do a good job of
newtype Moo = MkMoo Age
f :: Moo -> Age
f x = ntCast x
Try it.. it'll normalise the (NT Moo Age) to (NT Int Int), so the
coercion we ultimately build wil take x down to Int, then back up
to Age. But that's fine... the coercion optimiser will remove the
intermediate steps.
This has lots of advantages:
- No need to remember directions; ntCast does the job in either
direction or both
- No need for multiple levels of unwrapping... and hence no
ambiguity for the intermediate steps.
A note about roles
~~~~~~~~~~~~~~~~~~
We are very keen that if we declare
data Map key val = [(key,val)]
where the keys are kept ordered, then we do NOT want to allow
a cast from (Map Int val) to (Map Age val)
We were thinking about exercising this control by saying, in
a standalone deriving clause
deriving NT v1 v2 => NT (Map k v1) (Map k v2)
But another, and more robust, way to express the fact that we
should not allow you to cast (Map Int val) to (Map Age val) is
to give Map the rules
p Map key@Nominal val@Representational
in Richard's new system (about to be committed). This gives
Map's first argument a more restrictive role than role inference
would give it.
And for good reason! If we had
class C k where
foo :: Map k Int -> Bool
then we would NOT want to allow
newtype Age = MkAge Int deriving( C )
And the thing that now prevents us doing that 'deriving( C )' is
precisely the more restrictive role on Map.
So, our proposal is: for every
data T a = ... deriving( NT )
we get the lifting instance
instance NT a b => NT (T a) (T b)
whose shape is controlled by T's argument roles.
We probably want to be able to say -XAutoDeriveNT, like -XAutoDeriveTypeable.
--- End Message ---
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
