Discussion: Chaining operators requires excessive `Eval` or `@@`

[Skyfold]

I've been thinking about how to make using Fcf functions more like their value level counterparts. In particular its been bothering me that you cannot chain the functions in Fcf.Control.Monad without interleaving Eval.

Monad Changes

When you try to write Left "err" >> Right 5 >> Right 6 at the type level, you get a type error:

> :m Fcf.Control.Monad Fcf
> :k! 'Left "err" >> 'Right 5 >> 'Right 6

<interactive>:1:1: error:
    • Expecting one more argument to ‘'Left "err" >> 'Right 5’
      Expected kind ‘Either a0 a1’,
        but ‘'Left "err" >> 'Right 5’ has kind ‘Either
                                                  GHC.Types.Symbol GHC.Num.Natural.Natural
                                                -> *’
    • In the first argument of ‘(>>)’, namely ‘'Left "err" >> 'Right 5’
      In the type ‘'Left "err" >> 'Right 5 >> 'Right 6’
> :k! Eval ('Left "err" >> 'Right 5) >> 'Right 6
Eval ('Left "err" >> 'Right 5) >> 'Right 6 :: Either
                                                GHC.Types.Symbol GHC.Num.Natural.Natural
                                              -> *
= 'Left "err" >> 'Right 6

You end up with a similar issue with >>=:

> :m Fcf.Control.Monad Fcf
> :k! 'Left "err" >>= (Return <=< (+) 1) >>= (Return <=< (-) 1)

<interactive>:1:1: error:
    • Couldn't match kind ‘*’ with ‘GHC.Num.Natural.Natural’
      Expected kind ‘Either GHC.Types.Symbol GHC.TypeNats.Nat
                     -> GHC.TypeNats.Nat’,
        but ‘'Left "err" >>= (Return <=< (+) 1)’ has kind ‘Either
                                                             GHC.Types.Symbol GHC.TypeNats.Nat
                                                           -> *’
    • In the first argument of ‘(>>=)’, namely
        ‘'Left "err" >>= (Return <=< (+) 1)’
      In the type ‘'Left "err" >>= (Return <=< (+) 1)
                   >>= (Return <=< (-) 1)’
