Hey David,
could you exposit what would go wrong? a concrete proof witness or explanation would help me a lot. other people might benefit too.


for the stateT s Maybe a, perhaps i'm still waking up this AM, so let me try
newtype StateT s m a = StateT {runStateT :: s -> m (a, s)}

so this should expand to 
'(s -> Maybe (a,s)),'
but the coerce would be on the 'a' here ... so i'm not seeing the issue?



the latter example seem to boil down to "a free appplicative/functor Gadt" with some extra bits, though i've not worked through to seeing the unsafety
for the latter examples, the definitions are the following :
traverseBia :: (Traversable t, Biapplicative p)
            => (a -> p b c) -> t a -> p (t b) (t c)
traverseBia = inline (traverseBiaWith traverse)
--------
traverseBiaWith :: forall p a b c s t. Biapplicative p => (forall f x. Applicative f => (a -> f x) -> s -> f (t x)) -> (a -> p b c) -> s -> p (t b) (t c) traverseBiaWith trav p s = smash p (trav One s)
-------
smash :: forall p t a b c. Biapplicative p => (a -> p b c) -> (forall x. Mag a x (t x)) -> p (t b) (t c) smash p m = go m m where go :: forall x y. Mag a b x -> Mag a c y -> p x y go (Pure t) (Pure u) = bipure t u go (Map f x) (Map g y) = bimap f g (go x y) go (Ap fs xs) (Ap gs ys) = go fs gs <<*>> go xs ys #if MIN_VERSION_base(4,10,0) go (LiftA2 f xs ys) (LiftA2 g zs ws) = biliftA2 f g (go xs zs) (go ys ws) #endif go (One x) (One _) = p x go _ _ = impossibleError

---- and then the magma is 
-- This is used to reify a traversal for 'traverseBia'. It's a somewhat -- bogus 'Functor' and 'Applicative' closely related to 'Magma' from the -- @lens@ package. Valid traversals don't use (<$), (<*), or (*>), so -- we leave them out. We offer all the rest of the Functor and Applicative -- operations to improve performance: we generally want to keep the structure -- as small as possible. We might even consider using RULES to widen lifts -- when we can: -- -- liftA2 f x y <*> z ==> liftA3 f x y z, -- -- etc., up to the pointer tagging limit. But we do need to be careful. I don't -- *think* GHC will ever inline the traversal into the go function (because that -- would duplicate work), but if it did, and if different RULES fired for the -- two copies, everything would break horribly. -- -- Note: if it's necessary for some reason, we *could* relax GADTs to -- ExistentialQuantification by changing the type of One to -- -- One :: (b -> c) -> a -> Mag a b c -- -- where the function will always end up being id. But we allocate a *lot* -- of One constructors, so this would definitely be bad for performance. data Mag a b t where Pure :: t -> Mag a b t Map :: (x -> t) -> Mag a b x -> Mag a b t Ap :: Mag a b (t -> u) -> Mag a b t -> Mag a b u #if MIN_VERSION_base(4,10,0) LiftA2 :: (t -> u -> v) -> Mag a b t -> Mag a b u -> Mag a b v #endif One :: a -> Mag a b b instance Functor (Mag a b) where fmap = Map instance Applicative (Mag a b) where pure = Pure (<*>) = Ap #if MIN_VERSION_base(4,10,0) liftA2 = LiftA2 #endif



On Sun, Jan 3, 2021 at 11:09 AM David Feuer <david.feuer@gmail.com> wrote:
You're not being very imaginative at all. Try out, oh, `StateT s Maybe`. Or play around with a nice fake functor like the magma used to implement `traverseBia` in `bifunctors`—pretty sure that won't work out.

On Sun, Jan 3, 2021, 11:00 AM Carter Schonwald <carter.schonwald@gmail.com> wrote:
Hey everyone!

for context, I have some code where I was seeing how far coerce lets me go to avoid doing wrappers for certain codes,

i found i had to write the following (mapping an operation over to its newtyped sibling)

```
-- > :t QRA.wither
--- forall a b f . Applicative f => (a -> f (Maybe b)) -> RAList a -> f (RAList b)
---
wither :: forall a b f . (Applicative f, (forall c d .  Coercible c d => Coercible (f c) (f d))  ) =>
        (a -> f (Maybe b)) -> RAList a -> f (RAList b)
wither = \f la ->    coerce     $ QRA.wither f $ coerce la
```

i'd much rather be able to write
```
wither :: forall a b f . (Applicative f) =>
        (a -> f (Maybe b)) -> RAList a -> f (RAList b)
wither = \f la ->    coerce     $ QRA.wither f $ coerce la
```


this seems like it'd be best done via something like changing the functor class definition to

```
class (forall c d .  Coercible c d => Coercible (f c) (f d))  ) => Functor f where ..
```

is there any specific reason why this is not feasible? I cant think of a GADT where this wouldn't be totally safe to do (because unlike in foldable, f is in both the domain and co-domain), but maybe i'm not being imaginative enough?

look forward to learning what our obstacles are to making this happen for ghc 9.2 :)

-Carter

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries