Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Created Jun 1, 2017
Embed
What would you like to do?
Implication constraints, Show1, Eq1, Read1, Ord1
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, ^
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment