Eliminate Type-Level Distinction of Static and Dynamic

[andrewthad]

I think this may be able to be handled at the value level instead. Roughly, here's the idea. We have three kinds of tokens:

• Static: read, ignore
• Dynamic: deallocate
• Neutral: allocate, modify

There's some kind of lattice thing going on (or maybe it's a partial order) where neutral can be merged with either of the other token types, assuming their type. The dynamically and statically would scoped the computation introducing the appropriate token type.

The reason this is appealing to me is that library authors will already have to explicitly deal with tokens somewhat often. However, it turns out there are a number of definable functions that work in a static or dynamic context. I'll need to think about the soundness of this more.

[andrewthad]

Let's give this a try:

data Mode = Static | Dynamic
data Token :: Type
data Action :: Mode -> Type

action :: Token ->. Action m ->. Action m

-- Dynamic actions
allocate :: Object a =>. Action Dynamic ->. (Action Dynamic, Reference a)
deallocate :: Object a => Reference a ->. Action Dynamic ->. (Action Dynamic, Reference a)

-- Static Actions
read :: Object a => Reference a ->. Action Static ->. (Action Static, a)
ignore :: Reference a ->. Action Static ->. Action Static

-- Scoping Computations
statically_ :: Object a => Reference a ->. (a ->. Action Static ->. Action Static) -> Reference a
dynamically_ :: Object a => Reference a ->. (a ->. Action Dynamic ->. Action Dynamic) -> Reference a

Under this scheme, we can actually nest a static/dynamic computation directly under a computation of the same type. I don't think this introduces unsoundness.

What's cool about this is that I think we can still write functions like map and cons that operate on lists without mentioning tokens in the type signatures. But is it sound?...

[andrewthad]

I have dynamically_ wrong. It should be:

dynamically_ :: Object a => Reference a ->. (a ->. Action Dynamic ->. (Action Dynamic,a)) ->. Action Static ->. Action Static

It needs to be this way since we want to preserve replace the payload and then immidiately discard the reference. But what about the more simple:

dynamically_ :: Object a => Reference a ->. (a ->. Action Dynamic ->. (Action Dynamic,a)) ->. Reference a

Does this work? To recover the behavior of the one suggested above, one could combine this with read.

[andrewthad]

Hmmm... The definition of dynamically_ now implies that we can only allocate if we already have a reference in scope. But how do we get the very first reference?

[andrewthad]

Maybe the top-level continuation-accepting function would be:

run :: (Reference () ->. Unrestricted b) ->. Unrestricted b

The type of this feels a little unnatural though.

[andrewthad]

Even better would be:

run :: (Action Dynamic ->. (Action Dynamic,Unrestricted a)) ->. Unrestricted a

This is basically like dynamically except that it is missing the reference/payload component. It makes sense that we have to start in a dynamic context. If we started in a static context, there would be nothing to do.

[chessai]

I thought we would need to start in a neutral context?

[andrewthad]

Starting in a neutral context does not work. Starting with only a Token, there is no way to create a Reference.

[chessai]

Static: read, ignore Dynamic: deallocate Neutral: allocate, modify

am i interpreting this incorrectly?

[andrewthad]

In the type signature for allocate (the one in the code block above has an unintended omission), I changed my mind on that:

allocate :: forall a. Object a                                                                        
  =>  a                                                                                               
  ->. Action 'Dynamic                                                                                 
  ->. (Action 'Dynamic, Reference a)                                                                  

If allocate could run in a neutral context, then you could allocate something in a static context and then ignore the reference. This would leak memory.

[chessai]

okay

[andrewthad]

This was completed in 770ad31bc42c5382f74a71f194f1b5c062e968fe.

[andrewthad]

Dang. This is not sound. With statically_, we can throw away arbitrary references.

[chessai]

rip happiness

[andrewthad]

I have reverted back to the old approach with a force push to master. I cannot figure out a way to do this without pushing a static/dynamic distinction to into the types. This is unfortunate because the types could be much pretty. However, I am growing more confident that this somewhat cumbersome system is actually sound.

[chessai]

happiness = fleeting