can/should Functor have a quantified coercible constraint?

[Carter Schonwald]

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[David Feuer]

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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

i guess the issue lies with the `One ` construtor? but the comment along side this datatype already states that its treated as being "unsafe coerced" already! so i dont quite see it  as creating further issues?

On Sun, Jan 3, 2021 at 11:31 AM Carter Schonwald <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Oleg Grenrus]

    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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[David Feuer]

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Oleg Grenrus]

I think Mag, regex-applicative etc. examples are all reparable. The main culprit is however StateT and a like, as you pointed out. It's meaningless to discuss Mag if we cannot even write Functor m => Functor (StateT s m).

> Coercible constraints aren't unpacked in data constructors

Aren't they zero-width at run time? That's IMO a bug if that is not true.

- Oleg

On 3.1.2021 19.08, David Feuer wrote:

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[David Feuer]

Coercible is a lifted constraint wrapping the unlifted constraint, which I remember is spelled either ~#r or some other permutation of those characters. Last I looked, Coercible was *not* unpacked in data constructors.

On Sun, Jan 3, 2021, 12:12 PM Oleg Grenrus <[hidden email]> wrote:

I think Mag, regex-applicative etc. examples are all reparable. The main culprit is however StateT and a like, as you pointed out. It's meaningless to discuss Mag if we cannot even write Functor m => Functor (StateT s m).

> Coercible constraints aren't unpacked in data constructors

Aren't they zero-width at run time? That's IMO a bug if that is not true.

- Oleg

On 3.1.2021 19.08, David Feuer wrote:

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

Isn’t the issue here the first orderness of the current roles system in ghc?  In which case what technological issues should be fixed? That we can’t do this because of limitations in the role system and I feel that doing this sortah change would *force* this to be prioritized.  

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

On Sun, Jan 3, 2021 at 12:15 PM Oleg Grenrus <[hidden email]> wrote:

I think Mag, regex-applicative etc. examples are all reparable. The main culprit is however StateT and a like, as you pointed out. It's meaningless to discuss Mag if we cannot even write Functor m => Functor (StateT s m).

> Coercible constraints aren't unpacked in data constructors

Aren't they zero-width at run time? That's IMO a bug if that is not true.

- Oleg

On 3.1.2021 19.08, David Feuer wrote:

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

So like, for stateT, isn’t the “fix” adding suport for higher order role annotations to surface Haskell? 

On Sun, Jan 3, 2021 at 1:02 PM Carter Schonwald <[hidden email]> wrote:

Isn’t the issue here the first orderness of the current roles system in ghc?  In which case what technological issues should be fixed? That we can’t do this because of limitations in the role system and I feel that doing this sortah change would *force* this to be prioritized.  

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

On Sun, Jan 3, 2021 at 12:15 PM Oleg Grenrus <[hidden email]> wrote:

I think Mag, regex-applicative etc. examples are all reparable. The main culprit is however StateT and a like, as you pointed out. It's meaningless to discuss Mag if we cannot even write Functor m => Functor (StateT s m).

> Coercible constraints aren't unpacked in data constructors

Aren't they zero-width at run time? That's IMO a bug if that is not true.

- Oleg

On 3.1.2021 19.08, David Feuer wrote:

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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) = 

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

In particular; the original design for roles was to attach role info to the kinds of types.  See 

https://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf from 2011 

Since ghc now has pervasive annotations on types internally via the linearity work, enriching those with role information may be a tad more tractable than it was at the time 

On Sun, Jan 3, 2021 at 1:25 PM Carter Schonwald <[hidden email]> wrote:

So like, for stateT, isn’t the “fix” adding suport for higher order role annotations to surface Haskell? 

On Sun, Jan 3, 2021 at 1:02 PM Carter Schonwald <[hidden email]> wrote:

Isn’t the issue here the first orderness of the current roles system in ghc?  In which case what technological issues should be fixed? That we can’t do this because of limitations in the role system and I feel that doing this sortah change would *force* this to be prioritized.  

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

On Sun, Jan 3, 2021 at 12:15 PM Oleg Grenrus <[hidden email]> wrote:

I think Mag, regex-applicative etc. examples are all reparable. The main culprit is however StateT and a like, as you pointed out. It's meaningless to discuss Mag if we cannot even write Functor m => Functor (StateT s m).

