Static Choices and Offerings

[David Barbour]

[from: To Quota or not]

On Fri, Aug 16, 2013 at 11:19 PM, Ross Angle <rok...@gmail.com> wrote:

I think all I want is for that "block" type to be well-understood.

This is unrelated to 'well-understood' termination and quotas, but I rather another aspect of our block types:

First, assume a concept of choice - much like sums, except static:

        leftChoice :: (Static (x ~> x') * (x | y)) ~> (x' | y)

        mirrorChoice :: (x|y) ~> (y|x)

        assoclChoice :: (x|(y|z)) ~> ((x|y)|z)

The following approach seems opaque:

        isProduct :: x ~> (Static Boolean * x)

        isSum :: x ~> (Static Boolean * x)

        isGreaterZero :: Static Int ~> Static Boolean 

        orStatic :: (Static Boolean * Static Boolean) ~> Static Boolean

        staticDisjoin :: (Static Boolean * x) ~> (x | x)

        isProduct staticDisjoin

Information about what choice is made transitions through this lossy bottleneck called 'Boolean' . It is especially lossy across `orStatic`

The following approach would seem to expose dependent types and type-matching pretty well:

        exposeProduct :: x ~> ((a * b) | x)

        exposeSum :: x ~> ((a + b) | x)

        exposeStaticChoice :: x ~> ((a | b) | x)

        exposeGreaterZero :: (Static Int * x) ~> (Static Int * x) | (Static Int *  x)

There should be fewer ops (since I avoid Static Boolean type entirely), but I do lose the ability to operate using ad-hoc polymorphism on multiple branches (like `orStatic` enables). I might regain that:

        -- (x|y) means the type is x or y, and I know which

        -- (x\y) means the type is x or y, but I've lost info about which. x\x is essentially just x.

        mergeStaticChoice :: (x|y) ~> (x\y)

Induction-recursion operations could be defined for products, sums, and static choices; if our aim is to expose these types as well as possible, then having those as primitives might serve us more effectively than burying values in a fixpoint combinator. 

Inverted, we might want to leave a choice to the client of a value. In the earlier formation, this essentially matches a rational type ((x|y) / Boolean), which is again lossy info due to booleans; it's also getting a tad ugly since we now have booleans on both ends and it's difficult to grok how they should be combined. In the latter formation, I might want to model this in terms of a new type:

       -- (x & y): I'm statically offering both x and y, and you must pick one

       initOffering :: x ~> (x & x)

       firstOffering :: (Static (x ~> x') * (x & y)) ~> (x' & y)

       swapOffering :: (x & y) ~> (y & x)

       assoclOffering :: (x & (y & z)) ~> (x & (y & z))

       acceptOffering :: (x & y) ~> x

       exposeOffering :: x ~> ((a&b)|x)

To drop an offering, you must accept an offering then drop it (just in case there are linear types hidden within it). We can also develop induction-recursion over offerings.

(An interesting possibility is to build a `heuristicChooseOffering` atop the induction-recursion.)

I'll probably need to add a bunch of distributive operations, which will generally be lossy.

[Ross Angle]

On Sat, Aug 17, 2013 at 9:45 AM, David Barbour <dmba...@gmail.com> wrote:

[from: To Quota or not]

On Fri, Aug 16, 2013 at 11:19 PM, Ross Angle <rok...@gmail.com> wrote:

I think all I want is for that "block" type to be well-understood.

This is unrelated to 'well-understood' termination and quotas, but I rather another aspect of our block types:

First, assume a concept of choice - much like sums, except static:

My intuition leads me to disagree with the idea that sums are not static, but I can see value in your approach.

With an (x | y) type, you can tell whether it's x or y at compile time. With (x + y), you can only tell at run time, and only if you're at a partition that can observe both sides. So far so good. However, if (x + y) contains static data signals, then the idea that "you can only tell at run time" actually refers to the run time of the static signals, which is compile time.

As I think about static signals inside (x + y), I'm noticing some surprises. For Underreact, I would want to ensure that a static signal cannot bdisjoin across a purely dynamic condition, because the static "partition" can't observe enough branch information to do filtering. And come to think of it, we cannot actually have a general operation (1 ~> Static ()), because then we could apply this inside a dynamic (x + y) choice to cause the same problem.

There's a certain clear advantage for having (x | y) as a distinct type. In dependent typing terms, it could be pretty easily encoded as a sigma type: (SigSuchThat (Static Boolean) (b) ~ If b Then x Else y). In general, the sigma type for (x + y) would have to do something special to account for the fact that not every partition can observe the boolean. I'm not sure what that would look like yet.

The following approach would seem to expose dependent types and type-matching pretty well:

        exposeProduct :: x ~> ((a * b) | x)

        exposeSum :: x ~> ((a + b) | x)

        exposeStaticChoice :: x ~> ((a | b) | x)

        exposeGreaterZero :: (Static Int * x) ~> (Static Int * x) | (Static Int *  x)

This reminds me of Haskell's Data.Dynamic, which can be more generic thanks to typeclasses:

toDyn :: (Typeable a) => a -> Dynamic

fromDynamic :: (Typeable a) => Dynamic -> Maybe a

I do this in Era for the Sink type, but I hardcode it for just three cases right now, since I don't have typeclasses.

There should be fewer ops (since I avoid Static Boolean type entirely), but I do lose the ability to operate using ad-hoc polymorphism on multiple branches (like `orStatic` enables). I might regain that:

        -- (x|y) means the type is x or y, and I know which

        -- (x\y) means the type is x or y, but I've lost info about which. x\x is essentially just x.

        mergeStaticChoice :: (x|y) ~> (x\y)

I think (x \ y) is almost just (x + y), except that you're choosing not to peek at the branch information. This makes it related to the distinction between strong and weak existentials. In one case we're allowed to derive the example value (in this case a Boolean), and in the other case we aren't. Here's some nice discussion about the terminology.

Inverted, we might want to leave a choice to the client of a value. In the earlier formation, this essentially matches a rational type ((x|y) / Boolean), which is again lossy info due to booleans; it's also getting a tad ugly since we now have booleans on both ends and it's difficult to grok how they should be combined.

I find fractional types pretty hard to grok, but I think I can say at least this much: They can do causal loops, so if you use them to carry any dup'able types, those types will need to be under beat indexes... or maybe some kind of linear reference type (Linear Boolean) that gets consumed upon dereference.

In the latter formation, I might want to model this in terms of a new type:

       -- (x & y): I'm statically offering both x and y, and you must pick one

       initOffering :: x ~> (x & x)

       firstOffering :: (Static (x ~> x') * (x & y)) ~> (x' & y)

       swapOffering :: (x & y) ~> (y & x)

       assoclOffering :: (x & (y & z)) ~> (x & (y & z))

       acceptOffering :: (x & y) ~> x

       exposeOffering :: x ~> ((a&b)|x)

To drop an offering, you must accept an offering then drop it (just in case there are linear types hidden within it). We can also develop induction-recursion over offerings.

Whew, this is just the linear logic dual of +. No cause for alarm. :)

Though I wonder whether the upstream code would be able to peek at the co-(Static Boolean) chosen by the downstream code. That is to say, maybe you'll also want duals of (x | y) and (x \ y). Running out of space on the keyboard yet? :-p

-Ross

[Ross Angle]

On Sat, Aug 17, 2013 at 6:15 PM, Ross Angle <rok...@gmail.com> wrote:

I find fractional types pretty hard to grok, but I think I can say at least this much: They can do causal loops, so if you use them to carry any dup'able types, those types will need to be under beat indexes... or maybe some kind of linear reference type (Linear Boolean) that gets consumed upon dereference.

Nope, (Linear Boolean) doesn't help at all. We can create a Boolean with no initial cause like so:

1

1/(Linear Boolean) * Linear Boolean

1/(Linear Boolean) * Boolean

1/(Linear Boolean) * Boolean * Boolean

1/(Linear Boolean) * Linear Boolean * Boolean

1 * Boolean

Boolean

-Ross

[David Barbour]

On Sat, Aug 17, 2013 at 6:15 PM, Ross Angle <rok...@gmail.com> wrote:

if (x + y) contains static data signals, then the idea that "you can only tell at run time" actually refers to the run time of the static signals, which is compile time.

We might be able to tell at compile-time if we *split* on a static signal (or used intro0). But the '+' type loses that tidbit of information. We can feasibly convert from (x|y) ~> (x+y), but never the inverse. An important reason for (x | y) is that we want eventually to 'forget' about most branches without ever properly merging. The outcome of a static choice is accessible to developers, and they don't want to keep considering every possible branch. Another good reason is that disjoin is trivial on (x | y). 

Whew, this is just the linear logic dual of +. No cause for alarm. :)

I think offerings will be a usable/grokkable way to express backwards flowing static choices. It's more the dual of `|`.

 

maybe you'll also want duals of (x | y) and (x \ y). Running out of space on the keyboard yet? :-p

The `\` type is not observable to developers (it means we've forgotten which branch) so I'm not sure how to model a dual for it. The offering is already the dual for (x | y).

So far, I don't believe a dual for a runtime choice is feasible in Awelon. A backwards flowing runtime choice is closer to:  1/(x+y).

[Ross Angle]

On Sat, Aug 17, 2013 at 7:31 PM, David Barbour <dmba...@gmail.com> wrote:

On Sat, Aug 17, 2013 at 6:15 PM, Ross Angle <rok...@gmail.com> wrote:

if (x + y) contains static data signals, then the idea that "you can only tell at run time" actually refers to the run time of the static signals, which is compile time.

We might be able to tell at compile-time if we *split* on a static signal (or used intro0). But the '+' type loses that tidbit of information. We can feasibly convert from (x|y) ~> (x+y), but never the inverse. An important reason for (x | y) is that we want eventually to 'forget' about most branches without ever properly merging. The outcome of a static choice is accessible to developers, and they don't want to keep considering every possible branch. Another good reason is that disjoin is trivial on (x | y). 

From where I'm seeing things, the only part I disagree with is "But the '+' type loses that tidbid of information."

If it helps, I consider there to be an isomorphism between (x | y) and ((Static () * x) + (Static () * y)). This means if (x + y) contains enough static signals, it's possible to reconstruct (x | y).

So far, I don't believe a dual for a runtime choice is feasible in Awelon. A backwards flowing runtime choice is closer to:  1/(x+y).

Fractional types for runtime signals?

== An interpretation of the original paper ==

I took a close look at the small-step operational semantics presented in "Negative and Fractional Types." It's specified as a nondeterministic transition system. Half the rules of the system describe the upstream behavior and half describe the downstream behavior, and these are bridged by the use of negative types. Nondeterministic branching arises in these cases:

• A downstream or upstream input to the composed circuit (c1 + c2) is unified against both (left v) and (right v), in two nondeterministic branches.
  
• For the multiplicative elimination circuit, which takes values of type ((1/a) * a) to 1, a downstream input is unified against (1/v, v). This won't necessarily succeed. (Upstream inputs on the multiplicative introduction circuit behave likewise.)
• For the additive elimination circuit, which takes values of type (-a + a) to 0, the downstream input is unified against both (left -v) and (right v), in two nondeterministic branches. Then the stream direction is flipped. (Upstream inputs on the additive introduction circuit behave likewise.)
  

Given a program which takes type `x` to type `y`, we can execute it as follows: We determine a set of logic variables that corresponds to all the positive parts of `x` and the negative parts of `y`, and we provide a nondeterministic selection of constraint sets to describe our inputs to those variables. As output, we receive a set of logic variables that corresponds to all the negative parts of `x` and the positive parts of `y`, along with a nondeterministic selection of constraint sets which describe the outputs from those variables. We can also switch this, providing inputs to the negative parts and receiving outputs from the positive ones.

(Actually, I'm not quite sure how to formalize "positive parts" and "negative parts" here. If a type contains (1 + (1 + -1)), then the first two 1's are positive parts, and we'll actually have only one of them as input (or output).)

If the input has total information (a single nondeterministic branch whose constraints describe complete input values), then I believe the same will be true of the output. On the other hand, an underconstrained variable may turn into multiple branches or vice versa, and certain programs may impose constraints on our input so that if we provide something incorrect, our branches fail. For instance, a program can take ((1 / (1 + 1)) * (1 + 1)) to 1, using the multiplicative elimination primitive. If the input we provide is ((1 / left ()), right ()), then it won't unify properly, so the branch will fail.

== An interpretation for RDP continuous-time signals ==

For RDP's run time signals, I think we would want to implement this nondeterminism in such a way that we can reason about latency, and we would not want to execute any side effects on branches which are going to fail... which I suppose means we don't want to fail.

When we backbeat ((1 / x) * x), whichever parts of these signals carry continuous-time information downstream, this information must combine to represent *all* the constraints, and these constraints must always be consistent (but perhaps insufficient to determine a full "value," if we're willing to nondeterministically branch with multiple successes). The signals must also have some well-defined way to propagate this information back upstream. (Since the constraints must be consistent, we probably don't actually need to represent them. We can just carry partial values along the signal. On the other hand, I doubt there's a clear physical representation of a signal (Atom hither t + Atom yonder t) where the choice is underconstrained.)

When we backbeat (-x + x), the continuous-time downstream parts must usually be enough to determine whether the left signal or the right signal is originally active, so that we don't have to nondeterministically branch and then fail. On the other hand, if the branch depends on an underconstrained logic variable, then both branches will succeed, so we may want to execute them both somehow. No matter how we proceed from here, we need to propagate the original data (plus a logic constraint, if necessary) along the other side's signal. Hence, that signal must have some well-defined way to send this continuous-time information upstream.

Now let's consider the isomorphisms between (-a * b) and (- (a * b)) and (a * -b). To make sense of these, we don't necessarily want `-a` to reverse each signal type of `a`. Instead, we probably want `-a` to be limited so that it only acts on signals `a` which are symmetrical enough that (-a + a) can plug together. As long as we're talking about continuous-time signals, some examples of `a` might include (Atom p t * Co (Atom p t)) and, um, ((1 + Atom p t) * Co (1 + Atom p t)), where (Co _) is a modality for upstream-downstream reversal. (I would use linear negation, but (1 / _) might work too.)

As far as I can tell right now, these design decisions might lead to a working system, but there are many compromises to to be made on the way there. The way I see it, we don't get the same nondeterministic model, we have to limit (1 / _) to linear types, and we have to limit (- _) to some kind of self-pluggable types. Does this seem to be in line with what you're thinking?

Warm Regards,

Ross

[David Barbour]

On Mon, Aug 19, 2013 at 8:33 PM, Ross Angle <rok...@gmail.com> wrote:

If it helps, I consider there to be an isomorphism between (x | y) and ((Static () * x) + (Static () * y)). This means if (x + y) contains enough static signals, it's possible to reconstruct (x | y).

Containing static signals does not mean anything about the runtime activity is known. 

     myBeh :: S p () ~> (S p () + S p ())

     myBeh = getMousePos testInsideWindow split [intro1] 

     myBeh' :: S p () ~> ((Static () * S p ()) + (Static () * S p ()))

     myBeh' = myBeh [intro1] left [intro1] right

The split, here, is based on a dynamic signal. It doesn't matter that the right-hand type contains statics. 

The (x | y) type, however, means that the choice itself was static.

For statics to interact with runtime behaviors requires first lowering them into the runtime (like `bconst` in Sirea):

     constInteger :: (Static Integer * S p ()) ~> (S p Integer) 

      -- (partition specific; not all partitions support all number sizes)

One can intuit the Static types either being continuously active or never active or just imaginary/unrealized; it doesn't matter because it isn't visible at runtime.

 

a program can take ((1 / (1 + 1)) * (1 + 1)) to 1, using the multiplicative elimination primitive. If the input we provide is ((1 / left ()), right ()), then it won't unify properly, so the branch will fail

The primitives of shape (1/x * x) would, of course, need to simply output their own input.

      beat :: 1 ~> (1/x * x) 

      backbeat :: (1/x * x) ~> 1

What you describe is the backbeat operation, just instantiated for x=(1+1).

But there is nothing preventing developers from creating systems that input left and output right. It just takes a simple mirroring operation:

     backbeatWithTwist = [mirror] second backbeat

At this point, we could input `right ()` and output `1 / left ()`, no problem. I'm thinking the problem with the unification argument you presented is that it's shallow. 

In any case, I really don't follow the "non-determinism"  claim; they mention non-determinism in an analogy to logic systems, but I don't believe non-determinism is part of their semantics. Indeed, it seems very deterministic. Relevant to the case you presented: "In the case of sums, the shape of the value, i.e., whether it is tagged with left or right, determines whether path c1 or path c2 is taken."

 

When we backbeat (-x + x), the continuous-time downstream parts must usually be enough to determine whether the left signal or the right signal is originally active, so that we don't have to nondeterministically branch and then fail. 

Yeah, that sounds right. Though, I might want another name for sums. Hmm.

 

Now let's consider the isomorphisms between (-a * b) and (- (a * b)) and (a * -b). To make sense of these, we don't necessarily want `-a` to reverse each signal type of `a`.

Why not? Perhaps we should think of `-a` as a backwards flowing a.

Actually, it makes sense to have a couple more generic operations:

         turninDatBeatAround :: Static (x ~> y) ~> Static (1/y ~> 1/x)

         negativeBehavior :: Static (x ~> y)  ~> Static ( (-y) ~> (-x) )

 

Instead, we probably want `-a` to be limited so that it only acts on signals `a` which are symmetrical enough that (-a + a) can plug together. As long as we're talking about continuous-time signals, some examples of `a` might include (Atom p t * Co (Atom p t)) and, um, ((1 + Atom p t) * Co (1 + Atom p t)), where (Co _) is a modality for upstream-downstream reversal. (I would use linear negation, but (1 / _) might work too.)

As far as I can tell right now, these design decisions might lead to a working system, but there are many compromises to to be made on the way there. The way I see it, we don't get the same nondeterministic model, we have to limit (1 / _) to linear types, and we have to limit (- _) to some kind of self-pluggable types. Does this seem to be in line with what you're thinking?

Warm Regards,

Ross

--
You received this message because you are subscribed to the Google Groups "reactive-demand" group.
To unsubscribe from this group and stop receiving emails from it, send an email to reactive-dema...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[David Barbour]

Ack! Some keyboard combo sent this prematurely. I'll just continue where I left off.

On Tue, Aug 20, 2013 at 12:32 AM, David Barbour <dmba...@gmail.com> wrote:

         turninDatBeatAround :: Static (x ~> y) ~> Static (1/y ~> 1/x)

         negativeBehavior :: Static (x ~> y)  ~> Static ( (-y) ~> (-x) )

Technically, these two operations shouldn't be difficult to implement by bracketing them with beat and backbeat messages (or their - + equivalents). But if we make primitives of them, we could leave the beat index alone.

 

 

As far as I can tell right now, these design decisions might lead to a working system, but there are many compromises to to be made on the way there. The way I see it, we don't get the same nondeterministic model, we have to limit (1 / _) to linear types, and we have to limit (- _) to some kind of self-pluggable types. Does this seem to be in line with what you're thinking?

Actually, they're looking cleaner to me the more I think about them. I still don't have an intuition for negative types, but thinking about it in terms of overall shape of the program makes it easier.

Warm Regards,

Dave

[Ross Angle]

On Tue, Aug 20, 2013 at 12:32 AM, David Barbour <dmba...@gmail.com> wrote:

On Mon, Aug 19, 2013 at 8:33 PM, Ross Angle <rok...@gmail.com> wrote:

If it helps, I consider there to be an isomorphism between (x | y) and ((Static () * x) + (Static () * y)). This means if (x + y) contains enough static signals, it's possible to reconstruct (x | y).

Containing static signals does not mean anything about the runtime activity is known. 

Oh, that makes sense! That's very interesting.

     myBeh' :: S p () ~> ((Static () * S p ()) + (Static () * S p ()))

     myBeh' = myBeh [intro1] left [intro1] right

I'm not sure it makes a difference for the point you're making, but I don't think you can introduce those static signals like that. It makes the static computation branch on... nothing, because (S p ()) is active only at dynamic coordinates.

(As I said above: "And come to think of it, we cannot actually have a general operation (1 ~> Static ()), because then we could apply this inside a dynamic (x + y) choice to cause the same problem.")

One can intuit the Static types either being continuously active or never active or just imaginary/unrealized; it doesn't matter because it isn't visible at runtime.

The way I see it, a Static signal is active instantaneously, carrying a single value at compilation time. If it's in a dead program branch, then it's inactive. At run time, its activity is indeterminate (the same as S1), because it doesn't exist at any run time coordinates.

 

a program can take ((1 / (1 + 1)) * (1 + 1)) to 1, using the multiplicative elimination primitive. If the input we provide is ((1 / left ()), right ()), then it won't unify properly, so the branch will fail

The primitives of shape (1/x * x) would, of course, need to simply output their own input.

      beat :: 1 ~> (1/x * x) 

      backbeat :: (1/x * x) ~> 1

What you describe is the backbeat operation, just instantiated for x=(1+1).

That's what I said, but using "multiplicative elimination primitive" instead of "backbeat." Keep in mind this was under the heading "An interpretation of the original paper," so both `x` and (1 / x) are considered to be inputs which are logic variables. The way we're trying to interpret this for RDP, (1 / x) is an output instead, and it'll probably carry full values instead of logic variables.

But there is nothing preventing developers from creating systems that input left and output right. It just takes a simple mirroring operation:

     backbeatWithTwist = [mirror] second backbeat

At this point, we could input `right ()` and output `1 / left ()`, no problem.

I realize you're talking about an RDP interpretation, but just to be clear about the paper's interpretation: If we try to invoke that program with an input value of ((1 / left ()), left ()), we'll get nondeterministic failure.

I'm thinking the problem with the unification argument you presented is that it's shallow. 

In any case, I really don't follow the "non-determinism"  claim; they mention non-determinism in an analogy to logic systems, but I don't believe non-determinism is part of their semantics. Indeed, it seems very deterministic. Relevant to the case you presented: "In the case of sums, the shape of the value, i.e., whether it is tagged with left or right, determines whether path c1 or path c2 is taken."

You're quoting the wrong part of the paper. That's before they introduce negative and fractional types.

"Previously the shape of the value determined which of the combinators c1 or c2 to use. Now the incoming value could be a fresh logical variable, and indeed we have two rules with the same left hand side, and only depending on the success or failure of some further unification, can we decide which of them applies. The situation is common in logic programming in the sense that it is considered a non-deterministic process that keeps searching for the right substitution if any."

When we backbeat (-x + x), the continuous-time downstream parts must usually be enough to determine whether the left signal or the right signal is originally active, so that we don't have to nondeterministically branch and then fail. 

Yeah, that sounds right. Though, I might want another name for sums. Hmm.

 

Now let's consider the isomorphisms between (-a * b) and (- (a * b)) and (a * -b). To make sense of these, we don't necessarily want `-a` to reverse each signal type of `a`.

Why not? Perhaps we should think of `-a` as a backwards flowing a.

So we can start with a backwards flowing `a` and a forwards flowing `b`, and then we can use the the (-a * b) to (a * -b) isomorphism to derive a forwards flowing `a` and a backwards flowing `b`? I don't know how to make sense of that.

(I don't have any particular response to your follow-up email.)

Warm Regards,

Ross

[David Barbour]

On Wed, Aug 21, 2013 at 10:01 AM, Ross Angle <rok...@gmail.com> wrote: 

One can intuit the Static types either being continuously active or never active or just imaginary/unrealized; it doesn't matter because it isn't visible at runtime.

The way I see it, a Static signal is active instantaneously, carrying a single value at compilation time. If it's in a dead program branch, then it's inactive. At run time, its activity is indeterminate (the same as S1), because it doesn't exist at any run time coordinates.

Okay, I'll try to represent this based on the way you see things.

In the normal case (e.g. branching on dynamic information), static information - such as the type - must flow down BOTH branches of (x + y). Thus, you should think of `(x + y)` as having a corresponding static product carrying ("sum" * (typeRep(x)*typeRep(y)) ). By comparison, (x | y) is a true static decision. The instantaneous signal has a nature closer to ("left" * typeRep(x)) or ("right" * typeRep(y)), and we're free to just ignore the branches we aren't taking. We can think of `intro1` as operating on the 'static signal' that carries type information. Since `x` always has a type signal (proof: we're looking at a type called 'x'), we can always operate on that signal to form `1*x`. In case of (x + y), we always have the correct underlying typeRep for signal processing such that applying `[intro1] left` will compute a new type ((1*x)+y). No problems there!

The `+` type cannot be said to know which branch it is on. If there is a marker for dead code, it should be part of the `x` or `y` types. In that case, `intro1` would move us from `dead(x)` to `dead(1*x)`. It is, of course, possible that both branches are dead.

One could think about (x | y) as a constraint on a fuller implicit ("sum" * (typeRep(x)*typeRep(y)) signal, where this constraint says that one of those entries is dead. One might even implement it as such. But, as a programmer, I find it worth thinking about (x | y) and (x + y) as different types with somewhat different characteristics (e.g. regarding distribution and merge).

But there is nothing preventing developers from creating systems that input left and output right. It just takes a simple mirroring operation:

     backbeatWithTwist = [mirror] second backbeat

At this point, we could input `right ()` and output `1 / left ()`, no problem.

I realize you're talking about an RDP interpretation, but just to be clear about the paper's interpretation: If we try to invoke that program with an input value of ((1 / left ()), left ()), we'll get nondeterministic failure.

What would be non-deterministic about that failure?

Anyhow, the paper on rational types initially introduced logic variables as an "analogy" to help "explain" their semantics. When I read the paper, I mentally substituted it with 'arrows' and 'wires' all the way through, without difficulty, so I kind of forgot logic variables were mentioned at all.

  

 

Now let's consider the isomorphisms between (-a * b) and (- (a * b)) and (a * -b). To make sense of these, we don't necessarily want `-a` to reverse each signal type of `a`.

Why not? Perhaps we should think of `-a` as a backwards flowing a.

So we can start with a backwards flowing `a` and a forwards flowing `b`, and then we can use the the (-a * b) to (a * -b) isomorphism to derive a forwards flowing `a` and a backwards flowing `b`? I don't know how to make sense of that.

You're right. The negative type doesn't mean "flowing backwards" in context of a pair.  If `a` was flowing backwards through a product, it would be 1/a. 

Obviously, I still don't have a good intuition for negative types. Perhaps one can consider it as a more restrictive form of vacuous proof.

Fractionals I understand much better - they're concrete, tangible, just running against the stream.

Warm Regards,

Dave

[Ross Angle]

On Wed, Aug 21, 2013 at 1:20 PM, David Barbour <dmba...@gmail.com> wrote:

On Wed, Aug 21, 2013 at 10:01 AM, Ross Angle <rok...@gmail.com> wrote: 

One can intuit the Static types either being continuously active or never active or just imaginary/unrealized; it doesn't matter because it isn't visible at runtime.

The way I see it, a Static signal is active instantaneously, carrying a single value at compilation time. If it's in a dead program branch, then it's inactive. At run time, its activity is indeterminate (the same as S1), because it doesn't exist at any run time coordinates.

Okay, I'll try to represent this based on the way you see things.

In the normal case (e.g. branching on dynamic information), static information - such as the type - must flow down BOTH branches of (x + y). Thus, you should think of `(x + y)` as having a corresponding static product carrying ("sum" * (typeRep(x)*typeRep(y)) ). By comparison, (x | y) is a true static decision. The instantaneous signal has a nature closer to ("left" * typeRep(x)) or ("right" * typeRep(y)), and we're free to just ignore the branches we aren't taking. We can think of `intro1` as operating on the 'static signal' that carries type information. Since `x` always has a type signal (proof: we're looking at a type called 'x'), we can always operate on that signal to form `1*x`. In case of (x + y), we always have the correct underlying typeRep for signal processing such that applying `[intro1] left` will compute a new type ((1*x)+y). No problems there!

I've had to ponder this explanation for a while, and I think I finally came around to understanding exactly what you're saying. If not, then I might want to keep going with my misinterpretation as an idea of its own, lol. ;)

You have a type grammar you use to represent types in type signatures, and then for the Static pass you manipulate richly type-tagged values. If we take a look at those type tags on their own, they're not quite the same type grammar as the type signatures.

Given a richly type-tagged value and a type signature, there happens to be an algorithm we can use to check whether the former is an example of the latter. That's a nice way to show the two grammars and their relationship:

import Data.Typeable (TypeRep)

import Data.Dynamic (Dynamic)

-- type signature (named after "annotation")

data Ann =

    AnnRunTimeAtom Partition TimeOffset TypeRep

  | AnnStaticAtom BeatIndex TypeRep

  | AnnZero

  | AnnSum Ann Ann

  | AnnOne

  | AnnProduct Ann Ann

  | AnnStaticChoice Ann Ann

  | AnnStaticForgottenChoice Ann Ann

  | ...

-- value manipulated by the Static pass (named after "interface")

data Face =

    FaceRunTimeAtom Partition TimeOffset TypeRep AttachableHose

  | FaceStaticAtom BeatIndex TypeRep Dynamic

  | FaceZero

  | FaceSum Face Face

  | FaceOne

  | FaceProduct Face Face

  | FaceStaticLeft Face

  | FaceStaticRight Face

  | ...

check :: Face -> Ann -> Boolean

check (FaceRunTimeAtom fp fTime fType _) (AnnRunTimeAtom ap aTime aType) =

  (fp, fTime, fType) == (ap, aTime, aType)

check (FaceStaticAtom fi fType _) (AnnStaticAtom ai aType) =

  (fi, fType) == (ai, aType)

check FaceZero AnnZero = True

check (FaceSum fx fy) (AnnSum ax ay) = check fx ax && check fy ay

check FaceOne AnnOne = True

check (FaceProduct fx fy) (AnnProduct ax ay) = check fx ax && check fy ay

check (FaceStaticLeft fx) (AnnStaticChoice ax ay) = check fx ax

check (FaceStaticRight fy) (AnnStaticChoice ax ay) = check fy ay

check face (AnnStaticForgottenChoice ax ay) = check face ax || check face ay

...

check _ _ = False

For the example of "flow down BOTH branches of (x + y)," the type signature is (AnnSum x y), and at the Static level we manipulate a value of the form (FaceSum x y). This value can contain complex data (here represented as the Dynamic part of FaceStaticAtom) and/or enough information to manipulate the flow of run time signals (here represented as the AttachableHose part of FaceRuntimeAtom).

This AttachableHose metaphor is used by Truenorth's Corelet Language, which has a static pass that... well, really attaches these suckers. My implementation of Underreact works the same way, and I get the impression this technique is very common. Heck, it's just imperative graph construction, lol.

Well, I imagine you're not actually thinking of using AttachableHoses. You're thinking the Static layer would perform an *effectful* transformation from Face to Face, where the effect is to generate an appropriately typed run time behavior. For instance, you can use (>>>) or (***) or (+++) to compose two Static-layer computations, and the resulting dynamic behavior will automatically represent the corresponding (>>>) or (***) or (+++) composition on the run time network. But (+++) composition is an odd case here: For the run time network it represents two mutually exclusive paths, but for the Static-layer computations it represents a parallel transformation of both sides of a FaceSum (just like (***) acts on both sides of a FaceProduct). In this way, you really do "flow down BOTH branches of (x + y)."

This is pretty interesting stuff. I keep wondering how to represent staged programming in a way that's more seamless with normal programming, and I think this is it. If we extrapolate from your two-stage model, I think we'll arrive at a wonderfully elegant stage-indexed family of sum operators. :)

I'd like to make sure we can extrapolate this into a stage-indexed family of Sigma types. That'll be interesting to think about, since I haven't even figured out what Sigma types need to look like for RDP yet. Maybe the combined requirements will be clarifying.

 

But there is nothing preventing developers from creating systems that input left and output right. It just takes a simple mirroring operation:

     backbeatWithTwist = [mirror] second backbeat

At this point, we could input `right ()` and output `1 / left ()`, no problem.

I realize you're talking about an RDP interpretation, but just to be clear about the paper's interpretation: If we try to invoke that program with an input value of ((1 / left ()), left ()), we'll get nondeterministic failure.

What would be non-deterministic about that failure?

The program would nondeterministically choose among 0 possible futures for the computation.

Depending on how we run the nondeterministic machine, we could get different results: A greedy search could immediately give up. A backtracking search could backtrack. A concurrent search could terminate a thread. A time-travel-enabled machine could prevent itself from taking that path in the first place.

Fractionals I understand much better - they're concrete, tangible, just running against the stream.

I suppose you and I at least have a common understanding for continuous-time fractional types now, so I'll understand what you're talking about when you use them. ^_^

I still suspect the closest existing theory for this is the self-dual operator sometimes studied with the Calculus of Constructions. I still haven't taken the time to look and make sure. If it doesn't have a beat-backbeat temporal loop, it might be some other idea entirely. :)

Display logic has the beat-backbeat loop, but it's probably not as close a connection. We would either need to change its structural operator to a formula operator, or introduce new structural operators that take the role of our sums and products (basically building the structural operators of the Calculus of Constructions all over again).

Warm Regards,

Ross

[David Barbour]

On Fri, Aug 23, 2013 at 12:34 AM, Ross Angle <rok...@gmail.com> wrote:

Well, I imagine you're not actually thinking of using AttachableHoses. You're thinking the Static layer would perform an *effectful* transformation from Face to Face, where the effect is to generate an appropriately typed run time behavior. For instance, you can use (>>>) or (***) or (+++) to compose two Static-layer computations, and the resulting dynamic behavior will automatically represent the corresponding (>>>) or (***) or (+++) composition on the run time network. But (+++) composition is an odd case here: For the run time network it represents two mutually exclusive paths, but for the Static-layer computations it represents a parallel transformation of both sides of a FaceSum (just like (***) acts on both sides of a FaceProduct). In this way, you really do "flow down BOTH branches of (x + y)."

This is pretty interesting stuff. I keep wondering how to represent staged programming in a way that's more seamless with normal programming, and I think this is it. If we extrapolate from your two-stage model, I think we'll arrive at a wonderfully elegant stage-indexed family of sum operators. :)

Your comprehension now looks good to me. I hadn't thought about creating an 'elegant stage-indexed family of sum operators' though. :)

 

I'd like to make sure we can extrapolate this into a stage-indexed family of Sigma types. That'll be interesting to think about, since I haven't even figured out what Sigma types need to look like for RDP yet. 

I assume by 'sigma types' you mean taking some subset of a family of types? E.g. 'signal of integral numbers between 12 and 14000'? Yeah, I don't know how to address those in a stage-indexed way either, nor even how to represent them except using the more traditional static approaches. If you figure this out, let me know. :)

Warm Regards,

Dave

[Ross Angle]

A Sigma type can be used for that purpose, and I've done so in these discussions (even going so far as to use "SuchThat" as the notation). A Sigma type is an indexed sum, and its values let you extract two pieces of information:

- Which branch of the sum you're seeing (the index).
- The content of that branch.

The second value's *type* can depend on the first *value*.

Sigma types are a close counterpart to Pi types, which are indexed products.

The question I've been pondering is, where does the index signal live? For an RDP (Atom hither t () + Atom yonder t ()) signal, the index information is sometimes hither and sometimes yonder, but it's never available in both places.

I've come up with an answer. We can have some signals which supposedly represent run time information, but which don't actually live in any partition at run time. Instead these are abstract global statements about the run time phenomena, which are useless at run time but useful for a dependent typechecker. We can represent (a + b) as (Sigma (x : OmniBool) ~ if x then a else b), and sometimes we can use normal signals in the index type too (or instead): (Sigma (x : Atom elsewhere t Boolean) ~ if x then a else b).

Note that I'm not using a tacit syntax here--the x is a variable that holds a signal--but I've done some sketching that makes me think it isn't hard to avoid this.

For multi-stage programming, every Atom and OmniBool would be marked with a stage. An OmniBool is not a static signal; its stage is the same as its fellow Atoms. If you have a value of a Sigma type, there will be two ways to decompose it:

a) Given a stage, get the incomplete index. This will be a value that's partially uninformative because future stages haven't been decided yet.
b) Given a stage and an index completion, get the projection. An index completion represents whatever information could possibly fill in the gaps of the incomplete index.

In the one-stage case, this collapses back to the usual Sigma semantics: We always "give" the same stage, and there's never any incompleteness since there are no future stages to shroud in mystery.

In the two-stage case, for binary sums, this collapses to your static choice operator:

a1) Given stage 1, get a useless unit value.
a2) Given stage 2, get a boolean index representing which branch you're seeing.
a1) Given stage 1 and a boolean, get whichever branch will correspond to that.
a2) Given stage 2 and a useless unit value, get the branch you're on.

The full generality of this operator would be tough to implement. I would want to use a technique based on "Observational Equality, Now!" to formalize the incomplete indexes and index completions in terms of the things they could potentially be equal to. However, I'm afraid that will be very cumbersome to work with, much like my extensible-sums-based approach to the expression problem in Era.

Hmm... extensible staged sums. :) I suppose that'll be my next step into the abyss. :-p

-Ross

[Ross Angle]

On Mon, Aug 26, 2013 at 8:21 PM, Ross Angle <rok...@gmail.com> wrote:

Note that I'm not using a tacit syntax here--the x is a variable that holds a signal--but I've done some sketching that makes me think it isn't hard to avoid this.

Last night I put my sketch here:

https://github.com/rocketnia/underreact/blob/gh-pages/notes/reactive-staging.txt

Instead of just using (_ : _) type judgments, I'm also using judgments (_ : _ -> _) where the arrow is baked into the judgment syntax. On top of that, I'm using a judgment (_ : _ -> #type) to represent value-to-type transformations, as needed for the dependent result type of a Sigma or Pi. (I don't have #type as its own type.)

In order to support Sigmas inside of Sigmas, I actually define Sigma in the form of a (_ : _ -> #type) operator. Instead of writing (x + y) as (Sigma (b : OmniBool) -> if b then x else y), I write it this way:

(#invoke

  (#typeSigma (#procureType (#bool s))

    (#if s (#procureType x) (#procureType y)))

  1

  1)

The #procureType operator takes a type expression and turns it into a (1 -> #type) arrow. The #invoke operator takes a (_ -> #type) arrow and turns it back into a type expression. I think we need type expressions sometimes, because we're using judgment syntaxes like (_ : _ -> _) where some of the blanks are type expressions.

On the other hand, maybe we don't need type expressions, just (1 -> #type) expressions. Then perhaps we could write this:

(#typeSigma (#bool s) (#if s x y))

Oh my gosh....

By the way, the `s` in the above is my stage annotation. (The notation (#if s x y) is not something that branches on `s`; it's actually a ((#bool s * a) -> #type) arrow.)  At this point I'm just making the simplifying assumption that all stages are drawn from a predetermined set of constants, so that I don't need (_ -> #stage) arrows.

Warm Regards,

Ross

[David Barbour]

On Mon, Aug 26, 2013 at 8:21 PM, Ross Angle <rok...@gmail.com> wrote:

The question I've been pondering is, where does the index signal live? For an RDP (Atom hither t () + Atom yonder t ()) signal, the index information is sometimes hither and sometimes yonder, but it's never available in both places.

I've come up with an answer. We can have some signals which supposedly represent run time information, but which don't actually live in any partition at run time. Instead these are abstract global statements about the run time phenomena, which are useless at run time but useful for a dependent typechecker.

In early implementation efforts, I attempted to carry something like the 'OmniBool' index signal at runtime different sums. But I had terrible trouble dealing with assocl+.

    assocl+ :: (a + (b + c)) ~> ((a + b) + c)

Well, I could deal with it, but it required a lot of masks and merges, and there wasn't a clear partition for it (given that splits can occur in different partitions). I ultimately gave up tracking it. 

From a typechecking perspective, however, I can understand how conceiving of this abstract OmniBool signal might be useful. 

I'm still trying to absorb most of what you're saying, so I'll get back to you later.

[David Barbour]

On Mon, Aug 26, 2013 at 8:21 PM, Ross Angle <rok...@gmail.com> wrote:

We can represent (a + b) as (Sigma (x : OmniBool) ~ if x then a else b), and sometimes we can use normal signals in the index type too (or instead): (Sigma (x : Atom elsewhere t Boolean) ~ if x then a else b).

Note that I'm not using a tacit syntax here--the x is a variable that holds a signal--but I've done some sketching that makes me think it isn't hard to avoid this.

For tacit representation of behavior types, the best I've come up with is behaviors that transform typereps... which are modeled as static values in the type system. I haven't figured out why, but I don't really find this satisfying. Let me know if you have any other ideas. :)

In the two-stage case, for binary sums, this collapses to your static choice operator:

a1) Given stage 1, get a useless unit value.
a2) Given stage 2, get a boolean index representing which branch you're seeing.

b1) Given stage 1 and a boolean, get whichever branch will correspond to that.
b2) Given stage 2 and a useless unit value, get the branch you're on.

The full generality of this operator would be tough to implement.

I'm not sure it could be implemented in a concrete way. In which partition would be the observer? I suppose you're talking about the abstract implementation?

Last night I put my sketch here:
https://github.com/rocketnia/underreact/blob/gh-pages/notes/reactive-staging.txt

I've been trying to get a handle on this, but I'm having some difficulty following the significance of each stage constraint. I think I got lost starting at #procureDeadAtom. Some extra inline documentation might help.

maybe we don't need type expressions, just (1 -> #type) expressions. Then perhaps we could write this:
(#typeSigma (#bool s) (#if s x y))
Oh my gosh....

That could simplify things a little. :)

Warm Regards,

Dave

[Ross Angle]

On Tue, Aug 27, 2013 at 5:32 PM, David Barbour <dmba...@gmail.com> wrote:

On Mon, Aug 26, 2013 at 8:21 PM, Ross Angle <rok...@gmail.com> wrote:

We can represent (a + b) as (Sigma (x : OmniBool) ~ if x then a else b), and sometimes we can use normal signals in the index type too (or instead): (Sigma (x : Atom elsewhere t Boolean) ~ if x then a else b).

Note that I'm not using a tacit syntax here--the x is a variable that holds a signal--but I've done some sketching that makes me think it isn't hard to avoid this.

For tacit representation of behavior types, the best I've come up with is behaviors that transform typereps... which are modeled as static values in the type system. I haven't figured out why, but I don't really find this satisfying. Let me know if you have any other ideas. :)

It sounds like you're not talking about the same problem as I am. Those typereps are themselves shaped like expressions, right? Sigma type expressions typically have local variables, so the use of typereps doesn't mean you're avoiding variables overall.

Incidentally, could you describe the primary reasons you're pursuing tacit programming rather than programming with variables? I could make some guesses, but I don't want to put words in your mouth. :)

In the two-stage case, for binary sums, this collapses to your static choice operator:

a1) Given stage 1, get a useless unit value.
a2) Given stage 2, get a boolean index representing which branch you're seeing.
b1) Given stage 1 and a boolean, get whichever branch will correspond to that.
b2) Given stage 2 and a useless unit value, get the branch you're on.

The full generality of this operator would be tough to implement.

I'm not sure it could be implemented in a concrete way. In which partition would be the observer? I suppose you're talking about the abstract implementation?

Whoops, to begin with, those rules I gave were actually for an (x + y) choice, not "your static choice operator" as I had described.

You're asking about partitions. The way I'm thinking about this, whenever we have a pair of stages where one precedes the other, the later stage lives in a particular partition of the earlier one. Say partition p2 lives in partition p1 of stage s1. When we perform operations in stage s2, there's a side effect at stage s1, which is to generate program code that's observable by partition p1. I'm not quite sure what it would look like to extract this generated code, but I'll make a guess toward the end of this email after I've introduced some other notation. (Look for "getSourceCode.")

I'm going to try giving specific examples of these rules again, but this time I'll be much more specific about the stage and partition of each piece of data. I'll use the notation (Atom s p Bool) for a boolean at stage `s` and partition `p`, and I'll use the notation (Omni s Bool) for a boolean at stage `s` in no partition. (For a traditional RDP signal, this partition is a (spatial partition, time offset) pair. For Static signals, it might be a beat index instead.)

For the main example, the branch will occur in the middle stage of a 3-stage hierarchy, so we can see both the relatively static and relatively dynamic ramifications at the same time. Stage s3 lives in partition p2 of stage s2. Stage s2 lives in partition p1 of stage s1. We're going to branch on a boolean in stage s2.

Index -- Get an (Omni s2 Bool).

Projection at s1 -- Given an (Omni s1 Bool), get the s1 parts of the branch. (This input is our prediction of (Omni s2 Bool).)

Projection at s2 -- Get the s2 parts of the branch.

Projection at s3 -- Get the s3 parts of the branch.

Now let's change this up with one more example, an eight-legged branch operator whose index type is (Atom s1 p1 Bool * Atom s2 p2 Bool * Atom s3 p3 Bool).

Index -- Get an (Atom s1 p1 Bool * Atom s2 p2 Bool * Atom s3 p3 Bool).

Projection at s1 -- Given an (Omni s1 Bool * Omni s1 Bool), get the s1 parts of the branch. (This input is our prediction of (Atom s2 p2 Bool * Atom s3 p3 Bool).)

Projection at s2 -- Given an (Omni s2 Bool), get the s2 parts of the branch. (This input is our prediction of (Atom s3 p3 Bool).)

Projection at s3 -- Get the s3 parts of the branch.

(When I was being vague about the stage of each value, I wrote multiple cases for the index rule. Now it's just one rule that works for all stages at one.)

I'd really like to see if there's a good semantics for stage ranges, not just for individual stages:

Index -- Get an (Omni s2 Bool).

Projection at s1 -- Given an (Omni s1 Bool), get the s1 parts of the branch.

Projection at s2..s3 -- Get the s2 and s3 parts of the branch.

This way we could manage multi-stage signals without them getting sliced up into stage-specific parts all the time.

To achieve this, I'm thinking of formalizing "the _ parts of the branch" in a particular way:

Index -- Get an (Omni s2 Bool).

Projection at s1 -- Given an (Omni s1 Bool), get the entire branch. We cannot use this operation unless we promise our computation becomes dead code after stage s1.

Projection at s2 -- Get the entire branch. We cannot use this operation unless we promise our computation becomes dead code after stage s2.

Projection at s3 -- Get the entire branch. We cannot use this operation unless we promise our computation becomes dead code after stage s3 (which is trivial if we only have these three stages).

This way there's no need for "Projection at s2..s3," and for that matter there's no need for "Projection at s2." Both of these are covered as specific use cases of "Projection at s3."

In my sketch I use the judgment (b : x -> {s1..s2} y) to signify that a behavior begins doing things in stage s1 and becomes dead code after stage s2. At this point I'm not sure there's actually a reason to track the first stage, but I was thinking it might come in handy either for contravariant occurrences of the dead code constraint, or as a way to simplify the multiple projection rules into one, or (come to think of it) as a way to harness the code generation side effect:

getSourceCode :

  (a -> {s2..s3} b)

  -> {s1..s1}

  (Atom s1 p1 (a -> {s2..s3} b))

Given an abstraction which *only* does things in stages *following* s1, we can get its source code at stage s1.

This is the first time I've thought about how to formulate this getSourceCode operation, and at this point my number one concern is that it might not make sense with closures. How could we get the source code of the encapsulated signal?

Last night I put my sketch here:
https://github.com/rocketnia/underreact/blob/gh-pages/notes/reactive-staging.txt

I've been trying to get a handle on this, but I'm having some difficulty following the significance of each stage constraint. I think I got lost starting at #procureDeadAtom. Some extra inline documentation might help.

Yeah, sorry, it was mainly just a sketch. :) I did add a little documentation when I published it so that it wouldn't be entirely gibberish, but it's so buggy and incomplete that I can hardly look at it without wanting to make drastic changes.

Now that I've written this email, I think I might be ready to make some of those drastic changes. For posterity, the link above originally pointed to this version (and still does, for now): https://github.com/rocketnia/underreact/blob/810d0b5478cd3492412c0ed1dd0f20ef90b72e1d/notes/reactive-staging.txt.

Warm Regards,

Ross

[David Barbour]

On Sat, Aug 31, 2013 at 3:57 PM, Ross Angle <rok...@gmail.com> wrote:

 Sigma type expressions typically have local variables, so the use of typereps doesn't mean you're avoiding variables overall.

True. I've been thinking a bit about how to model 'local variables' for tracking this sort of dependent type analysis (in an environment like Awelon's, which lacks scope, and RDP, which lacks identity). Best I can come up with is to maintain an affine typed uniqueness-source in the environment as a name generator, and to somehow bind proof elements to each signal. 

could you describe the primary reasons you're pursuing tacit programming rather than programming with variables?

I put this in another e-mail. 

 

You're asking about partitions. The way I'm thinking about this, whenever we have a pair of stages where one precedes the other, the later stage lives in a particular partition of the earlier one. Say partition p2 lives in partition p1 of stage s1. When we perform operations in stage s2, there's a side effect at stage s1, which is to generate program code that's observable by partition p1.

I'm interpreting this as: Omni is only observed by the compiler or typechecker, which happens somewhere. 

Projection at s1 -- Given an (Omni s1 Bool * Omni s1 Bool), get the s1 parts of the branch. (This input is our prediction of (Atom s2 p2 Bool * Atom s3 p3 Bool).)

We're making a prediction in s1 about the future states in s2 and s3. What happens when we predict wrongly? 

(I apologize for being unable to follow about 80% of your last e-mail. I really should do a course in dependent typing. I should have time for one next year.)

my number one concern is that it might not make sense with closures. 

How could we get the source code of the encapsulated signal?

What do you mean the 'source code' of a signal?

One way to model closures is a static behavior coupled with a record of signals - a "poor man's closure". If we're feeling insecure about this, we could make the coupling tight using either a sealer/unsealer pair or a dedicated primitive (we don't really need identity for a closure). 

The only source-code associated with such signals would be the data plumbing.

Hmm. I wonder if I should provide primitive support for this pattern. Maybe something like:

      capture :: ((x*y)~>z)*x ~> (y~>z)

But I kind of like how my poor-man's closure keeps everything visible in the type system; makes it a lot easier to understand the limits and security implications. I'll need to reconsider adding this primitive much later, after everything else is working. 

 

Now that I've written this email, I think I might be ready to make some of those drastic changes. For posterity, the link above originally pointed to this version (and still does, for now): https://github.com/rocketnia/underreact/blob/810d0b5478cd3492412c0ed1dd0f20ef90b72e1d/notes/reactive-staging.txt.

I'll take another look later, then. 

Warm Regards,

Dave

[Ross Angle]

On Sat, Aug 31, 2013 at 9:44 PM, David Barbour <dmba...@gmail.com> wrote:

On Sat, Aug 31, 2013 at 3:57 PM, Ross Angle <rok...@gmail.com> wrote:

 Sigma type expressions typically have local variables, so the use of typereps doesn't mean you're avoiding variables overall.

True. I've been thinking a bit about how to model 'local variables' for tracking this sort of dependent type analysis (in an environment like Awelon's, which lacks scope, and RDP, which lacks identity). Best I can come up with is to maintain an affine typed uniqueness-source in the environment as a name generator, and to somehow bind proof elements to each signal. 

My point was that typereps don't necessarily remove the need for variables (once we have higher-order type constructors like Sigma), but these (_ : _ -> _) typing judgments do. Hopefully I can explain this better at some point. :)

could you describe the primary reasons you're pursuing tacit programming rather than programming with variables?

I put this in another e-mail. 

 

You're asking about partitions. The way I'm thinking about this, whenever we have a pair of stages where one precedes the other, the later stage lives in a particular partition of the earlier one. Say partition p2 lives in partition p1 of stage s1. When we perform operations in stage s2, there's a side effect at stage s1, which is to generate program code that's observable by partition p1.

I'm interpreting this as: Omni is only observed by the compiler or typechecker, which happens somewhere. 

Hmm, I'm not sure if that fits what I'm saying or not.

In the system I'm describing, typechecking occurs before all stages, and it ensures that every single stage will be type-correct. Think of it like this: I'm not talking about generating program code as flat text which might have syntax errors, and I'm not talking about generating programs with type errors either.

An (Omni s x) signal cannot be observed in any partition of stage `s`. Before that stage, its *true* value has not yet been determined. Nevertheless, when we do static analysis on that program (e.g. during dependent typechecking), we can observe its *hypothetical* values.

Projection at s1 -- Given an (Omni s1 Bool * Omni s1 Bool), get the s1 parts of the branch. (This input is our prediction of (Atom s2 p2 Bool * Atom s3 p3 Bool).)

We're making a prediction in s1 about the future states in s2 and s3. What happens when we predict wrongly? 

There's no way to "predict wrongly." This is the cornerstone of the model, where I'm generalizing your idea that static signals flow over both branches of a dynamic sum. :)

In the branches of this sum, the s3 signals only flow over one branch of this eight-branch operator. The s2 signals flow over two. The s1 signals flow over four. When we want to get the s1 signals out of one branch of this sum, we have to choose between four branches, and we express this chioce as an (Omni s1 Bool * Omni s1 Bool).

my number one concern is that it might not make sense with closures. 

How could we get the source code of the encapsulated signal?

What do you mean the 'source code' of a signal?

If a signal carries a first-class program (e.g. a behavior), there may or may not be a serialized representation of that program. That's what I mean by its source code.

I can't say my terminology is perfect here. This might not be *source* code in the sense of being a starting point of some transformation process. I just didn't want to say something as ambiguous as "getCode," so I went with "getSourceCode."

A getSourceCode operator would take an isolated stage s2 subprogram and make its source code available as a first-class value in stage s1. These days, many multi-stage programs accomplish this kind of first-class access by using quasiquotation and bytecode generation and such, but the approach I'm describing would make it possible to achieve the same end results while using a more seamless programming style.

Looking at it another way, getSourceCode is a way to wrap an impure computation under a pure interface. If one of these multi-stage computations does something in stage s3, really it has a side effect in stage s2 to generate code for stage s3, and a side effect in stage s1 to generate this side-effectful code for stage s2. The use of getSourceCode lets us treat these generated programs as proper return values.

For the two-stage case you originally described (static and dynamic), we don't really need getSourceCode. Our entire static stage generates a single program for the dynamic stage. We compile a program and then (at some point) execute it, with no programmable steps in between.

On the other hand, you represent dynamic behaviors as typed atoms. I think source code representations would have pretty much exactly the same type, and I think some of the same operations and implementations would apply to both. Underreact lacks dynamic behaviors, and I think this might be a great way to approach them.

One way to model closures is a static behavior coupled with a record of signals - a "poor man's closure". If we're feeling insecure about this, we could make the coupling tight using either a sealer/unsealer pair or a dedicated primitive (we don't really need identity for a closure). 

The only source-code associated with such signals would be the data plumbing.

Hmm. I wonder if I should provide primitive support for this pattern. Maybe something like:

      capture :: ((x*y)~>z)*x ~> (y~>z)

But I kind of like how my poor-man's closure keeps everything visible in the type system; makes it a lot easier to understand the limits and security implications. I'll need to reconsider adding this primitive much later, after everything else is working. 

That `capture` operator is pretty much identical to Underreact's `bclosure`, but they're very different in terms of implementation. I would say `bclosure` avoids the negative "limits and security implications" of `capture`, but actually I recommend sticking with poor-man's closures for now.

Underreact's first-class behaviors are erased before run time; their computation happens earlier than that, in the form of inlining. This makes it possible to model closures, because the compiler runs as a closed system when it does this inlining, so it can just neglect to provide any way to break encapsulation.

When you first talked about the (Static x) signal types, I thought you just needed to mark which information lived at this inlining step. It's interesting that you're encountering a desire to have closures at the static level, but it makes complete sense because you're trying to have open-system composition at that level too.

Even in the generalized multi-stage system, I imagine we'd do typechecking, then do inlining of functions, and only then start running the stage(s). This is no help, unless you find it satisfying to have *arbitrarily many* open-system metaprogramming stages preceded by a single closed-sytem inlining phase. Just how much openness do you need, anyway? :-p

A real solution would probably involve some kind of cryptography so as to distribute data and capabilities into the outside world while keeping them encapsulated. Are you implying this with the sealer/unsealer pairs you mentioned, or would those work by some other mechanism?

---

This topic makes me want to mention something slightly related. The multi-stage programming model would potentially support function types as a concept *derived* from staged Sigmas:

• Function types...
• Are a special case of dependent function types (Pi types),
• Which are indexed product types (the function parameter is the index),
• Which we can model as a special case of these staged indexed sum types (staged Sigma types): The function parameter is now the index completion, and the real index needs to live at some future stage. To talk about this real index type, it could be convenient to have a consistent transformation from parameter types like (Atom s p Bool) into types they could be completions of, like (FarFutureOmni Bool).
  

In order to model functions with extra side effects (e.g. RDP behaviors), I might want Sigma types to support those side effects when a branch is accessed. Not sure how to formalize this yet, and I think it would make things even more confusing at the moment. :-p

 

 

Now that I've written this email, I think I might be ready to make some of those drastic changes. For posterity, the link above originally pointed to this version (and still does, for now): https://github.com/rocketnia/underreact/blob/810d0b5478cd3492412c0ed1dd0f20ef90b72e1d/notes/reactive-staging.txt.

I'll take another look later, then. 

Still haven't gotten around to it. :) Last weekend was my dad's birthday, and then the "Mighty No. 9" Kickstarter sapped all my attention. (Can't wait to see where that goes....)

Warm Regards,

Ross

[David Barbour]

I can't say I understand all the dependent type stuff. Hopefully I'll have an a-ha moment at some point. :) 

I'll move on to the stuff I do understand. Hope you don't mind.

On Sat, Sep 7, 2013 at 6:11 PM, Ross Angle <rok...@gmail.com> wrote:

What do you mean the 'source code' of a signal?

For the two-stage case you originally described (static and dynamic), we don't really need getSourceCode. Our entire static stage generates a single program for the dynamic stage. We compile a program and then (at some point) execute it, with no programmable steps in between.

On the other hand, you represent dynamic behaviors as typed atoms. I think source code representations would have pretty much exactly the same type, and I think some of the same operations and implementations would apply to both. Underreact lacks dynamic behaviors, and I think this might be a great way to approach them.

I tend to think of 'staging' this way: there is a static stage, then there is a dynamic stage. But, there are some dynamic behaviors, and they can have their static stage at runtime. An issue with my way of thinking about it is that I cannot guarantee type-safety for dynamic behaviors until I've expanded them, and expanding them is (for Awelon) a Turing complete computation. Though I can think of ways to address this, none of them are very elegant.

You seem to be thinking more in terms of a multi-stage static computation, perhaps with later stages getting close to a dynamic configuration that will somehow snap safely into place. Personally, I'll need to take your word for it that such a thing is even plausible. Well, yours and Oleg's and Adam Chlipala's and Matt McClelland's. ;)

But I have this nagging fear. 

My main motivations for dynamic behavior haven't changed since I described it a couple years ago: hot-pluggable extensibility, interacting with lazy or incremental systems, brokering connections or smart-networks, optional control capabilities for mutable views, a form of linking to ad-hoc resources in a dynamic environment. The common factor in all these cases is that the dynamic behavior depends not only on runtime inputs, but runtime source-code from sources that you might not even know about statically. 

My fear is this: we will build a powerful, dependently typed framework around everything. And it will be good for those cases where we might want dynamic behaviors based on runtime inputs. But that pattern won't really fit the motivating use-cases for dynamic behavior, so the best we'll accomplish is modeling some type-safe interpreters and compilers for ad-hoc remote source code. And while that might be cool (providing a smaller trusted base) it won't really be useful.

OTOH, perhaps I'm underestimating the number of use-cases for dynamic behaviors based on observing runtime values and building the code locally.

It's interesting that you're encountering a desire to have closures at the static level, but it makes complete sense because you're trying to have open-system composition at that level too.

Well, that's part of it. But I think the tipping point was when I realized I can provide static signal inputs to a dynamic behavior, i.e. like configuration variables. I imagine this could make high-performance dynamic behaviors quite feasible.   

 

A real solution would probably involve some kind of cryptography so as to distribute data and capabilities into the outside world while keeping them encapsulated. Are you implying this with the sealer/unsealer pairs you mentioned, or would those work by some other mechanism?

Awelon's sealer/unsealer pairs currently are only good for static computations. If I figure out how to 'serialize' a sealed value for partition crossing (without unsealing it first) perhaps I'll address cryptography then. :)

Capabilities could be modeled by encrypting code or by using a GUID to represent stored code. It might also be interesting if capabilities can encapsulate some signals. I'm still thinking on how to best model them in Awelon. What I have decided is that some partitions will provide ambient authority, and that ambient authority partitions will typically have an associated 'sandbox' partition that can only manipulate the ambient partition with an associated capability. I'm doing this mostly because ambient authority is a better fit for the AVM and compiler.

 

This topic makes me want to mention something slightly related. The multi-stage programming model would potentially support function types as a concept *derived* from staged Sigmas:

x_X  brains exploding

 

Still haven't gotten around to it. :) Last weekend was my dad's birthday, and then the "Mighty No. 9" Kickstarter sapped all my attention. (Can't wait to see where that goes....)

Mighty 9 looks nice. An obvious Mega Man clone. Though, I guess when you've got one of the original Mega Man lead developers... maybe it doesn't count as a clone.

I'll look into picking it up if it gets a PS3 release. :)

Warm  Regards and Exploded Brain Matter,

Dave

[Ross Angle]

On Sat, Sep 7, 2013 at 7:36 PM, David Barbour <dmba...@gmail.com> wrote:

I can't say I understand all the dependent type stuff. Hopefully I'll have an a-ha moment at some point. :) 

I'll move on to the stuff I do understand. Hope you don't mind.

Well,  some of the other topics you're bringing up are tangled up in dependent types, so I'm sorry in advance. ^_^;

On Sat, Sep 7, 2013 at 6:11 PM, Ross Angle <rok...@gmail.com> wrote:

What do you mean the 'source code' of a signal?

For the two-stage case you originally described (static and dynamic), we don't really need getSourceCode. Our entire static stage generates a single program for the dynamic stage. We compile a program and then (at some point) execute it, with no programmable steps in between.

On the other hand, you represent dynamic behaviors as typed atoms. I think source code representations would have pretty much exactly the same type, and I think some of the same operations and implementations would apply to both. Underreact lacks dynamic behaviors, and I think this might be a great way to approach them.

I tend to think of 'staging' this way: there is a static stage, then there is a dynamic stage. But, there are some dynamic behaviors, and they can have their static stage at runtime.

Oh, "static stage at runtime." So you'd alternate between a layer of continuous reactive side effects and a layer of code generation side effects. This seems a bit arbitrary to me, but it's also a reasonable-looking choice to make.

You seem to be thinking more in terms of a multi-stage static computation, perhaps with later stages getting close to a dynamic configuration that will somehow snap safely into place.

So far, for example purposes, I've only talked about total orderings of stages (e.g. the obvious total ordering between stages named "s1," "s2," and "s3") because that's already an interesting enough case to be challenging to design or explain.

In general, I expect many applications will use stages in a *partial* ordering, and the meat of the application will be somewhere in the middle:

Composition and link time program logic

 |

Run time program logic (the meat of the application)

 / | \

Dynamically generated code for storage or distribution

The run time stage uses worker sub-stages to manage specific tasks. To distribute or store a program, we pretend to do that computation inside its own sub-stage, and then we bundle up our actions (getSourceCode) and send them off to another partition or external resource.

Now let's shift to an external program's point of view: We have a well-typed interface of our own, and we receive a typed source code value over that interface. Thus, it must be the type we expected, and we can straightforwardly eval it.

(What I'm talking about here is interpreting code that already has a known type. I'll get to untyped code, like a raw text or binary representation, in just a second.)

Personally, I'll need to take your word for it that such a thing is even plausible. Well, yours and Oleg's and Adam Chlipala's and Matt McClelland's. ;)

But I have this nagging fear. 

My main motivations for dynamic behavior haven't changed since I described it a couple years ago: hot-pluggable extensibility, interacting with lazy or incremental systems, brokering connections or smart-networks, optional control capabilities for mutable views, a form of linking to ad-hoc resources in a dynamic environment. The common factor in all these cases is that the dynamic behavior depends not only on runtime inputs, but runtime source-code from sources that you might not even know about statically. 

My fear is this: we will build a powerful, dependently typed framework around everything. And it will be good for those cases where we might want dynamic behaviors based on runtime inputs. But that pattern won't really fit the motivating use-cases for dynamic behavior, so the best we'll accomplish is modeling some type-safe interpreters and compilers for ad-hoc remote source code. And while that might be cool (providing a smaller trusted base) it won't really be useful.

It sounds like you're worried these interpreters and compilers won't have the full expressive power of the original language. Sure, a self-interpreter will pose steep logical challenges if we want to model it as a pure and total function, but we could start smaller.

An interpreter for untyped code will have to deal with at least as many issues as an interpreter for typed code. Namely, both kinds of interpretation need to avoid instantaneous feedback loops through external resources. We might be able to address this with some explicit delay and/or a system of "tainted" types.

To interpret untyped code (e.g. text), we'll additionally need to be tolerant of parse errors and/or type errors (which is easy; just return an Either), and we'll need some way to avoid the kinds of paradoxes that could arise from self-interpretation (e.g. Tarski's undefinability theorem and Gödel's theorems). I think we can cast out these paradoxes by modeling the self-interpreter as though it might not terminate (...even if it does always terminate in practice, as with Matt M's technique). What do you think of sending a self-interpretation request to an external resource and waiting for it to come back with a result?

OTOH, perhaps I'm underestimating the number of use-cases for dynamic behaviors based on observing runtime values and building the code locally.

I'm not sure if this is what you're pondering about, but... since Underreact doesn't have dynamic behaviors yet, it doesn't have any way to expand and retract the reactive node graph at run time. If programmers need to manage this kind of thing to optimize their resource usage, dynamic behaviors might come in handy for this purpose, even inside of a single codebase.

Other than that, yeah, I think dynamic behaviors would mainly be useful at API boundaries.

It's interesting that you're encountering a desire to have closures at the static level, but it makes complete sense because you're trying to have open-system composition at that level too.

Well, that's part of it. But I think the tipping point was when I realized I can provide static signal inputs to a dynamic behavior, i.e. like configuration variables. I imagine this could make high-performance dynamic behaviors quite feasible.   

Which of these type signatures is closest to what you mean by "provide static signal inputs to a dynamic behavior"?

• Use (Dyn (Code (Sta x ~~> y))) and (Dyn x) to get `y`.
  
• Use (Dyn (Code (Sta x ~~> y))) and (Sta x) to get `y`.
• Use (Sta (Code (Sta x ~~> y))) and (Sta x) to get `y`.

For the sake of making the above options clearer, I'm using some specialized notation for this question:

• The notation "Dyn x" means "an `x` signal at the run time stage (at a partition and time offset that don't matter for this example)."
  
• The notation "Sta x" means "an `x` signal at the compile time stage (at a beat index that doesn't matter for this example)."
  
• The notation "Code (x ~~> y)" means "a serializable first-class behavior from `x` to `y`."

 

A real solution would probably involve some kind of cryptography so as to distribute data and capabilities into the outside world while keeping them encapsulated. Are you implying this with the sealer/unsealer pairs you mentioned, or would those work by some other mechanism?

Awelon's sealer/unsealer pairs currently are only good for static computations. If I figure out how to 'serialize' a sealed value for partition crossing (without unsealing it first) perhaps I'll address cryptography then. :)

Sounds more like the converse to me. If we ever have a satisfactory way to serialize a sealed value, that's probably because we're using some kind of cryptography.

Capabilities could be modeled by encrypting code or by using a GUID to represent stored code. It might also be interesting if capabilities can encapsulate some signals. I'm still thinking on how to best model them in Awelon. What I have decided is that some partitions will provide ambient authority, and that ambient authority partitions will typically have an associated 'sandbox' partition that can only manipulate the ambient partition with an associated capability. I'm doing this mostly because ambient authority is a better fit for the AVM and compiler.

You reversed this decision in the "Capability Security in Awelon" thread, so I guess I won't comment on this. :)

 

Still haven't gotten around to it. :) Last weekend was my dad's birthday, and then the "Mighty No. 9" Kickstarter sapped all my attention. (Can't wait to see where that goes....)

Mighty 9 looks nice. An obvious Mega Man clone. Though, I guess when you've got one of the original Mega Man lead developers... maybe it doesn't count as a clone.

I'll look into picking it up if it gets a PS3 release. :)

It's not up to the PS3 / 360 / Wii U stretch goal quite yet, but at this rate it'll get there sometime in the next couple of days. As for me, I think I'll be just fine with Windows and Linux versions. :)

-Ross