Roadmap - Polysemy

@Love Waern (King of the Homeless) @Georgi Lyubenov // googleson78 We should talk a little bit about polysemy's roadmap - there're a few things that I think would be worth sorting out. My thoughs:

• performance - 8.10 is slowly approaching and with it's release we would probably expect polysemy to fulfil expectations that Sandy set in our README - that means we want to make sure we thoroughly test it's behaviour in both microbenchmarks and more real-world-like examples. Plus, I guess it could be helpful to coordinate forces with Alexis - her work on eff could help us point out flaws in our own system.

• fake fundeps - I think it would be good idea to investigate possibility of splitting plugin from the library - currently it's strongly tied to internal machinery, even though the concept could potentially work for any type of constraints and could be useful for other libraries. Plus, building some exact model around how it should work would possibly help us make sure that it's actually sound and safe - typechecker plugins are moving on very thin ice by being able to prove whatever bogus constraint they want.

• named effects - We should investigate problems related with having multiple effects of same type in stack - is the type of effect it's key identifier or should we move towards model based on named effects to avoid ambiguity? Can row polymorphism help us? Or we want to get aggressive at newtype-ing?

• tactics - Last year during Sandy's visit to Bratislava we sat down and discussed implementation of Weaving to make sure I have good idea about how it behaves - but even after building my own toy version of polysemy, I'm not sure if I can hold reasonable model of it's behaviour in my head in real world scenarios. Problem is, while users don't have to interact with internals directly, they tend to return back to us with all sorts of questions and issues related to tactics/strategies, simply because why they can write higher-order interpretations that typecheck, they can't reason about heir behaviour efficiently. I remember that at some point, Sandy himself considered idea of Sem fixed in IO as final effect, simply to make reasoning about library's behaviour easier. What are your thoughts on this?

This is obviously my point of view and I may be missing something - what do you think?

re: named effects, what is your opinion on tagged, it seems to be very related? I haven't tried it out in practice.
I think tactics/strategy stuff could use a lot of examples with comments/explanations, and if/when I get a grasp of what's going on there I would sit down to write some, but that is unfortunately not the case right now

There are also some "hanging" prs that seem to have been put on hold? Particularly 239 and 242 seem of interest

@Georgi Lyubenov // googleson78 I've mixed feelings about using Symbols (~ Strings) for choosing effects - if they're worth a name, shouldn't that be real identifier instead of a string? I mean, if two module define Tagged "counter" (State Int), I doubt they're going to mean the same thing - but compiler will treat them the same...

In general, we give values names, because real types usually have multiple inhabitants - isn't it the same with effects? The fact that some two effects have the same type does not imply they are the same - need for Tagged basically points that out.

What I imagine is model where omitting effect's identifier in signature means "I work over arbitrary effect of such type" - that's the case of common combinators. And in user code, identifiers that tell me "this is the state that counts team members", "this is the reader that keeps fallback config".

Without identifier, we could do fake fundeps - if we fail, we ask for it.

• Performance - I definitely agree. This is one of my weak spots, both preparing a benchmarking environment, doing proper benchmarks, and analyzing core.
• It would be difficult to split the plugin from the library seeing how the plugin needs some kind of idea of what constraints it should focus on. Regarding the safety; from what I understood, what the fundep library does is generate additional type equality constraints which provides enough information for the type-checker to eliminate ambiguities and resolve type-checking. Does it actually generate bogus proofs?
• Multiple completely identical effects can definitely be part of the same effect stack, and the type of the effect is not its key identifier. The way ambiguities are resolved is thatMember targets the first instance of the named effect in the effect stack, which usually results in the behaviour you'd want. The effects in polysemy are mostly intended as primitives, of which you can reinterpret other effects to, or build newtypes upon; so named effects are already (mostly) the way to go the way to go for more intricate applications.. I'd favour effect newtypes/reinterpretation rather than Tagged here.
• I feel that the confusion about tactics can be resolved through good documentation and a tutorial. I can help a lot with this. Regarding Sem fixed in IO: that would be very sad, because we'd lose a big chunk of the testing/mocking story. Despite how much I rag on the weave abstraction, it works well enough for most purposes, and once we document tactics well enough, it will become sufficiently usable.
  Edit: missed the semantic behaviour part of your comment. Yeah, this is where the use of the weave abstraction hurts -- it can get really damn stupid and confusing -- and there's no way to fix this without shifting abstractions (which I'm hesitant towards unless we can find a drop-in replacement that is pretty much strictly better), or documenting the hell out of it. And since weave is so confusing, the documentation will be hard to write.

I'd also like to add the additional point:

• Documentation. There's a lot of documentation work I want to get done, especially making it clear how tactics work. This includes tutorials. 232 and 234 are the main issues here (but there are other marked as better-docs).

My thoughts was that the Strategy rework, deletion of deprecated code, documentation, and potentially even 8.10-oriented optimizations would all be released as part of v2.0. I can compile what we said here into a check-list issue for v2.0 on Friday - if there's anything (small or big) that we haven't mentioned already, toss it here.