> Coercible constraints aren't unpacked in data constructors

Aren't they zero-width at run time? That's IMO a bug if that is not true.

- Oleg

On 3.1.2021 19.08, David Feuer wrote:

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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) = 

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper... so revisiting it and seeing if the original design is worthwhile may be easier than you'd expect!

for my own purposes, i'm doing the approach below / inline  for now ;)

wither :: forall a b f . (Applicative f) =>
        (a -> f (Maybe b)) -> RAList a -> f (RAList b)
wither = \f la ->    coerceWith coerceThroughFunctor     $ QRA.wither f $ coerce la
---
-- applicatives / functors can be coerced under, i have spoken
{-
for context, i otherwise need to do the following :
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
-}
{-#INLINE coerceThroughFunctor #-}
coerceThroughFunctor :: forall a b f.  (Coercible a b, Functor f) => (Coercion (f a) (f b))
coerceThroughFunctor = (unsafeCoerce (Coercion :: Coercion a b  )) :: (Coercion (f a) (f b))

On Sun, Jan 3, 2021 at 2:40 PM Carter Schonwald <[hidden email]> wrote:

In particular; the original design for roles was to attach role info to the kinds of types.  See 

https://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf from 2011 

Since ghc now has pervasive annotations on types internally via the linearity work, enriching those with role information may be a tad more tractable than it was at the time 

On Sun, Jan 3, 2021 at 1:25 PM Carter Schonwald <[hidden email]> wrote:

So like, for stateT, isn’t the “fix” adding suport for higher order role annotations to surface Haskell? 

On Sun, Jan 3, 2021 at 1:02 PM Carter Schonwald <[hidden email]> wrote:

Isn’t the issue here the first orderness of the current roles system in ghc?  In which case what technological issues should be fixed? That we can’t do this because of limitations in the role system and I feel that doing this sortah change would *force* this to be prioritized.  

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

On Sun, Jan 3, 2021 at 12:15 PM Oleg Grenrus <[hidden email]> wrote:

I think Mag, regex-applicative etc. examples are all reparable. The main culprit is however StateT and a like, as you pointed out. It's meaningless to discuss Mag if we cannot even write Functor m => Functor (StateT s m).

> Coercible constraints aren't unpacked in data constructors

Aren't they zero-width at run time? That's IMO a bug if that is not true.

- Oleg

On 3.1.2021 19.08, David Feuer wrote:

Mag uses the One it does for efficiency/compactness. Coercible constraints aren't unpacked in data constructors, sadly. If you're looking for more examples of slightly-invalid but useful Functors, the first place I'd check (beyond the very-Mag-like things in lens that inspired Mag) is Roman Cheplyaka's regex-applicative. I don't know if his lifts coercions or not (haven't looked in a while) but it does some similarly illegitimate things for good reasons.

On Sun, Jan 3, 2021, 12:03 PM Oleg Grenrus <[hidden email]> 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) = 

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Roman Cheplyaka-2]

On 03/01/2021 17.59, Carter Schonwald wrote:
> 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 ..
> ```

I think it's important we keep the definitions of Functor and other
fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

Roman
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

So this actually is a very good point!

Happily, the technological steps needed to resolve issues that other comments so far have raised point to a better fix!

Borrowing from the 2011 paper, we would write the following 

‘’’

class Functor (f : Type/representational -> Type)  where 

‘’’

Basically this then pushes the info into kind signatures.  As was originally intended. And role inferred/ annotated kind signatures provides a mechanism for gnd to work again for monad transformers and unvoxed vector 

On Mon, Jan 4, 2021 at 5:50 AM Roman Cheplyaka <[hidden email]> wrote:

On 03/01/2021 17.59, Carter Schonwald wrote:
> 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 ..
> ```

I think it's important we keep the definitions of Functor and other
fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

Roman
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Richard Eisenberg-5]

On Jan 3, 2021, at 1:02 PM, Carter Schonwald <[hidden email]> wrote:

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

Lifting the limitation would be nice, but it's a lot of work. First, we need an updated theory for Core, with a type safety proof. This proof is essential: it's what our safety as a language depends on. Then, we'd need to implement it. I'm more worried about the former than the latter.

> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...

Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf.

Roman writes:

> I think it's important we keep the definitions of Functor and other

fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

This is tough. I've considered a Functor definition like the one Carter proposes before. I would personally rather come up with the best definition first, then figure out how to make it palatable to newcomers second. For example, we could write (today)

> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)

and then the class constraint looks more pleasant. Or we could create ways of suppressing confusing information. Or there are other solutions. Depending on the benefit of the change (here or elsewhere), I would advocate holding off on making the change until we can support it without disrupting the newcomer story. But I wouldn't want to abandon the idea of an improvement a priori just because of a disruption to the newcomer experience.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

Thx for  the link.  I’ll take a look at your suggested reading. 

What are ways I could help progress whatever’s needed to get to a nice ending?

On Mon, Jan 4, 2021 at 9:00 AM Richard Eisenberg <[hidden email]> wrote:

On Jan 3, 2021, at 1:02 PM, Carter Schonwald <[hidden email]> wrote:

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

Lifting the limitation would be nice, but it's a lot of work. First, we need an updated theory for Core, with a type safety proof. This proof is essential: it's what our safety as a language depends on. Then, we'd need to implement it. I'm more worried about the former than the latter.

> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...

Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf.

Roman writes:

> I think it's important we keep the definitions of Functor and other

fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

This is tough. I've considered a Functor definition like the one Carter proposes before. I would personally rather come up with the best definition first, then figure out how to make it palatable to newcomers second. For example, we could write (today)

> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)

and then the class constraint looks more pleasant. Or we could create ways of suppressing confusing information. Or there are other solutions. Depending on the benefit of the change (here or elsewhere), I would advocate holding off on making the change until we can support it without disrupting the newcomer story. But I wouldn't want to abandon the idea of an improvement a priori just because of a disruption to the newcomer experience.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[John Ericson-2]

I talked to Carter a bit on IRC for my progress on that front, but I thought maybe this would be a good time to mention this more widely

- The constraint side is iffy. Local constraints and constraint kinds make it hard to have some sort of codata guardedness / cotermination checking argument for higher order coercion "instances" that doesn't also need to apply to the constraint system at large, which makes it quite laborious to increase expressive power without trade-offs like no local quantified constraints. (Yay mission creep.)

- The core side looks good. Cale and I pretty confident in the "coercions as fixed points of products", with {0, 1, multiplication, and exponentiation, limits} passing my cardinality sniff test that coercions still have no computational content and thus can be erased.

- Additionally, I am less but decently confident (though I haven't talked to Cale about this) that the existing role admissibility solver can be repurposed to produce those (to-be-erased) terms rather than just merely deciding the admissibility of (opaque) axiomatic coercions. This change would have no expressive power implications one way or the other, but complete the "theory refactor" so that the "sans-nth" version could be said to work end to end.

So tl;dr I can't actually do anything to help Carter's problem at the moment, but I think I can get David's https://github.com/ghc-proposals/ghc-proposals/pull/276 over the finish line, with the side benefit of loosening things up and getting us closer so the higher-order roles problem seems less out of reach.

I have revised my "progress report" wildly since I started thinking about these things, but with the latest ratchet back, I think I finally have a stable prediction.

Cheers,

John

On 1/4/21 9:12 AM, Carter Schonwald wrote:

Thx for  the link.  I’ll take a look at your suggested reading. 

What are ways I could help progress whatever’s needed to get to a nice ending?

On Mon, Jan 4, 2021 at 9:00 AM Richard Eisenberg <[hidden email]> wrote:

On Jan 3, 2021, at 1:02 PM, Carter Schonwald <[hidden email]> wrote:

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

Lifting the limitation would be nice, but it's a lot of work. First, we need an updated theory for Core, with a type safety proof. This proof is essential: it's what our safety as a language depends on. Then, we'd need to implement it. I'm more worried about the former than the latter.

> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...

Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf.

Roman writes:

> I think it's important we keep the definitions of Functor and other

fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

This is tough. I've considered a Functor definition like the one Carter proposes before. I would personally rather come up with the best definition first, then figure out how to make it palatable to newcomers second. For example, we could write (today)

> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)

