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].

1 Like
#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.

2 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