stefan-hoeck / idris2-freer

Efficient, stack-safe implementation of freer monads.
BSD 3-Clause "New" or "Revised" License
4 stars 0 forks source link

Small example of usage #7

Open isberg opened 6 months ago

isberg commented 6 months ago

It would be great if there could be just a small example of usage, how do create a script and then run it. It would also be great with some guidance how on how the usages of the freer monad differs from other variations of a free monad.

isberg commented 5 months ago

@stefan-hoeck I would be most grateful for an example of how to use FoldMap or runM, I am not clear about which would be simpler. I have managed to use run : Free I a -> a. With foldMap the closest I have come is a Mismatch between: Counter argTy and Free Counter Nat. where argTy seems to be Control.Monad.Free.argTy but that makes me no wiser.

stefan-hoeck commented 5 months ago

I'm sorry for not answering earlier. I'm afraid, I don't use this library myself anymore: I wrote it while experimenting with effect systems in Idris, but I'm not into these kinds of things anymore, because in Idris, we can do most stuff over a simple core monad such as IO together with implicits and proof search.

I'll try and come up with an example, but it would be helpful if you could try and minimize the example you currently have and post it here.

isberg commented 5 months ago

My idea is that I want code of structure similar to this (with freer as the only direct dependency):

import Control.Monad.Free

data BazConstructor : Type -> Type where
  Foo : (String -> next) -> BazConstructor next
  Bar : String -> (Integer -> next) -> BazConstructor next
  Baz : Integer -> (Bool -> next) -> BazConstructor next

FBazConstructor : Type -> Type
FBazConstructor = Free BazConstructor

foo : FBazConstructor String
foo = lift $ Foo id

bar : String -> FBazConstructor Integer
bar x = lift $ Bar x id

baz : Integer -> FBazConstructor Bool
baz x = lift $ Baz x id

script : FBazConstructor Bool
script = do
  x <- foo 
  x <- bar x
  x <- baz x
  pure x

The different instructions could in a real world scenario be things like sending email och communicate with external systems and I expect that the script might also be dynamically generated or have optional parts.

My goal is to be able to run the script both with a test runner and a production runner as well as compare the structure of the script with an expected format, but I suspect that as soon as I learn to interpret it in some sensible way I could manage all of them.

I am totally unclear if I am expected to implement MonadRec for my own type, or if I should map it to some other monad that have a MonadRec implementation, or something else. Any hint would be greatly appreciated.