and then the class constraint looks more pleasant. Or we could create ways of suppressing confusing information. Or there are other solutions. Depending on the benefit of the change (here or elsewhere), I would advocate holding off on making the change until we can support it without disrupting the newcomer story. But I wouldn't want to abandon the idea of an improvement a priori just because of a disruption to the newcomer experience.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Keith]

Currently:

head ~(a :| _) = a
tail ~(_ :| as) = as

But head and tail are both strict. At best the '~'s have no effect.

Should I open a PR to change it to

head (a :| _) = a
tail (_ :| as) = as

or maybe even more clearly

head !(a :l _) = a
tail !(_ :| as) = as

?
--Keith
Sent from my phone with K-9 Mail.

On January 4, 2021 2:40:58 PM UTC, John Ericson <[hidden email]> wrote:

I talked to Carter a bit on IRC for my progress on that front, but I thought maybe this would be a good time to mention this more widely

- The constraint side is iffy. Local constraints and constraint kinds make it hard to have some sort of codata guardedness / cotermination checking argument for higher order coercion "instances" that doesn't also need to apply to the constraint system at large, which makes it quite laborious to increase expressive power without trade-offs like no local quantified constraints. (Yay mission creep.)

- The core side looks good. Cale and I pretty confident in the "coercions as fixed points of products", with {0, 1, multiplication, and exponentiation, limits} passing my cardinality sniff test that coercions still have no computational content and thus can be erased.

- Additionally, I am less but decently confident (though I haven't talked to Cale about this) that the existing role admissibility solver can be repurposed to produce those (to-be-erased) terms rather than just merely deciding the admissibility of (opaque) axiomatic coercions. This change would have no expressive power implications one way or the other, but complete the "theory refactor" so that the "sans-nth" version could be said to work end to end.

So tl;dr I can't actually do anything to help Carter's problem at the moment, but I think I can get David's https://github.com/ghc-proposals/ghc-proposals/pull/276 over the finish line, with the side benefit of loosening things up and getting us closer so the higher-order roles problem seems less out of reach.

I have revised my "progress report" wildly since I started thinking about these things, but with the latest ratchet back, I think I finally have a stable prediction.

Cheers,

John

On 1/4/21 9:12 AM, Carter Schonwald wrote:

Thx for  the link.  I’ll take a look at your suggested reading. 

What are ways I could help progress whatever’s needed to get to a nice ending?

On Mon, Jan 4, 2021 at 9:00 AM Richard Eisenberg <[hidden email]> wrote:

On Jan 3, 2021, at 1:02 PM, Carter Schonwald <[hidden email]> wrote:

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

Lifting the limitation would be nice, but it's a lot of work. First, we need an updated theory for Core, with a type safety proof. This proof is essential: it's what our safety as a language depends on. Then, we'd need to implement it. I'm more worried about the former than the latter.

> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...

Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf.

Roman writes:

> I think it's important we keep the definitions of Functor and other

fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

This is tough. I've considered a Functor definition like the one Carter proposes before. I would personally rather come up with the best definition first, then figure out how to make it palatable to newcomers second. For example, we could write (today)

> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)

and then the class constraint looks more pleasant. Or we could create ways of suppressing confusing information. Or there are other solutions. Depending on the benefit of the change (here or elsewhere), I would advocate holding off on making the change until we can support it without disrupting the newcomer story. But I wouldn't want to abandon the idea of an improvement a priori just because of a disruption to the newcomer experience.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[David Feuer]

The first one. Neither twiddles nor bangs are useful or add clarity.

On Fri, Jan 8, 2021, 11:53 AM Keith <[hidden email]> wrote:

Currently:

head ~(a :| _) = a
tail ~(_ :| as) = as

But head and tail are both strict. At best the '~'s have no effect.

Should I open a PR to change it to

head (a :| _) = a
tail (_ :| as) = as

or maybe even more clearly

head !(a :l _) = a
tail !(_ :| as) = as

?
--Keith
Sent from my phone with K-9 Mail.

On January 4, 2021 2:40:58 PM UTC, John Ericson <[hidden email]> wrote:

I talked to Carter a bit on IRC for my progress on that front, but I thought maybe this would be a good time to mention this more widely

