Implication constraints, Show1, Eq1, Read1, Ord1

irc.log

mniip
edwardk, I think I just came up with the most complicated solution to the Show1 problem 
phadej
Show1 problem? 
mniip
instance Show (IdentityT m a) where ??? 
phadej
and your solution is? 
mniip
coming up 
(this margin is too narrow to contain it) 
phadej
:) 
edwardk
i just want an internal hom for Constraint 
then 
deriving instance (Show a |- Show (f a), Show a) => Show (Jet f a) 
not a perfect Show1 but its progress 
and would let you express many instances that need polymorphic recursion 
RyanGlScott
"Internal hom" meaning "implication constraints"? 
i.e, https://ghc.haskell.org/trac/ghc/ticket/2256 ? 
mniip
edwardk, you mean ((forall x. Show x |- Show (f x)), Show a) 
edwardk
that would be needed in this case yeah 
ryanglscott: yeah 
edwardk
mniip the usual way i try to worl the example is to show that |- :: (k -> Constraint) -> ( k -> Constraint) -> Constraint etc. is definable by induction 
then use Show |- Compose Show f 
but that needs more from Compose 
mniip
edwardk, I'm thinking of fmap vs runNT fmap 
and thinking a similar approach could be used for, say, show 
but it's not quite a category 
mniip
we're looking for show :: c a String 
mniip
where c is either an encoding of (->), or something like '/\a b -> forall x. Show x => a x -> b' 
/\a b -> forall x. Show x => d (a x) b 
like a lopsided NT 
mniip
tempted to say 'NT _ Identity' but the kind is not fancy enough 
mniip
I think I found a ghc bug... 
shapr
ooh, tell me more 
RyanGlScott
Agreed 
mniip
bonus points 
I can Show (Identity Proxy a) 
IdentityT* 
mniip
yeah, not a ghc bug, I just overlooked some constraints 
lpaste
mniip pasted “Show” at http://lpaste.net/355969 
mniip
edwardk, ^