runST
is a Haskell function that statically constrains the usable lifetime of a resource through types. To do this it uses rank-2 polymorphism. Standard ML's simpler type system only offers rank-1 polymorphism.
Can Standard ML still use types to constrain the lifetime of a resource to similar end results?
This page and this page demonstrate some ways to restructure code to only need simpler types. If I understand correctly the core is to wrap the expression up so that it's replaced by its possible observations in context, which are finite. Is this technique general? Can it, or a related encoding, be used with something like (obviously not identical in signature to) runST
, to prevent the type of a value escaping from a wrapped expression being observed? If so, how?
The scenario I'm imagining is something like this:
magicRunSTLikeThing (fn resource =>
(* do things with resource *)
(* return a value that most definitely doesn't contain resource *)
)
...where magic...
provides a resource that is impossible for the user-supplied code to share in any way. Obviously a simple interface like this with a single library function isn't possible, but perhaps with various layers of wrapping and hand-inlining and extracting...?
I've seen this, but if I understood it correctly (...most likely not), that doesn't actually prevent all references to the resource from being shared, only ensures that one reference to it must be "closed".
Basically I want to implement safely typed explicit (not inferred MLKit-style) regions in SML.
After some headbanging, I think this is possible - or at least close enough to it to work - although it isn't very pretty to look at. (I may be on completely the wrong track here, someone knowledgeable please comment.)
It's possible (I think) to use SML's generative datatypes and functors to create abstract phantom types that cannot be referred to outside a given lexical block:
This prevents the program from simply returning
resource
or declaring external mutable variables it could be assigned to, which deals with most of the issue. But it can still be closed over by functions created within the "region" block, and retained that way past its supposed close point; such functions could be exported and the dangling resource reference used again, causing problems.We can imitate
ST
though, and prevent closures from being able to do anything useful withresource
by forcing the region to use a monad keyed with the phantom type:(this is a mess, but it shows my basic idea)
The resource takes the role of
STRef
; if all of the provided operations on it return a monadic value instead of working directly, it will build up a chain of delayed operations that can only be executed by being returned torun
. This counters the ability of closures to retain a copy ofr
outside the block because they will never actually be able to execute the op chain, being unable to return torun
, and are therefore unable to access it in any way.Invoking
T.run
twice will re-use the same "key" type, meaning this isn't equivalent to a nestedforall
, but that shouldn't make a difference if there's no way to sharer
between two separate invocations; which there isn't - if it can't be returned, can't be assigned outside, and any closures can't run the code that works on it. At least, I think so.