Encode equivalent of 2nd rank polymorphism in SML

Question

runST is a Haskell function that statically limits the useful life of a resource through types. For this, a rank 2 polymorphism is used. The standard simplified type ML system offers only rank 1 polymorphism.

Can the ML standard still use types to limit the resource of a resource to similar end results?

This page and this page demonstrate some ways to restructure the code only needed for simpler types. If I understand correctly, the core is to wrap the expression so that it is replaced by its possible observations in a context that are finite. Is this technique common? Can it or the encoding associated with it be used with something like (obviously not identical in the signature) runST to prevent the type of the value coming from the wrapped expression being kept? If so, how?

The scenario that I present looks 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 not possible so that the code provided by the user can be shared in any way. Obviously, a simple interface like this with a single library function is not possible, but perhaps with different levels of wrapping and manual nesting and highlighting ...?

I saw this one , but if I understood it correctly (... most likely not), this does not actually interfere with all links to the resource being shared, it only ensures that one link to it should be "closed".

Basically, I want to implement safe typed (non-MLKit-style output) areas in SML.

Answer 1

After some turning, I think it’s possible - or at least close enough to him to work - although it’s not very nice to watch. (Perhaps I am on a completely wrong path, someone who knows, please comment.)

It is possible (I think) to use generating data types and SML functors to create abstract phantom types that cannot be referenced outside of this lexical block:

 datatype ('s, 'a) Res = ResC of 's signature BLOCK = sig type t val f:('s, t) Res -> t end signature REGION = sig type t val run:unit -> t end functor Region(B:BLOCK) :> REGION where type t = Bt = struct type t = Bt datatype phan = Phan fun run () = let val ret = (print "opening region\n"; Bf(ResC Phan)) in print "closing region\n" ; ret end end structure T = Region(struct type t = int fun f resource = ( (* this function forms the body of the "region" *) 6 ) end) ;print (Int.toString(T.run())) 

This prevents the program from simply returning a resource or declaring external mutable variables to which it can be bound, for most of the problem. But it can still be closed by functions created in the "region" block, and is thus saved beyond its supposed close point; such functions can be exported, and the link to the damaged resource is used again, which causes problems.

We can mimic the ST , although preventing the locks from doing anything useful with the resource , forcing the scope to use the monad with the phantom key:

 signature RMONAD = sig type ('s, 'a, 'r) m val ret: ( * 'r) -> 'a -> ('s, 'a, 'r) m val bnd: ('s, 'a, 'r) m * ('a * 'r -> ('s, 'b, 'r) m) -> ('s, 'b, 'r) m val get: -> ('s, 'a, 'r) m -> 'a * 'r end structure RMonad :> RMONAD = struct type ('s, 'a, 'r) m = -> * 'a * 'r fun ret (k, r) x = fn _ => (k, x, r) fun bnd (m, f) = fn k => let val (_, v, r) = mk in f (v, r) k end fun get km = let val (_, v, r) = mk in (v, r) end end signature MBLOCK = sig type t val f:(t -> ('s, t, 'r) RMonad.m) (* return *) * ('r -> ('s, string, 'r) RMonad.m) (* operations on r *) -> ('s, t, 'r) RMonad.m end signature MREGION = sig type t val run:unit -> t end functor MRegion(B:MBLOCK) :> MREGION where type t = Bt = struct type t = Bt datatype phan = Phan fun run () = let val (ret, res) = RMonad.get Phan (Bf(RMonad.ret(Phan, "RESOURCE"), (fn r => RMonad.ret(Phan, "RESOURCE") r))) in print("closing " ^ res ^ "\n") ; ret end end structure T = MRegion(struct type t = int fun f (return, toString) = let val >>= = RMonad.bnd infix >>= in return 6 >>= (fn(x, r) => toString r >>= (fn(s, r) => ( print ("received " ^ s ^ "\n"); return (x + 1) ))) end end) ;T.run() 

(this is a mess, but it shows my main idea)

The resource takes on the role of STRef ; if all the provided operations on it return a monadic value instead of direct work, it will create a chain of pending operations that can only be performed by returning to run . This means that the locks keep a copy of r outside the block, because they will never be able to execute the opportunist chain without being able to return to run and, therefore, will not be able to access it in any way.

A call to T.run will repeat the use of the same type of “key” twice, which means that this is not equivalent to a nested forall , but it should not matter if it is not possible to split r between two separate calls; which is not - if it cannot be returned, cannot be assigned externally, and any closures cannot run code that runs on it. At least I think so.