- The constraint side is iffy. Local constraints and constraint kinds make it hard to have some sort of codata guardedness / cotermination checking argument for higher order coercion "instances" that doesn't also need to apply to the constraint system at large, which makes it quite laborious to increase expressive power without trade-offs like no local quantified constraints. (Yay mission creep.)

- The core side looks good. Cale and I pretty confident in the "coercions as fixed points of products", with {0, 1, multiplication, and exponentiation, limits} passing my cardinality sniff test that coercions still have no computational content and thus can be erased.

- Additionally, I am less but decently confident (though I haven't talked to Cale about this) that the existing role admissibility solver can be repurposed to produce those (to-be-erased) terms rather than just merely deciding the admissibility of (opaque) axiomatic coercions. This change would have no expressive power implications one way or the other, but complete the "theory refactor" so that the "sans-nth" version could be said to work end to end.

So tl;dr I can't actually do anything to help Carter's problem at the moment, but I think I can get David's https://github.com/ghc-proposals/ghc-proposals/pull/276 over the finish line, with the side benefit of loosening things up and getting us closer so the higher-order roles problem seems less out of reach.

I have revised my "progress report" wildly since I started thinking about these things, but with the latest ratchet back, I think I finally have a stable prediction.

Cheers,

John

On 1/4/21 9:12 AM, Carter Schonwald wrote:

Thx for  the link.  I’ll take a look at your suggested reading. 

What are ways I could help progress whatever’s needed to get to a nice ending?

On Mon, Jan 4, 2021 at 9:00 AM Richard Eisenberg <[hidden email]> wrote:

On Jan 3, 2021, at 1:02 PM, Carter Schonwald <[hidden email]> wrote:

This limitation is a misfeature, how can we make this get addressed sooner rather than later? Is this somewhere where Eg Haskell foundation or something could help?

Lifting the limitation would be nice, but it's a lot of work. First, we need an updated theory for Core, with a type safety proof. This proof is essential: it's what our safety as a language depends on. Then, we'd need to implement it. I'm more worried about the former than the latter.

> i think its worth emphasizing that ghc today uses a simplification of the original 2011 paper...

Yes, that was originally true, but the current formulation goes beyond the 2011 paper in some respects. See section 7.1 of https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf.

Roman writes:

> I think it's important we keep the definitions of Functor and other

fundamental classes understandable by newcomers, and this change would
make the definition look scary for a marginal benefit.

This is tough. I've considered a Functor definition like the one Carter proposes before. I would personally rather come up with the best definition first, then figure out how to make it palatable to newcomers second. For example, we could write (today)

> type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)

and then the class constraint looks more pleasant. Or we could create ways of suppressing confusing information. Or there are other solutions. Depending on the benefit of the change (here or elsewhere), I would advocate holding off on making the change until we can support it without disrupting the newcomer story. But I wouldn't want to abandon the idea of an improvement a priori just because of a disruption to the newcomer experience.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Tom Ellis-5]

On Fri, Jan 08, 2021 at 04:52:33PM +0000, Keith wrote:

> Currently:
>
>    head ~(a :| _) = a
>    tail ~(_ :| as) = as
>
> But head and tail are both strict. At best the '~'s have no effect.
>
> Should I open a PR to change it to
>
>    head (a :| _) = a
>    tail (_ :| as) = as

I would support that.  It would be nice if GHC warned about misleading
lazy patterns.

> or maybe even more clearly
>
>    head !(a :l _) = a
>    tail !(_ :| as) = as

Why do you say "more clearly"?  Every pattern match is strict, more or
less by definition[1] so I don't see how a bang pattern adds anything.
If this is more clear then shouldn't we make the case to do it to
*every* pattern match everywhere?

Tom



[1] with the exception of weird edge cases around pattern synonyms:

pattern Pat :: p
pattern Pat <- _

pattern LPat :: a -> Maybe a
pattern LPat a <- ~(Just a)

f :: a -> Int
f Pat = 1
f _ = 2

f' :: a -> Int
f' !Pat = 1
f' _ = 2

g :: Maybe a -> Int
g (LPat _) = 1
g _ = 2

g' :: Maybe a -> Int
g' (LPat _) = 1
g' _ = 2
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries