Opened 20 months ago

Last modified 12 months ago

#14770 new feature request

Allow static pointer expressions to have static pointer free variables

Reported by: TheKing01 Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: StaticPointers Cc: gershomb
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Static pointer expressions can not have free variables. For example:

addPointers :: StaticPtr Int -> StaticPtr Int -> StaticPtr Int
addPointers x y = static (deRefStaticPtr x + deRefStaticPtr y)

would be invalid, since x and y are free variables. My proposal would be to make this code sample valid. In particular, my proposal is to allow free variables in static expressions if the free variables of the type StaticPtr a for some type a.

Let's say that m n are Static pointers to integers. The serialized form would of addPointers m n would be:

A pointer to the code deRefStaticPtr x + deRefStaticPtr y

The serialized form of m, associated with x.

The serialized form of n, associated with y.

When this is sent over the wire and dereferenced, the other machine would

Find m and n's pointers

Find the code deRefStaticPtr x + deRefStaticPtr y

Evaluate deRefStaticPtr x + deRefStaticPtr y, substituting m's value for x, and n's value for y.

The reason this feature would be useful is would let the user modify and combine static pointers.

You might ask "why not let the user create a GADT to do that (like in https://hackage.haskell.org/package/distributed-static-0.3.8/docs/Control-Distributed-Static.html#t:Static)?" The reason is that then it won't fuse (with recreating every fusion rule for that GADT). For example, if m is static 7 and n is static 3, then addPointers m n can fuse to static 11.

This is more important then it seems. For example, say you have composePointers :: StaticPtr (a -> b) -> StaticPtr (b -> c) -> StaticPtr (a -> c), and you compose a bunch of pointers. With the GADTS, every composePointers would be its own node, but with GHC support, it would probably fuse.

In general, dealing with a GADT requires a lot of "glue code" that can be eliminated with GHC support. I'm not sure if this proposal makes a performance difference (it probably makes it more efficient), but it would make code more elegant, cutting out all the glue code.

Change History (9)

comment:1 Changed 19 months ago by facundo.dominguez

I don't understand how this works yet.

Static pointers are put in the static pointer table (SPT) before the program executes. What is put in the SPT if the static form is allowed to have free variables?

Before executing the program, the values of the free variables might be still unknown.

comment:2 Changed 19 months ago by TheKing01

The code surrounding the free variables is put in the SPT. A static pointer then points to that code, as well as separate static pointers for the free variables. This makes static pointers a recursive data type.

comment:3 Changed 14 months ago by gershomb

Cc: gershomb added

comment:4 Changed 14 months ago by simonpj

Gershom: you've just added yourself in cc. Do you have a use-case?

Generally, this ticket would be much stronger if there were some concrete examples. I'm pretty sympathetic to the line of reasoning -- I think that static pointers are not yet "right" -- but we need compelling examples.

comment:5 Changed 14 months ago by gershomb

No concrete use-case at the moment (in that I'm not working on a system that does cloud distribution). I wanted to track this ticket as I've been thinking a lot about questions related to this ticket, including possible other uses for static and how it relates to Contextual Modal Type Theory (and also the question of staging).

I think the ticket has the right of it in terms of the problem. Semantically, the "correct" thing to do is, treating StaticPtr as a modality, allow computation _within_ the modality such that we have StaticPtr (a -> b) -> StaticPtr a -> StaticPtr b directly. Instead, we have the workaround the ticket points to, which makes use of an opaque GADT. So that means, as the ticket says, this gives (on its own) a potential efficiency gain, but not expressivity gain.

I think we'll need more people using static pointers "at scale" to see if the efficiency cost becomes a genuine pain point.

comment:6 Changed 14 months ago by simonpj

I think the ticket has the right of it in terms of the problem. Semantically, the "correct" thing to do is,...

I agree with the direction of travel. But I'm keen to see concrete use-cases.

comment:7 Changed 13 months ago by mpickering

This ticket seems to really want a splice like operator for static forms.

comment:8 Changed 13 months ago by mpickering

I think the comment in comment:2 is suggesting that the result of a static expression is *not* a StaticPtr.

Terminology:

  • A StaticPtr is something which resides in the static pointer table.
  • A Closure is an expression which can be serialised.

We now distinguish the two situations with two keywords.

  • static <e :: T> creates a value of StaticPtr T where e is placed in the SPT. The current restrictions about static forms apply to e.
  • closure <e :: T> creates a value of Closure T as per the proposal, free variables in e are allowed to refer to values of type Closure.

We first give the concrete definition of Closure which is a simplified version of Closure from the static-closure package.

data Closure a where                                                            
  CPure :: Closure (ByteString -> a) -> ByteString -> a -> Closure a              
  CStaticPtr :: StaticPtr a -> Closure a                                         
  CAp :: Closure (a -> b) -> Closure a -> Closure b                              

Then the RHS of addPointers from the original post desugars to:

addPointers :: Closure Int -> Closure Int -> Closure Int                         
addPointers c1 c2 = closure ( $$c1 + $$c2 )                                       
===>                                                                             
addPointers c1 c2 = static (+) `CAp` c1 `CAp` c2                                 

Static parts of the expression are still added to the SPT by using static. Dynamic parts of the expression are then applied using CAp.

This definition also allows us to directly embed serialisable values into the static form.

addOneToPointer :: Closure Int -> Closure Int                                   
addOneToPointer p = closure (1 + $$p)                                            
===>                                                                            
addOneToPointer c1 = static (+) `CAp` (CPure (static decode) (encode 1) 1) `CAp` c1

The mechanical transformation that we're performing here is we take a static form, abstract over the spliced variables and then reapply the result of the splice. Let floating the splices in essence.

This definition of Closure still allows us to serialise a Closure to a bytestring and deserialise it. It also allows us to "dereference" the closure just like you can dereference a StaticPtr.

I think the whole static-closure library is lovely and looks like a nice way to make writing StaticPointers code more easily.

comment:9 Changed 12 months ago by simonpj

I still want examples of usage! Who needs these extra facilities?

Note: See TracTickets for help on using tickets.