Thoughts?

@Love Waern (King of the Homeless)

• It seems to me that the idea of plugin is basically "functional dependency that get's dropped if it isn't satisfied" - polysemy-plugin does some other things too I think, but if they're domain-specific, they could just stay where they are. The thing is, I can imagine this plugin being helpful for something like eff or mtl-wthout-fundeps, or even something like implicit arguments or field access - I hope that if we split it, we can possibly attract more contributors into it, simply because they find it useful in their own libraries - And we'll be able to reason about it separately. When it comes to safety, It already blow up a few times in type-incorrect code for me - it's not that bad, because I still get other errors and it seems to be fine once I resolve them, but this is something that will need to be investigated and something that's harder to test being limited just to Member machinery.
• Yeah, my question basically boils down to "identifiers or newtypes for giving concrete meaning to effect?"
• Yeah, it's the weave I find problematic here. Some time ago, based on thoughts around fixed result, I've created this sort of "compiler"-style prototype, that treat's set of effects as "high-level language" that can be "compiled" into "low-level" monad/stack - this implementation is basically Reader of interpretations over final monad. Such model seems strictly less expressive - you can't "pop" effects from the stack, but they should be arbitrarily "mixable and split-able", with unlifting being pretty easy and completely general: https://gitlab.com/snippets/1903905
• That would be really cool! :slight_smile:
• 2.0 is a big version bump - If we have some breaking changes to make, they should probably be part of it

The check-list is gonna be delayed a day, am busy today

hi

@TheMatten I'd like to talk more about named effects because I don't feel I understand what the issue is about. Is it about what philosophy we should promote when it comes to user-defined effects? Like, the question if they should use out-of-the-box effects like State, with newtyped type parameters, or if they shouldnewtype the effect itself, or create a completely new effect which is then reinterpreted to State, or if they should use Tagged?

What do you mean by "identifiers"?

@Love Waern (King of the Homeless) At value level, we have values that have types:

foo :: Bar
foo = ...

When we want to use some specific value, we name it by it's identifier - simply because most types aren't singletons and so they values may differ.
One could get rid of using identifiers by using newtypes that determine concrete values - you could e.g. define:

class Value t where
  value :: t

newtype FortyTwo = FortyTwo Int

instance Value FortyTwo where
  value = FortyTwo 42

newtype HelloWorld = HelloWorld String

instance Value HelloWorld where
  value = HelloWorld "Hello world!"

This sounds completely ridiculous, right?

But question is, how does it differ from what we do with effects? What if treat effect in row as a value containing some group of actions to be executed, where I can use interpreter to merge that value into other effects, like when you e.g. remove duplicates from the list. What if we instead saw concrete effects in row as values identified by type variables? So instead of:

data PlayerCount m a where ..

-- stuff around interpreting it to primitive effect, e.g. State Int

foo :: Members '[PlayerCount] r => ...

we would have:

foo :: Members { playerCount :: State Int } r => ...

because PlayerCount is actually State Int in same way as 42 is an Int.

Of course, you may encounter effects where concrete representation is internal information - but's already something we experience with newtyped values, e.g. when I have Username represented as Text hidden under newtype. In same way, we would use newtypes to say "I hold some concrete invariants additionally to the actual representation". While in case of playerCount, we're simply talking about mutable Int, with nothing else to hide or capture.

Then, anonymous effects would be the same situation as e.g. use of currying:

showText :: Show a => a -> Text
showText = T.pack . show

has argument, but it's not worth naming - we know it's the one passed to expression inside

in same way, State a in:

get :: Member { _ :: State a } r => Sem r a

is not worth naming - there's just one we can talk about

This would allow us to avoid coerce-ing when we simply want to manipulate properties of effect's representation, in cases where we actually aren't interested in hiding it - where it's type actually describes it's meaning, with identifier specifying concrete group of actions it belongs to

Ok, I think I maybe get it. But can't you do all of this using Tagged? Modolu coerce, of course, and we can't really avoid having to un/wrap newtypes without proper row polymorphism.

Or perhaps a variant of Member that accepts an identifier parameter... hm. But that would require changing the representation of the effect stack so that each effect is associated with an identifier, so effects can be targeted, which just invites confusion when the identifier doesn't matter. Feels like having Tagged is preferable to doing that, so that identifiers are opt-in.

I don't know, but it does warrant discussion, and now I get what it's about. Thanks.

When it comes to row polymorphism... (Disclaimer: I don't want to do anything of this right now, I'm just thinking about future possibilites :big_smile:):

• we could do custom-operator-to-construct-field-in-list-thing and implement it in terms of type-level programming or plugin
• we could actually get { a :: B, c :: D } syntax in current Haskell, with a plugin - fact is that GHC parser parses rows just fine, it just throws error during later stages - we can transform them into our representation before that happens

Yeah, it's probably not reasonable to do that now - but I would like to think about way we want to move in the future

