Any time you “eliminate” a tag with intention, you should actually be cancelling that elimination with an introduction.
so what we need to change is to actually make hputStrLn return an SCod, that way it stays tagged, however in that case we cannot use it in an inner scope.
yea, the actual type of scoped is:
scoped :: Monad m => (forall s. SCod s m r) -> SCod s' m r
scoped act = lift (runSCod act)
Very nice, and the same objection applies to my “Bluefin with fewer tags” idea. You could just do
withFile (pure . hPutStrLn)
to violate encapsulation. Oh well. In a way it’s encouraging that Bluefin is no more complicated than necessary.
I think strictly “no eliminators with effects”, right?
1 Like
Hmm. I want to say “yes”, but care needs to be taken. Though an effectless function can’t act upon anything, it may still observe something about your scoped quantities that threatens your invariants if the observation isn’t also scoped.
Suppose, for example, you had:
newtype ID s = ID Integer
deriving (Eq, Ord)
identify :: Handle s a -> ID s
You or your users could rely on uniqueness of IDs, giving Handle Eq, Ord, TestCoercion, etc.
Depending on implementation, however, IDs might only be unique on a per-scope basis. In which case removing the s tag from ID would be very dangerous, purity of identify notwithstanding.
1 Like
This method seems similar to, or even equivalent to, Monadic Regions by Oleg Kiselyov and Chung-chieh Shan. I believe it was a general method for emulating a region (lifetime) type system in Haskell.
1 Like
I’m not very familiar with this monadic regions approach, but it’s indeed strange that, although monadic regions were discovered quite early, they haven’t received much attention.
Additionally, I believe that using Effectful’s Provider could similarly prevent resource leaks, but Bluefin’s method might be more convenient since it allows handles to be passed around as values.
2 Likes