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@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata@joachim-breitner.de