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