Exposing newtype coercions to Haskell
Joachim Breitner
mail at joachim-breitner.de
Tue Jul 23 13:45:04 CEST 2013
Hi,
Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
> I think that thinking about the base case is also
> productive, but I don't have a clear enough opinion to express on that
> front.
and it seems to tricky; Here we are hitting problems that we did not
have with the non-class-approach.
tl;dr: "IsNT a a" only works with IncoherentInstances, which are in
principle fine for this class (it is univalent in a sense), but
requiring this extension would be quite unfortunate.
Consider this ghci session (this already works here):
Prelude GHC.NT> newtype Age = Age Int deriving Show
Prelude GHC.NT> deriving instance IsNT Int Age
Prelude GHC.NT> castNT (1::Int) :: Age -- good, works
Age 1
Prelude GHC.NT> deriving instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Age -- also works
Left (Age 1)
Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- does not work yet
<interactive>:12:1:
No instance for (IsNT Int Int) arising from a use of ‛castNT’
In the expression:
castNT (Left 1 :: Either Int Int) :: Either Age Int
In an equation for ‛it’:
it = castNT (Left 1 :: Either Int Int) :: Either Age Int
Prelude GHC.NT> deriving instance IsNT Int Int
Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- works now
Left (Age 1)
Prelude GHC.NT> :t castNT :: (Either Int Int) -> (Either Age Int)
castNT :: (Either Int Int) -> (Either Age Int) :: Either Int Int -> Either Age Int
But we are not able to cast such that one type parameter changes while
leaving another type _variable_ untouched:
Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a)
<interactive>:1:1:
No instance for (IsNT a1 a1) arising from a use of ‛castNT’
Possible fix:
add (IsNT a1 a1) to the context of
an expression type signature: Either Int a1 -> Either Age a1
or the inferred type of it :: Either Int a -> Either Age a
In the expression: castNT :: (Either Int a) -> (Either Age a)
and if we add "IsNT a a" as a base case:
Prelude GHC.NT> instance IsNT a a
<interactive>:34:10: Warning:
No explicit method or default declaration for ‛coercion’
In the instance declaration for ‛IsNT a a’
we get
Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a)
<interactive>:1:1:
Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’
Matching instances:
instance [overlap ok] IsNT a a -- Defined at <interactive>:34:10
instance IsNT Int Int -- Defined at <interactive>:13:1
instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
-- Defined at <interactive>:10:1
(The choice depends on the instantiation of ‛a1’
To pick the first instance above, use -XIncoherentInstances
when compiling the other instance declarations)
In the expression: castNT :: (Either Int a) -> (Either Age a)
Re-doing the session with -XIncoherentInstances set helps, but requiring
that for every module that wants to derive a IsNT class is probably not
nice.
The one-parameter-variant does not help either.
One way to avoid the issue is to have two instances for Either:
Prelude GHC.NT> deriving instance (IsNT a a') => IsNT (Either a b) (Either a' b)
Prelude GHC.NT> deriving instance (IsNT b b') => IsNT (Either a b) (Either a b')
This still requires OverlappingInstances, but I can get the desired cast
without IncoherentInstances:
Prelude GHC.NT> :t castNT :: Either Int a -> Either Age a
castNT :: Either Int a -> Either Age a
:: Either Int a -> Either Age a
Other casts that should be “normal” are more complicated now:
Prelude GHC.NT> let c = (castNT :: Either Age Int -> Either Age Age) . (castNT :: Either Int Int -> Either Age Int)
Prelude GHC.NT> :t c
c :: Either Int Int -> Either Age Age
Prelude GHC.NT> c (Left 1)
Left (Age 1)
In any case, the whole thing needs a bit more massaging until it becomes
sufficiently elegant.
Greetings,
Joachim
--
Joachim Breitner
e-Mail: mail at joachim-breitner.de
Homepage: http://www.joachim-breitner.de
ICQ#: 74513189
Jabber-ID: nomeata at joachim-breitner.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130723/795d6de2/attachment.pgp>
More information about the ghc-devs
mailing list