On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <oleg.grenrus@iki.fi> wrote:

Prelude Control.Monad.Trans.State> :i StateT
type role StateT nominal representational nominal

Note, `StateT` is nominal in last argument (a). Thus if (forall c d. Coercible ...) where a Functor superclass, Functor (and thus Monad) wouldn't be definable for StateT. That would be... unfortunate.

Until there are "higher roles" Functor cannot be Coercible1. It would rule very simple code.
(OTOH Mag can be repaired, https://oleg.fi/gists/posts/2019-07-31-fmap-coerce-coerce.html#functor-should-be-parametric).

- Oleg

On 3.1.2021 18.31, Carter Schonwald wrote:
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
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries