how can I repeat monadic instructions inside kind's monads?

user_14576283 0
Viewed 86

I know that I can run monadic instructions sequentially inside monads in Kind language, like this:

Test: _
  IO {
   IO.print(Nat.show(2))
   IO.print(Nat.show(3))
   IO.print(Nat.show(4))
  }


output:
2
3
4

But is it possible to run monadic instructions repeatedly, like this below?

Test: _
  a = [2,1,3,4,5]
  IO {
    for num in a:
      IO.print(Nat.show(num))
  }

If it is possible how can I do it correctly?

kind monads functional-programming
1 Answers

Monads are usually represented by only two operators :

  return :: a -> m(a) // that encapulapse the value inside a effectful monad
  >>= :: m a -> (a -> m b) -> m b
  // the monadic laws are omitted

Notice, the bind operator is naturally recursive, once it can compose two monads or even discard the value of one and the return can be thought of as a "base case".

m >>= (\a -> ... >>= (\b -> ~ i have a and b, compose or discard? ~) >>= fixpoint)

You just have to produce that sequence, which is pretty straightforward. For example, in Kind we represent monads as a pair which takes a type-for-type value and encapluse a polymorphic type.

type Monad <M: Type -> Type> {
  new(
    bind: <A: Type, B: Type> M<A> -> (A -> M<B>) -> M<B>
    pure: <A: Type> A -> M<A>
  )
}

In your example, we just have to trigger the effect and discard the value, a recursive definition is enough :

action (x : List<String>): IO(Unit)
  case x {
    nil : IO.end!(Unit.new) // base case but we are not worried about values here, just the effects
    cons : IO {
      IO.print(x.head) // print and discard the value
      action(x.tail) // fixpoint
    }
  }

test : IO(Unit)
  IO {
    let ls = ["2", "1", "3", "4", "5"]
    action(ls)
  }

The IO as you know it will be desugared by a sequence of binds! Normally in case of list it can be generalized like the mapM function of haskell library :

Monadic.forM(A : Type -> Type, B : Type,
  C : Type, m : Monad<A>, b : A(C), f : B -> A(C), x : List<A(B)>): A(C)
  case x {
    nil : b
    cons : 
      open m
      let k = App.Kaelin.App.mapM!!!(m, b, f, x.tail)
      let ac = m.bind!!(x.head, f)
      m.bind!!(ac, (c) k) // the >> operator
  }

It naturally discard the value and finally we can do it :

action2 (ls : List<String>): IO(Unit)
  let ls = [IO.end!(2), IO.end!(1), IO.end!(3), IO.end!(4), IO.end!(5)]
  Monadic.forM!!!(IO.monad, IO.end!(Unit.new), (b) IO.print(Nat.show(b)), ls)

So, action2 do the same thing of action, but in one line!. When you need compose the values you can represent as monadic fold :

Monadic.foldM(A : Type -> Type, B : Type,
  C : Type, m : Monad<A>, b : A(C), f : B -> C -> A(C), x : List<A(B)>): A(C)
  case x {
    nil : b
    cons : 
      open m
      let k = Monadic.foldM!!!(m, b, f, x.tail)
      m.bind!!(x.head, (b) m.bind!!(k, (c) f(b, c)))
  }

For example, suppose that you want to sum a sequence of numbers that you ask for the user in a loop, you just have to call foldM and compose with a simple function :

Monad.action3 : IO(Nat)
  let ls = [IO.get_line, IO.get_line, IO.get_line]
  Monadic.foldM!!!(IO.monad, IO.end!(0), 
      (b, c) IO {
        IO.end!(Nat.add(Nat.read(b), c))
      },
   ls)

test : IO(Unit)
  IO {
    get total = action3 
    IO.print(Nat.show(total))
  }

For now, Kind do not support typeclass so it make the things a little more verbose, but i think a new support to forM loops syntax can be thought in the future. We hope so :)

user_98204830
Related