can/should Functor have a quantified coercible constraint?

Sun Jan 3 19:40:43 UTC 2021

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 <carter.schonwald at gmail.com>
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 <
> carter.schonwald at gmail.com> 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 <oleg.grenrus at iki.fi> 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 <oleg.grenrus at 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 <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#traverseBia> :: (Traversable t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090275>, Biapplicative <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Biapplicative> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090274>)            => (a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090273> -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090274> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090272> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090271>) -> t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090275> a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090273> -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090274> (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090275> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090272>) (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090275> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090271>)traverseBia <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#traverseBia> = inline (traverseBiaWith <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#traverseBiaWith> traverse)
>>>>  --------traverseBiaWith <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#traverseBiaWith> :: forall p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090289> a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090288> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090285> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090284> s <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090287> t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090286>. Biapplicative <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Biapplicative> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090289>  => (forall f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090291> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090290>. Applicative f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090291> => (a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090288> -> f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090291> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090290>) -> s <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090287> -> f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090291> (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090286> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090290>))  -> (a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090288> -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090289> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090285> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090284>) -> s <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090287> -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090289> (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090286> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090285>) (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090286> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090284>)traverseBiaWith <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#traverseBiaWith> trav <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089877> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089876> s <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089875> = smash <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#smash> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089876> (trav <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089877> One <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#One> s <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089875>)
>>>> -------smash <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#smash> :: forall p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090262> t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090258> a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090261> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090260> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090259>. Biapplicative <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Biapplicative> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090262>      => (a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090261> -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090262> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090260> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090259>)      -> (forall x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090264>. Mag <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Mag> a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090261> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090264> (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090258> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090264>))      -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090262> (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090258> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090260>) (t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090258> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090259>)smash <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#smash> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089872> m <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089871> = go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> m <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089871> m <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089871>  where    go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> :: forall x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090249> y <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090248>. Mag <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Mag> a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090261> b <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090260> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090249> -> Mag <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Mag> a <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090261> c <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090259> y <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090248> -> p <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090262> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090249> y <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679090248>    go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> (Pure <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Pure> t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089868>) (Pure <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Pure> u <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089867>) = bipure <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#bipure> t <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089868> u <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089867>    go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> (Map <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Map> f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089865> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089864>) (Map <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Map> g <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089863> y <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089862>) = bimap f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089865> g <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089863> (go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> x <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089864> y <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089862>)    go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> (Ap <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Ap> fs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089860> xs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089859>) (Ap <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#Ap> gs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089858> ys <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089857>) = go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> fs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089860> gs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089858> <<*>> <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#%3C%3C%2A%3E%3E> go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> xs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089859> ys <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089857>
>>>> #if MIN_VERSION_base(4,10,0)    go <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089870> (LiftA2 <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#LiftA2> f <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089855> xs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089854> ys <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089853>) (LiftA2 <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#LiftA2> g <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089852> zs <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089851> ws <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#local-6989586621679089850>) =  <https://hackage.haskell.org/package/bifunctors-5.5.9/docs/src/Data.Biapplicative.html#biliftA2>
>>>>
>>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210103/551c7ff4/attachment-0001.html>