Arc Forumnew | comments | leaders | submitlogin
1 point by akkartik 4335 days ago | link | parent

Sequel: http://rocketnia.wordpress.com/2012/04/29/a-dataflow-syntax-.... I haven't wrapped my head around it all (are linear variables different from linear types?).

FredBrach was thinking about something similar, decoupling scope declarations from variable declarations (http://arclanguage.org/item?id=16147)



2 points by rocketnia 4325 days ago | link

Whoops, I guess I didn't reply to this.

Yes, part of what FredBrach did with scopes was eerily similar to what I was thinking about at the time. ^_^ I didn't talk about it much in response, but I did consider it promising.

I was also thinking about this topic a couple of days before http://arclanguage.org/item?id=15831, where I wrote "Suppose there were a special form (varscope <var> <...body...>) which scoped (<var> <name> <val>) as a special form in the body, which both defines and assigns to a variable and returns the new value. One can say (var foo foo) to define a variable without modifying it."

I think this kind of generalized scope jives well with a linear system. Linearity is about assuming every value is produced once and consumed once by default. Everyday lambda calculus lets you introduce a variable at the acquisition site and then (nonlinearly) use it any number of times in the body. For the reverse of that, when we're dealing with values we use once but define in any number of places (e.g. for set accumulation or nondeterministic choice), maybe it can make more sense to "introduce" the variable at the usage site.

My blog post's "Aside" expressions cater to many-to-many, zero-to-many, many-to-zero, and zero-to-zero operations, where there's no obvious definition or usage site to single out for the variable introduction.

---

"I haven't wrapped my head around it all (are linear variables different from linear types?)."

Hmm, when I said "linear variable," I just meant a variable with a linear value or a linear type. This kind of variable appears in the code at exactly one definition site and one usage site, unless the code uses conditionals or something.[1]

If you're in the midst of changing your question to "are linear values different from linear types?" the answer is no, I'm talking about the same concept. :) However, it is possible to have dynamically checked linear values in an untyped language. Likewise, I bet it's even possible to have linear typing without linear values, in the sense of fostering a programming subculture which considers the types important and the values unimportant.

If you're in the midst of changing your question again, no, I'm not sure why it's called "linear." :-p But in order to rationalize the name myself, I look at the life story of a single value. For an intuitionistic value, this timeline can split apart across multiple parts of the program at once. A linear value can't typically branch, merge, begin, or end, unless it does so by transferring its content into new linear values. This makes its life story linear.

[1] Conditionals don't even exist in the expression language I described in that blog post, and I expect that'll make it less helpful as a language but easier to implement. :/ I haven't come up with a way to add conditionals yet.

-----