I'm still scared of ambiguity of Tagged strings, and coercing just doesn't look right - there are actually two ways of understanding identifiers:

• they're sort of "named constraints", where names apply in current definition as with function arguments
• they're defined at top level, can be imported/exported

That's basically "safe Tagged vs newtype"

except it behaves differently in cases I mentioned above

Wait, won't identifier names be just as ambiguous as using Tagged with strings as the phantom type parameter? Or do you mean type ambiguity? What makes Tagged (potentially) unsafe?

Let's say I have:

module A where
  foo :: Member (Tagged "log" (Output String)) r => _

module B where
  bar :: Member (Tagged "log" (Output String)) r => _

In some other part of code, I use them together, but forget to point them into corresponding "foo log" and "bar log", having Tagged "log" _ in scope again, because I find it to be a useful pattern for some terrible reason:

do
  ..
  foo _
  bar _
  ..

It happily typechecks - with local model, it would ask "which one is log?", with global it would ask "where is my A.log and B.log?"

Gotcha.

It's obviously a contrived example - but this "What if?" makes me stay awake at night :slight_smile:

Usually it won't be an issue, seeing how named effects are usually only relevant within the scope of a single application - in which case it would be easy to stay consistent. But nevertheless, it is an issue.

I'm worried about possibility of issues popping up - it will be too late if we find out that common uses of Tagged trigger this problem

Yeah.

They may not, they may though - and then such model would be at least a little bit more ergonomic

How the hell would we solve it though? Wouldn't we have the same problem even with row polymorphism?

We'd need a system to have module-local type identifiers

I guess I don't want typical row polymorphism - I just want it's syntax, but with different meaning of field names

Is the API for GHC plugins powerful enough to add type identifiers to the type system?

If you can say off-hand - you have more experience with it than I have.

@Love Waern (King of the Homeless) GHC plugins are like "I let you run at the end of my pass, do whatever you want, but be nice please :joy:" - You have access to basically everything, including AST and uniques generator we need

Neat!

Though, we may need some tricks to make output on :t/:i look nice - plus, parser plugins don't work yet in ghci - if we don't mind making QuasiQuoter for that for now, it wouldn't be that big of problem though

Ok, now I'll just try to find a way to summarize this discussion and put it on the roadmap.

isn't this a problem of the user? or rather if he wants to avoid having "stringly-typed" effects, he can just use an empty datatype (which is internal to the module) for the tag?

@Georgi Lyubenov // googleson78 good question - sort of, because you still have that ugly newtype - it's sort of "new effect with uncovered representation"

This sort of "global" behaviour - I'm more inclined to using named effects to resolve local ambiguities honestly - I want to pass my effects of interest to actions as arguments

ah yeah, I forgot that your suggestion is to entirely do away with having to use a newtype

this sounds like a more generally useful plugin, beyond polysemy btw

There's this identifier thing though - most libraries (I guess those for anonymous records) would want "stringy" fields probably - here we want some unique identifiers.
We need to create interface that doesn't care about how they work or allows one to "plug-in with their own plugin".

Issue created: https://github.com/polysemy-research/polysemy/issues/307

@Love Waern (King of the Homeless) Thanks a lot! :slight_smile:
Alright, would it be reasonable to say that for v2, we want to fix issues that currently trouble users, possibly in breaking way if absolutely needed and for v3, we'll think about things like named effects - basically "what should polysemy become in the future"?

Sounds good.

Nice - lI'll fill in v2 roadmap with current issues in checklist and look for others that should be considered

Already added the ones I've linked to the milestone

But I'd appreciate any others

Fixing #246 means switching from the weave abstraction -- that bug is inherent to it -- and that's too much for v2. Mind if I remove it from the milestone?

I mean, we COULD remove runNonDet, but that's the nuclear option.

@Love Waern (King of the Homeless) Ok - when it comes to NonDet, we should at least mark it DEPRECATED if we can't solve this for now

runNonDet specifically is the problem, not NonDet in general. I'd be sad to mark it as DEPRECATED. Maybe a big fat warning (maybe even through theWARNING pragma) would suffice?

I would like to know how much used it actually is - if not that much, it would be nice to not "trap" more code into it

At the same time, it's the only avenue for nondeterminism. It would be a terrible loss to lose it.

Hmm - okay, let's put BIG GLARING WARNING into docs to make sure people know about it :slight_smile:

https://funprog.zulipchat.com/#narrow/stream/201385-Haskell/topic/Native.20continuations - I wonder what effects could native continuations and eff itself have on polysemy in the future :slight_smile:

One idea: if API is going to change in v2 (which it is surely going to), we could possibly try to put together some sort of migration tool using retrie - it would be cool if users could run e.g. polysemy-migrate v1-v2 and simply check made changes

I'm starting to think that there may be enough breaking changes to do and #313 is far enough to justify moving those more "ambitious" goals into v3 and doing v2 with API changes closer to now