Newtypes are hell - Haskell

How can I work with polykinded categories without newtypes constantly kicking my ass?

e.g. suppose I have some arrow P :: K -> K -> * for some kind K

now because you can't do normal functional programming with type constructors and typeclasses, you have to make newtypes for things like this:

newtype Flip t a b = Flip { runFlip :: t b a }

ok fine, i'll use newtypes for that. the problem is the isomorphism introduced by the newtype is tied to the category ->

i.e. the isomorphism is t b a -> Flip t a b and Flip t a b -> t b a

but what I need is an isomorphism of the form:

t b a `P` Flip t a b
Flip t a b `P` t b a

the only way to implement this that I can see is to take some unreasonable constraint like Profunctor P, which of course forces P :: * -> * -> *

The newtype idiom just doesn't work beyond very simple use cases. Having type level combinators inextricably tied to term level isomorphisms is a pattern that scales extremely poorly

Would first-class-families help?

first-class-families helps to an extent but it makes for a very strange API if you surface that to your users

Agda <3

what would a solution look like here, asad?

do you need full dep types? or type lambdas? or what would give you enough to solve the problem nicely?

im working on a list of things that are technically or politically infeasible in haskell/ghc today

@Sandy Maguire Would you be interested in a call to just go over what I'm trying to model? I think one of the problems here is I don't know what the solution is, only what the problem is. If we had full dependent types, yes, that would solve the problem, but maybe there's something weaker as well that would solve it nicely.

I would join you if you don't mind :slight_smile: