Куклев пишет на фесбуке про линейную логику

[juan_gandhi]

src

After many years I finally have an intuitive understanding of linear logic operators.

The λλ̃-calculus by V. Choudhury et al. shows how to understand the multiplicative disjunction A ⅋ B, while the Verse calculus by SPJ et al. shows how to understand the multiplicative exponential ?A.

A × B — tuple

A ⅋ B — junction (employing terminology by Larry Wall)

A + B — producer-controlled alternative

A & B — consumer-controlled alternative

!A — factory producing A's, in particular

!A = 𝟘 & A & A × A & A × A & ···

?A — junction of any number of A's, in particular

?A = ⊥ + A + A ⅋ A + A ⅋ A ⅋ A + ···

All variables in Verse calculus are secretly of the kind ?T, where T is a cartesian type. So, one can even assume they are ?!X.

Comments

[sassa_nf]

That's one guy with untapped skill of explaining things.

But in this case I don't understand "consumer"/"producer" notion.

[juan_gandhi]

I agree, pretty weird and unexpected. Maybe we should ask him?

I especially enjoyed explanation of ! andc ? via free and cofree(?).

[sassa_nf]

here we go, the answer is: this is linear logic, so A&B is decided whether it is A or B at the time the value is accessed, and A+B - it is decided whether it is A or B at the time it is constructed.

[chaource]

I have a rough heuristic understanding of the "producer/consumer" metaphor. I see it strictly as a metaphor.

Consider this code example:

... some code ...
x :: A + B
x = f(t)

y :: C
y = k(x, m, n)
... more code ...

Here the value x is "produced" by the function call f(t). The value x is "consumed" by the function call k(x, m, n).

The type A + B is the same as the usual intuitionistic type. It means that x must be either Left(...) or Right(...). The decision of whether to return Left(...) or Right(...) is made by the function f. Typically, f will examine its argument (t) and make that decision, or perhaps f will hard-code that decision and always return a Right(...), say.

So, we say metaphorically, the decision is made "by the producer". In this sense, the type A + B is a "producer-controlled alternative". The function k (the consumer) must be able to accept both Left(...) and Right(...). The consumer has no control over what value x is going to be.

Now if we want to understand "consumer-controlled alternative" heuristically, we write a similar code:

... some code ...
x :: A & B
x = f(t)

y :: C
y = k(x, m, n)
... more code ...

The type of x is A & B and it is again either Left (A) or Right (B), but it is not known which one, until the function call k(x, m, n) is run.
The function k is the "consumer". What does it mean that the consumer "controls the alternative"? It means the consumer decides whether it will consume a value Left(...) or a value Right(...). The function call k(x, m, n) might examine its other arguments (m and n) to decide whether to accept x = Left(...) or x = Right(...).

Suppose k(x, m, n) decides to accept x = Right(...). This is a "consumer-controlled alternative", so the producer has no control over the alternative. It means that the function call f(t) must return a value of type Right(...) when k() decides to consume that.

But how does the producer f(t) know that it must return a Right(...)? Our usual intuition is that the function call f(t) is performed "before" the function call k(x, m, n) and so f(t) could not possibly know that k() will make some decisions later about the type of x. But this intuition does not apply to linear-typed languages. Somehow, the compiler of the linear-typed language must implement the feature that information about consumer-controlled choice is propagated back to the producer.

Since A and B are (possibly) linear types, the producer f(t) must produce exactly one of these two. Exactly one will be then consumed by k().

In this way, the linear type A & B must implement a "backpropagation" of information from consumer to producer.

[juan_gandhi]

Sounds reasonable.

[chaource]

A ⅋ B — junction

What is „junction“?

[juan_gandhi]

It's "multiplicative disjunction" in Wikipedia. But you could ask Kuklev.