Has anyone looked into "monadic regions" before?

Learn
1

I was researching the prior art similar to what I have been doing, dubbed “Linearly Versioned Monad.” This technique separates a monadic function into regions of different data versions using LinearTypes. Then I found these: “linear regions,” “monadic regions,” etc

References:

  • Monadic Regions
  • GitHub - basvandijk/regions: Provides the region monad for safely opening and working with scarce resources
  • Fluet, Matthew, Greg Morrisett, and Amal Ahmed. “Linear regions are all you need.” Programming Languages and Systems: 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006. Proceedings 15. Springer Berlin Heidelberg, 2006.
  • Chen, Chih-Ping, and Paul Hudak. “Rolling your own mutable ADT—a connection between linear types and monads.” Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 1997.
1 Like
2

In a sense all Haskell effect systems implement “monadic regions”. “Nested regions using explicit witness terms” describes my library Bluefin, which has value-level effect handles rather than passing effects at the type level. Kiselyov and Shan’s SubRegion is equivalent to Bluefin’s :>. I haven’t published anything with linear regions in Bluefin because I want to focus on other features for now, but I do have a branch where I explored linear types for ensuring that upstream termination of streams can be detected and handled [example].

2 Likes
3

I’m currently working on something similar but I have yet to figure out how to implement nesting ergonomically. I’m kinda stuck on that.
This is the WIP library. In contrast to using reference counting, this uses Codensity to register handlers such that resources are dropped when the scope ends.

3 Likes
4

One solution would of course be to do it like effect systems do but I have refused to accept this as it seems overkill

5

It’s pretty cool because with -XLinearTypes I think we can get close to something like rusts borrowing. scoped-codensity already feels very similar to something like the MutexGuards for rust mutexes where the lock is held until the block ends and when it drops it is freed. You could e g have a function lock var = Codensity withMVar var where the var would get a token that is equivalent to the MutexGuards live time

1 Like
6

How do you see what you’re doing as different from an effect system?

7

It can be subsumed by what you’re doing and it is much less than an effect system.

1 Like
8

“we have rust at home”, rust at home:

3 Likes
9

Yes, I played a lot with monadic regions in my toy language. After a lot of experimentation, I realized that it’s completely monadic regions (or more specifically the effect system based off it) are much more usable and ergonomic when you have boolean unification. I actually ended up rediscovering the region system that Flix uses.

1 Like
10

now on my git forge and also on hackage:

I think it might be useful for foreign ptr operations, maybe also for using async and Filehandles. In the future I am going to try to add reflection and mutable array support.

I am also looking to implement a nice abstraction for working with locks but haven’t gotten a good idea yet.

2 Likes
11

I haven’t been able to return to this thread because it prompted me to read more materials before I can confidently reply with something useful.

But I still haven’t managed to read them. :slight_smile: Instead of letting this thread cold, I’ll try my best to summarize my understanding of what has been mentioned so far.

Monadic Region

The techniquestatically guarantees that neither a file handle nor any computation involving the handle can leak outside of the region that created it. Therefore, the handle can be safely closed (and its resources disposed of)

Bluefin

Per @tomjaguarpaw, all effect systems implement “monadic region.” Bluefin is exploring linear types to prevent resource leaks. An example was attacked.

scoped-codensity

This implements a Monad just like Codensity from the kan-extensions package, but it uses a skolem trap just like the ST s monad to track resources allocated in the monad.

(See: mangoiv's webpage - codensity)

As far as I can tell, the motivation is to make the code use a lot of the “withResoruce” pattern to take advantage of the Haskell monad syntax and make it appear less tedious to write.

I have been looking for a motivational example code, the best I can find is its test case: scoped-codensity/test/Main.hs at main - mangoiv/scoped-codensity - Forgejo: Beyond coding. We Forge.

Lastly, here is a bit about my motivation for this topic.

What I have achieved in my project is to implement a “graded/indexed” monad, with the help of QualifiedDo, the code using this monad looks like just regular code in do notation.

However, under the hood, all data can be bound to a version, where the monad law guarantees that the version number can only stay the same or grow. This version number aims to track the changes in a “world” whose states evolve linearly. Anything that triggers the world to change state should be a monadic operation that advances the version number for future operations.

This makes using old data for newer state of the world a type error. I dubbed this “Linearly Versioned Monad (LVM)”, and here is the code of its bind operation of LVM:

-- ...
-- _Additional Law of Linearly Versioned Monad_
--
-- Additionally, each 'LVM' carries a proof of monotonic growth of data versions, denoted as such @m [va \<= vb]@. Then
-- we have:
--
-- 1) Law of linearly versioned monad: @ ma [va \<= vb] \>>= mb [vb <= vc] ≡ mc [va <= vc] @
(>>=) :: forall ctx va vb vc a b. ()
      => LVM ctx va vb a ⊸ (a ⊸ LVM ctx vb vc b) ⊸ LVM ctx va vc b
ma >>= f = MkLVM \ctx -> let !(aleb, ctx', a) = unLVM ma ctx
                             !(blec, ctx'', a') = unLVM (f a) ctx'
                         in  (Dict \\ leTrans @va @vb @vc \\ aleb \\ blec, ctx'', a')

Note that the bind operation requires the monadic operation to provide a proof of vb >= vc so that it can maintain the va >= vc for the monadic output.

This is an example operation that grows the version (not the v + 1 in the type signature), it updates a storage location in this “world”:

sput :: forall v r a. (YulO2 r a, ABIWordValue a)
     => P'V v r ADDR ⊸ P'V v r a ⊸ YulMonad v (v + 1) r (P'V (v + 1) r a)

In risk of too much of details unexplained, full code can be found here (LVM), here (LVM’s Combinators), and here (some real monadic operations).

To wrap up, my motivation is to find prior art for the approach I have taken so far, and the monadic region was the first clue I have found.