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 |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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) ---- and then the magma is
On Sun, Jan 3, 2021 at 11:09 AM David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Carter Schonwald
Prelude Control.Monad.Trans.State> :i StateT - Oleg On 3.1.2021 18.31, Carter Schonwald
wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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). On 3.1.2021 19.08, David Feuer wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Oleg Grenrus
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In particular; the original design for roles was to attach role info to the kinds of types. See 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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Carter Schonwald
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 |
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: _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Carter Schonwald
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 wouldmake 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 |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
The first one. Neither twiddles nor bangs are useful or add clarity. On Fri, Jan 8, 2021, 11:53 AM Keith <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Keith
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 |
Free forum by Nabble | Edit this page |