> :k! Eval ('Left "err" >>= (Return <=< (+) 1)) >>= (Return <=< (-) 1)
Eval ('Left "err" >>= (Return <=< (+) 1)) >>= (Return <=< (-) 1) :: Either
                                                                      GHC.Types.Symbol
                                                                      GHC.Num.Natural.Natural
                                                                    -> *
= 'Left "err" >>= (Return <=< (-) 1)

If we were to change the kind signature to wrap their first argument in Exp then we could chain functions without Eval (or resorting to using Fcf.Combinators.(=<<) which would be even harder to read).

In other words I would be making these changes (Old on top, new on bottom):

(>>=) :: m a -> (a -> Exp (ma)) -> Exp (m b) (>>=) :: Exp (m a) -> (a -> Exp (ma)) -> Exp (m b)

(>>) :: m a -> m b -> Exp (m b) (>>) :: Exp (m a) -> m b -> Exp (m b)

The disadvantage is you now need to use Fcf.Pure for the first argument of the chain (assuming it wasn't an Exp).

In essence we have to choose:

1. make it easy to work with functions that return Exp and require extra lifting into Exp for normal values (like lists, numbers or symbol)
2. keep it the way it is and use Eval or Fcf.Combinators to discharge the Exp after each type level function call.

What are you thoughts?

[gspia]

We could ask Lysxia if it would be ok to publish Fcf.Combinators.(>>=). Would this help?

The following methods are defined there (export list doesn't contain (>>=) yet):

data (=<<) :: (a -> Exp b) -> Exp a -> Exp b
type instance Eval (k =<< e) = Eval (k (Eval e))

data (>>=) :: Exp a -> (a -> Exp b) -> Exp b
type instance Eval (e >>= k) = Eval (k (Eval e))

data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c
type instance Eval ((f <=< g) x) = Eval (f (Eval (g x)))

(I'll open an issue there about publishing that function.)

Other thoughts: I think that "dev ergonomics" (or "api for dev'ing") is important. In this case, I'm thinking if it would be possible to support both ways. It could be pointed out to users with couple of examples, which use cases benefit using the former or latter style.

I really haven't used these much yet so it is quite difficult for me to judge the pros and cons, if it is sensible to just pick one approach. Do you see any difficulties, if first-class-families provided (>>=) and here the examples would exemplify the differencies between Fcf.Combinators.(>>=) and Fcf.Control.Monad.(>>=)?

Here we could even make sure that each of those operators would have both Exp and without Exp versions available, where it makes sense to have them available ((>>=), (=<<), ... what else)???

So, maybe the main questions here is: does it make sense to have both versions available?

[gspia]

Here is the link for the issue at Lysxia lib: https://github.com/Lysxia/first-class-families/issues/51

[Skyfold]

To be honest, I find adding Fcf.Combinators.(>>=) to be more confusing because you now have two (>>=) with different implementation (need qualified imports to distinguish), but are from the same class (Monad).

After thinking about this for awhile it dawned on me I'm going about this in completely the wrong direction. I should not be trying to lift arguments into Exp I should be implementing Fcf.Combinators in Fcf.Control.Monad.

I'm still working on writing an arrow instance for Monad

[Skyfold]

I really like the idea of writing a Monad instance for Exp in Fcf.Control.Monad, but for some reason GHC isn't using my instance (or maybe I'm missing something else).

I added this to Fcf.Control.Monad and it compiles happily:

type ExpHelper :: (a -> Type) -> (a -> b -> Type) -> b -> Type
type ExpHelper e k = (k (Eval e)) -- k (f r) r

type instance Eval (f >>= k) = Eval (ExpHelper f k)
-- Also can define the instance like so
-- type instance Eval (e >>= k) = Eval (k (Eval e))

However, when I go to use it, I run into issues:

> :m Fcf Fcf.Control.Monad
> :k! Eval (ExpHelper (Pure 1) ((+) 1))
Eval (ExpHelper (Pure 1) ((+) 1)) :: GHC.Num.Natural.Natural
= 2
> :k! (Pure 1) >>= ((+) 1)

<interactive>:1:2: error:
    • Couldn't match kind ‘*’ with ‘GHC.Num.Natural.Natural’
      Expected kind ‘GHC.Num.Natural.Natural -> GHC.TypeNats.Nat’,
        but ‘Pure 1’ has kind ‘GHC.Num.Natural.Natural -> *’
    • In the first argument of ‘(>>=)’, namely ‘(Pure 1)’
      In the type ‘(Pure 1) >>= ((+) 1)’

<interactive>:1:15: error:
    • Couldn't match kind ‘GHC.Num.Natural.Natural’
                     with ‘GHC.Num.Natural.Natural -> b0’
      Expected kind ‘GHC.TypeNats.Nat
                     -> Exp (GHC.Num.Natural.Natural -> b0)’,
        but ‘(+) 1’ has kind ‘GHC.TypeNats.Nat -> GHC.TypeNats.Nat -> *’
    • In the second argument of ‘(>>=)’, namely ‘((+) 1)’
      In the type ‘(Pure 1) >>= ((+) 1)’
>

What I'm confused with is why Eval (ExpHelper (Pure 1) ((+) 1)) works, while (Pure 1) >>= ((+) 1) does not. The definition of f >>= k is Eval (ExpHelper f k),

If you can spot my mistake, let me know.

[gspia]

I'm taking a quick look first (so not finding good explanations right away).

while (Pure 1) >>= ((+) 1) does not

What would be the monad here? (not sure if this is the problem). On term level, we would see that the m is left open (and I suspect that it is not ok - the partiality is really problematic often):

> :t (pure 1) >>= ((+) 1)
(pure 1) >>= ((+) 1) :: (Monad m, Num (m b)) => m b

Note also the difference between Pure and Return. (not sure if it has any relevance here - but I would need to think over where to put only a and where m a)

Pure :: a -> a -> *
Return :: a -> m a -> *

---

What definition did you use for the >>=? Was it

(>>=) :: Exp (m a) -> (a -> Exp (m a)) -> Exp (m b)

(I'm having hard time getting the ExpHelper to compile with that definition.)

With

(>>=) :: Exp a -> (a -> Exp (m a)) -> Exp (m b)

the

ExpHelper :: (a -> *) -> (a -> b -> *) -> b -> *

compiles.

---

Further thoughts, not sure why

> :t (pure 1) >>= ((+) 1)
(pure 1) >>= ((+) 1) :: (Monad m, Num (m b)) => m b

That (+) 1 is pure function so it looks like that on term level, it is automatically turned into a Int -> m Int function. Looking at the error messages, it looks like that this is not happening on type level automatically. (I tried with version of ExpHelper with m b and not just b. I tried too many things and rn confused here... )

[Skyfold]

What definition did you use for the >>=? Was it

Sorry, I should have included this in my post. I left the definition of >>= the same:

data (>>=) :: m a -> (a -> Exp (m b)) -> Exp (m b)

What would be the monad here? (not sure if this is the problem). On term level, we would see that the m is left open (and I suspect that it is not ok - the partiality is really problematic often):

Lets look at type Exp a = a -> Type, since we want to write a monad instance for Exp. There are several important parts of this definition: The arrow is (->) :: * -> * -> *, it takes two Type and returns a Type, so the a is a Type (Not Kind). The Type is a type (since Type :: *), but cannot be set. This means Exp :: * -> * even though (->) :: * -> * -> *. Its a bit like the Type fills the second argument with a black box.

So, at first I want to say the monad is the arrow monad (->) a :: * -> * similar to its arrow monad instance from Control.Monad:

instance Monad ((->) r) where
    f >>= k = \ r -> k (f r) r

Much like the Either Monad instance in Control.Monad, the arrow monad instance is operating on the second Type argument to (->).

However, Exp fills the second Type argument of arrow with Type and leave the first open. Its a bit like writing a monad instance for r (->). Exp :: * -> * is also the right kind for >>= since * -> * satisfies the m in m a -> (a -> Exp (m b)) -> Exp (m b).

At the same time we cannot write:

type instance Eval ((f :: Exp) >>= k) = Eval (k (Eval f))

since we will get:

    • Expecting one more argument to ‘Exp’

However, we can write

type instance Eval ((>>=) @((->) Type) e k) = Eval (k (Eval e))

And if we do >>= does work Only for Exp Type (>> is defined in terms of >>=)

> :k! Eval (Pure Int >> Pure Char)
Eval (Pure Int >> Pure Char) :: * -> *
= Pure Char

I have yet to figure out how to get GHC to realize the type instance works for any kind, not just Type.

For some reason this does not work:

type instance Eval ((->) a >>= k) = Eval (k a)

Full Code

data (>>=) :: m a -> (a -> Exp (m b)) -> Exp (m b)
type instance Eval ((>>=) @((->) Type) e k) = Eval (k (Eval e))
data (>>) :: m a -> m b -> Exp (m b)
type instance Eval (m >> k) = Eval (m >>= ConstFn k)

Notes

If -> was itself defined with a value (an thus an equivalent kind), we could easy write an instance.

To explain: -> is defined as type (->) = FUN 'Many and data FUN m a b. The important part is that FUN has no values and as such we cannot create a kind of arrow to match a type instance on.

To show you what I mean you can write:

data (>>=) :: m a -> (a -> Exp (m b)) -> Exp (m b)
newtype W a = W (Exp a)
type instance Eval ('W e >>= k) = Eval (k (Eval e))

And this will work:

> :k! Eval ('W (Pure 1) >> 'W (Pure 2))
Eval ('W (Pure 1) >> 'W (Pure 2)) :: W GHC.Num.Natural.Natural
= 'W (Pure 2)

Since we can match on 'W.

However, we cannot change Exp to be a newtype since it must be of type * so a data type deceleration can use it as the result. In other words, the only way to write the type instance we want for Exp is to convince GHC that it works for Exp a where a is any kind.

[Lysxia]

I think a discipline where arguments of combinators are wrapped in Exp to allow type-level code to look more like value-level code is a direction worth exploring. If you want to reuse the >>= name, you probably also want to reuse Pure. The current Pure can be renamed Uneval.

(>>=) :: Exp (m a) -> (a -> Exp (m b)) -> Exp (m b)
Pure :: a -> Exp (m a)

Uneval :: a -> Exp a

It's not clear to me whether the argument of Pure should be wrapped in Exp, but in any case it should probably match the type of >>= so that the monad laws typecheck: Eval (m >>= Pure) = Eval m.

So, at first I want to say the monad is the arrow monad (->) a :: -> similar to its arrow monad instance from Control.Monad

This is not possible because the arrow monad uses a lambda in its definition and there are no lambdas at the type-level. Another way to understand this is that the kind (->) is quite different from the type (->). Whereas the type of (->) is intuitively the type of functions, the kind (->) is the kind of matchable functions, with a "matchable" application f x ~ g y iff f ~ g and x ~ y, which isn't a property that makes much sense semantically. Because of that, the kind (->) is not a monad. What you want is a kind of "non-matchable" functions, which doesn't exist yet. If it did, it would probably subsume most use cases for fcf. What fcf does is allow you to emulate a kind of non-matchable functions as a -> Exp b, modulo an extensional equality: f equals g if Eval (f x) equals Eval (g x) for all x. This lets you define the arrow monad, aka. the reader monad, in the following way:

newtype Reader a b = Reader (a -> Exp b)

Using that encoding of (->) a, you can defunctionalize the lambda in the monad instance for (->) a, and wrap its symbol in Reader.

My using the =<< name only for the Exp combinator (instead of an overloaded operator) causes an unfortunate name collision. A possible solution is to just require people to import Fcf.Combinators qualified if they want to also use Fcf.Control.Monad.

[Skyfold]

This is not possible because the arrow monad uses a lambda in its definition and there are no lambdas at the type-level. the kind (->) is not a monad.

Well, that would explain why I was having so much trouble trying to write the type instance.

My using the =<< name only for the Exp combinator (instead of an overloaded operator) causes an unfortunate name collision. A possible solution is to just require people to import Fcf.Combinators qualified if they want to also use Fcf.Control.Monad.

The name collision isn't an issue unless its exported in Fcf. Its easy to just import Fcf.Combinators qualified, harder to import Fcf half qualified. I think the names in Fcf.Combinators are correct as they are since Exp is a monad.

If you want to reuse the >>= name, you probably also want to reuse Pure. The current Pure can be renamed Uneval.

I would keep it Pure, but don't export it from Fcf. (Let me know what you think)

Changes to Fcf.Control.Monad

I'd like to not only update Monad, but also Functor, Applicative and Traversable. Exactly which functions and to what degree will need a bit of playing around. I'll create a PR where we can discuss the details of each.

[gspia]

Ok, thanks to both of you for the interesting info and discussions: some of this is quite difficult to me atm. @Lysxia are you referring to things discussed or introduced in the "unsaturated type families" paper(s) with the following:

is the kind of matchable functions, with a "matchable" application f x ~ g y iff f ~ g and x ~ y, which isn't a property that makes much sense semantically. Because of that, the kind (->) is not a monad. What you want is a kind of "non-matchable" functions,

(It looks like that at the gch the unsaturated tf dev has slowed down for some time.)

I have some random vague thoughts about wrapping the arguments to Exp or not (these comments are based more on a feeling now than any analysis or clear thoughts). I've been thinking that it would be nice if the $ and . would have closer corresponding operators at Fcf available that "look and feel the same when using those": if not the same symbols, maybe some variants that are closer to those.

> (head . head) [[1],[2],[3]]

can be written as

> :kind! Eval ( (FromMaybe 0 <=< Head <=< FromMaybe '[0] <=< Head) '[ '[1], '[2], '[3]])

where <=< corresponds to term level .. Here, it might be easier to read, if we had, say

> :kind! Eval ( (FromMaybe 0 .: Head .: FromMaybe '[0] .: Head) '[ '[1], '[2], '[3]])

or something similar. (Would .. work?)

This gives the other vague questions/thoughts: what should be easy and convenient from the using point of view and what should be made for making building the fcf libs easier? (I feel that these are not fully separate goals, but still, may have a bit different viewpoint: I mean the things that are needed for organizing Evals and Exps and such things vs things that you are trying to achieve with using those Evals and Exps).

---

Changes to Fcf.Control.Monad

I'd like to not only update Monad, but also Functor, Applicative and Traversable. Exactly which functions and to what degree will need a bit of playing around. I'll create a PR where we can discuss the details of each.

Ok, some of those might be at defined in the first-class-families package (Functor and some of its instances): are you referring to those also?

On fcf-containers, I was planning to collect breaking changes to v0.9.0 and keep v0.8.x versions such that they are mostly backwards compatible. On text modules at the moment, there is the current module Text, OldText that equals the Text, and the forthcoming NewText. I'll replace the Text with the NewText contents on v0.9.0. (And then remove the OldText later one day.) Not sure if this is good approach (or, is there better ways) to handling the breaking changes: at least it gives some changes to people keep using the old versions with quite small maintenance need, in case that is something they want to do.

[Skyfold]

Ok, some of those might be at defined in the first-class-families package (Functor and some of its instances): are you referring to those also?

I think Fcf.Control.Monad should eventually end up in first-class-families. In my mind, first-class-families is base for dependent types. I would like to end up with Fcf.Control.Monad, Fcf.Control.Applicative and Fcf.Data.Traversable in first-class-families where each corresponds to their value level base equivalent.

Should I prototype this in a PR to fcf-containers or go ahead and write a PR to first-class-families?

Either way these will be breaking changes since many of the types will change (I likely won't change Functor since it already can write the Functor laws without Eval). Both Monad and Applicative will change to make chaining operations seamless.

On fcf-containers, I was planning to collect breaking changes to v0.9.0 and keep v0.8.x versions such that they are mostly backwards compatible. On text modules at the moment, there is the current module Text, OldText that equals the Text, and the forthcoming NewText. I'll replace the Text with the NewText contents on v0.9.0. (And then remove the OldText later one day.) Not sure if this is good approach (or, is there better ways) to handling the breaking changes: at least it gives some changes to people keep using the old versions with quite small maintenance need, in case that is something they want to do.

I think you are on the right track to handling breaking changes. Whatever we end up doing with Fcf.Control.Monad it will be a part of the v0.9.0 release.

[Lysxia]

are you referring to things discussed or introduced in the "unsaturated type families" paper(s)

Yes that was my thought.

first-class-families is base for dependent types

That sounds good to me. Feel free to open a PR.

• For naming modules, I already started with Data vs Class instead of Data vs Control, because the distinction seems clearer and more useful to me, but I don't feel strongly about it, so you can decide to change it back.
• If Fcf is to be the equivalent of Prelude, we may have to revisit the naming of the Exp-specific combinators like (=<<). I'm not a fan of prelude though, I prefer each thing to have a dedicated home module.
• It would be nice to have a consistent recipe for "wrapping" types in Exp. There are a few different types you might give the overloaded (>>=) for instance. There is probably no one best choice, but there may be a systematic way of predicting when to insert Eval/Uneval, and knowing what kind of expressions can be lifted to the type-level verbatim.

-- Candidate signatures for (>>=)
m a -> (a -> Exp (m b)) -> Exp (m b)
Exp (m a) -> (a -> Exp (m b)) -> Exp (m b)
Exp (m a) -> (Exp a -> Exp (m b)) -> Exp (m b)
Exp (m a) -> Exp (a -> Exp (m b)) -> Exp (m b)

[gspia]

Yes, I agree that these packages should be re-organized: if thinking that fcf-containers should somehow correspond to containers-package, then fcf-container probably should not contain that Fcf.Control.Monad, and in the same way, also the existing "Char" module would have better fit at the "first-class-families" package. (There might was some other modules or functions that would be better at "first-class-families" package. I'm thinking the Symbol and Tuple modules and their contents.)

Further, where to put the Text module. In a way, it probably would belong to "base". But then, would it mean first-class-families or would actually a new package e.g. fcf-text be better? If you think that new package would be good, I'd be ok to making one. (I'm not sure if there would be real need for a new package. Looks like a new package would solve the deprecation problem quite nicely here in the case of Text.)

[Skyfold]

We don't have to follow the value level Haskell library hierarchy/separation. Your Fcf.Data.NewText is more than the basic string functions in base, but not yet parsec at the type level. I think the better question is what you want NewText to become. If it will continue to become more like parsec, it should be in its own package.

[gspia]

Yes, exactly, the "Text" modules (old & new) here are not following string functions on base, but rather the text-package (https://hackage.haskell.org/package/text) and "Text" datatype has been the source of inspiration.