Summary

It would be great if the compiler supported the explicit selection of functions in Qualified do and ado notation with phantom types, which is the only syntactic sugar we have in PureScript. Indexed Monads don't quite satisfy the need here.

Motivation

Phantom types can be useful for helping us control the usage of certain functions. Consider if we have the data type of
Stream len a. We might be interested in talking about infinite streams vs finite streams, and therefore in concatenating two objects of type Stream Finite a and Stream Infinite a, with a concat operation. Some operations would if we had a Finite Stream, but not an Infinite Stream -- for example finite <> infinite would be acceptable, but infinite <> finite would not, because if the Infinite stream is first, the finite stream will never be reached.

Under the current state of the compiler, we will need to write separate concatX functions to handle the four combinations: Finite-Finite, Finite-Infinite, etc. And this is acceptable if we are just using normal functions. However, this becomes a blocker when our goal is to use the Qualified ado and do syntactic sugar, because the sugar can only handle one bind or apply function at a time, making it impossible to use the four separate functions together within the do or ado. In the following example:

Stream.do
  a <- finite
  b <- finite'
  c <- infinite
 pure $ [a, b]  --Rejected

There isn't a way to use the sugar and have the result be correctly typed, because only one bind function can be used, and we don't have function name overloading. This is problematic for Infinite and Finite streams, because some operations like takeLast would be valid for a Finite stream, but invalid for an Infinite stream. This means that phantom types are no longer useful when it comes to the ado and do syntax -- at least, for these kind of use cases. Even if we did coerce types here, we'd just lose the phantom type-safety for the result.

Indexed Monads are useful, but they don't correctly describe what's happening here, either. Indexed Monads allow us to constrain particular actions, but we aren't attempting new actions here. If we used an indexed monad, we might end up with a Stream Finite Infinite a as a consequence of producing an Infinite stream from an initial Finite stream. But now this new Stream can only be bound to a Stream i Finite, which is not the constraint we want. How it was produced has nothing to do with where we might want to use it.

Detailed description of the proposal.

The only wish here is to enable Qualified do and ado syntax to be more powerful. There's no need for anything like function overloads or type-level programming of phantom types so that we can choose the final type based on the input types, within a single function.

The simplest, least-verbose way I can think of for this is to have the module be able to export lists of functions that it wants to use to override what is used for the Qualified-do-ado syntax. So perhaps this:

module Streams 
( indexl
, foldl

, do bind (bindFF, bindFI, bindIF, bindII)      -- exports of candidates for bind

, do pure (pureFF, pureFI, pure)                 -- exports for pure

, ado apply (applyFF)                 -- exports for apply

...                         -- exports for discard, or whatever else. If they're not included, then 
                            --  the default Qualified-do
                           --    strategy would be used.
)
where 

Under the assumption that using reserved keywords would make this easiest to implement, we could start the exports with the
names of the syntactic sugar they hope to replace.

If necessary, the order of export could be significant, and represent the order in which these functions are considered. Functions with identical type signatures would not be allowed.

It's possible that the exported functions for bind won't cover all use cases. Given phantom types, a Stream Unknown a might be created. If it's used in the bind, it would be sufficient to issue an error that Unknown isn't allowed by the parent module. And if some function isn't exported, then the normal strategy for Qualified-do would apply for that function.

It's also desirable that within the module itself, any do notation would work according to the exported rules when generating a value of the Stream type, just as a defined bind function normally would (iirc).

Now, I know that for the Bind typeclass, there's the desire for each instance to satisfy associativity, to enable do to be unambiguous. I'm not totally sure whether that would sink this proposal or not, or whether Qualified-do is supposed to obey those unambiguous rules or not. I can see where there might be issues. If the exported functions are strange, then this syntax would be ambiguous:

-- We might have nonsense rules that cause ambiguity:

-- Finite + Finite = Infinite
-- Infinite + Infinite = Finite
-- Infinite + Finite = Infinite
-- Finite + Infinite = Finite

Stream.do
  a <- finite  :: Stream Finite Int
  b <- finite'  :: Stream Finite Int
  c <- infinite a b :: Stream Infinite Int
 pure $ [a, b]  :: ?

Is the result a Stream Finite Int, or a Stream Infinite Int? I suppose it depends on how it desugars. But since c is generated using a and b, we know it has to desugar to finite >>= (\a -> finite' >>= (\b -> infinite a b)), so the type is Finite + Finite = Infinite, given how the combinations occur. But I can see how, if we were using infinite b instead, we would get a possible finite >>= (\a -> finite') >>= (\b -> infinite b), and assuming bind is left-associative, we would get a Finite + Infinite = Finite, whereas if we desugared it the same as the first example, we would still get Infinite. I don't know if the compiler does this kind of thing or not for Qualified-do, but it would be jarring to have the entire type change just because an argument wasn't used, so the compiler re-wrote the function differently.

We could address this by having the exporter publish the strategy they want to use -- to me, at least, it seems consistent with the syntax to always expand the do syntax the same way, as in finite >>= (\a -> finite' >>= (\b -> infinite a b)), so that types unify from the bottom-up in all cases.

I'm out of my depth here. But I still think that the proposal would make phantom types vastly more useful, by linking them with the sugar without needing Indexed Monads. It would make Qualified-do (and ado) itself more useful. And in most cases, it should fall to the Module writer to export a Qualified-do that actually makes sense under the defined desugaring strategy.

Examples

module Streams 
(module Example

, do strategy bottom-up            -- Always expand the `do` while keeping all bindings in scope for the last line.

, do bind (bindFF, bindFI, bindIF, bindII)      -- exports of candidates for bind

, do pure (pureFF, pureFI, pure)          -- exports for pure

, ado apply (applyFF)                -- exports for apply
)
where 

data Stream len a
data Finite
data Infinite

-- Unqualified `do` for a Stream should work within the module according to the exported rules.
do
  a <- finite :: Stream Finite Int
  b <- finite' :: Stream Finite Int
  c <- infinite :: Stream Infinite Int
 pure $ [a, b, c] :: Stream Infinite Int