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: [email protected]
Homepage: http://www.joachim-breitner.de
ICQ#: 74513189
Jabber-ID: [email protected]
signature.asc
Description: This is a digitally signed message part
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
