Language suggestion

[LucDuponcheelAtGitHub]

Hello,

Below is a language suggestion.
Just wanted to know if it makes sense at all.
I guess the answer is no
(otherwise much more clever guys than me would have introduced it already).

Here is the context of the suggestion.

Reading and writing are a bit like ying and yang
(technically, they are adjoint functors).

Traditionally

• an extra argument is used for reading, leading to functions of type R => (Z => Y),
• an extra result is used for writing, leading to functions of type Z => (Y && W), where type && = [Z, Y] =>> (Z, Y).

Context functions of type R ?=> (Z => Y) make (among others) reading more convenient.
I am a big fan of them.

Below is an example
(agreed, one that, on its own, does not really simplify things).

def withReading: Boolean ?=> Int => Int = i => i + 1

@main def mainReading(args: String*): Unit =
  given Boolean = true
  println(withReading(1))

Reading and writing can be combined.

Below is an example.

Note that it uses summon[Boolean] to write what has been read.

type && = [Z, Y] =>> (Z, Y)

def withReadingAndWriting: Boolean ?=> Int => (Int && Boolean) = i => (i + 1, summon[Boolean])

@main def mainReadingAndWriting(args: String*): Unit =
  given Boolean = true
  println(withReadingAndWriting(1))

Now here is the suggestion.

Could it make sense to introduce, at language level, a type &&?
so that functions of type Z => (Y &&? W) make (among others) writing more convenient.

For example, the code above could then be simplified to

def withReadingAndWriting: Boolean ?=> Int => (Int &&? Boolean) = i => i + 1

@main def mainReadingAndWriting(args: String*): Unit =
  given Boolean = true
  println(withReadingAndWriting(1))

[julienrf]

Hello @PSBP-Library, do you have an example where the written value is not exactly the read value?

[LucDuponcheelAtGitHub]

Two examples:

1. state monad

S ?=> Z => (Y &&? S) could then be used for dealing with state, which, of course, can change

2. writing monad

when implementing binding two values being written, say w1 and w2, are combined using append
(what you write is a monoid, remember).

the (somewhat complex) code (when taken out of its context) below is part of my library
I implement lifting as a context functor (cfr context functions, hence the ?)

some complexity could then conveniently be left away

  override private[plp] val `0c?=>1c ?~~> 1c?=>1c`: BinaryFromUnaries[Zero[C], One[C]] ?~~> BinaryFromUnaries[One[C], One[C]] = 
    new {
      private[plp] def apply[Z, Y]: (Z ?=> C[Y]) ?=> (C[Z] ?=> C[Y]) =
        liftD[W && Z, W && Y]{
          (w1, z) =>
            liftD[W && Y, W && Y]{ (w2, y) =>
              resultD(append(w1, w2), y)
            }{ given Z = z ; summon[Z ?=> C[Y]]}
        }(summon[D[(W && Z)]])  
    } 

[LucDuponcheelAtGitHub]

the context functor is a somewhat special one between
categories
[Z, Y] =>> Z ?=> C[Y]
and
[Z, Y] =>> C[Z] ?=> C[Y]

The categories have the same objects
The functor does not change the objects

(https://en.wikipedia.org/wiki/Functor)

[julienrf]

1. state monad

S ?=> Z => (Y &&? S) could then be used for dealing with state, which, of course, can change

How would you translate the following example of state monad usage into a context state?

def withReadingAndWriting(n: Int): State[Boolean, Int] =
  for
    bool <- State.get[Boolean]
    _    <- State.set(!bool)
  yield n + 1

The best I could get is something like the following:

val withReadingAndWriting: Boolean ?=> Int => (Int &&? Boolean) = i =>
  val bool = summon[Boolean]
  given setBool: Boolean = !bool
  i + 1

But I don’t think this is simplifying things. I would say that nesting givens increases the chances to mess up (e.g., if you change given setBool: Boolean = !bool to val setBool: Boolean = !bool then your program doesn’t return what you want it to return.

[LucDuponcheelAtGitHub]

Sorry for the late reply.

If the language extension would come with some more built-in syntax then the code could look like

val withReadingAndWriting: Boolean ?=> Int => (Int &&? Boolean) = i =>
  set(summon[Boolean] + 1)
  i + 1

set is used for writing just like summon is used for reading

agreed, maybe set should be replaced by a less common word
just like summon is used instead of get