Subscribe: Lambda the Ultimate - Comments
Language: English
Tags:
algebraic effects  algebraic  array  arrays  data  effects  language  linear values  linear  might  problem  types  values  work
Rate this Feed

Feed Details and Statistics
Preview: Lambda the Ultimate - Comments

# Lambda the Ultimate - Comments

Linearity

Tue, 20 Feb 2018 08:15:57 +0000

The problem I have with linearity is how it interacts with generic programming. Take for example a very simple algorithm like "swap". We want swap to take two mutable references to values of the same type and swap them. The problem I have encountered in languages like Rust is that it won't allow two mutable references into the same array, which prevents you writing a simple algorithm like an in place sort using swaps. My view of programming is that algorithms are fundamental, and simple (efficient) algorithms are more valuable than complex or inefficient algorithms. So here linear typing prevents us using the simplest efficient algorithm, which means it is working against the programmer rather than with the programmer. Yes you can work around this by either giving up efficiency or simplicity, but if this happens with every simple algorithm, you will end up with a complex mess. I think there is a complexity budget,that limits the most complex system a programmer can work with, so you need to be very careful to not introduce unnecessary complexity or you reduce the maximum size of program that a programmer can reliably work on. Having established that, the array problem could be a limitation with Rust, and not fundamental to linear types. We could view an array as an index of mutable references, the index being trivially constructed from the range of addresses from the array start to the array end. You can the pass ownership of the whole array by passing a linear reference to the array, and pass individual cells to swap by their 'synthetic' mutable reference. You would of course have to write the sort in a way the type system can confirm the same mutable-cell-reference does not get passed to swap as both arguments.

Overshoot

Mon, 19 Feb 2018 23:57:38 +0000

Well, I shouldn't have said very differently. I was roughly thinking about the difference between having mutability native or expressed through an interface on abstract functions for in-situ updates. Somewhat in a similar vein as the distinction Keaan made between monadic and imperative programming. But when I think about it, I assume that inlining and peephole optimization could take care of a lot of problems.

Linear decomposition of structure

Mon, 19 Feb 2018 21:53:45 +0000

Linear decomposition of structure, whether through techniques like zippers or row-polymorphic records, is a general and natural solution. Arguably, it's the symmetric dual to composing structures with linear elements. Partitioning of arrays is just one instance of this more general solution. That's essentially a zipper on the array type. Perhaps you believe it a "band-aid solution to one particular problem" because I did not show my work, did not explain above how I originally answered that problem. That's understandable. Arrays are popular enough that I've thought about them years ago, and consequently I have an answer available in my memory. But zippers are a concept and solution that can be systematically applied to algebraic data structures. If you've composed a well-behaved data structure with linear values, there is necessarily some way to decompose, access, and modify it linearly.
Using linear types in a functional language to allow for efficient in-situ updates is very different from using them for live time analysis in an imperative language.
For real-time interactive processing, what we need is a model to inject input data and extract required output data in small steps, and a real-time garbage collector. With this much, we can develop real-time systems. The developer needs only to ensure bounds for how much memory the program requires and how much work is performed between input and output. If the bound is smaller than the period between inputs, it can be real-time. Functional vs. imperative program model isn't a significant distinction here. Requests for effects are essentially a vector for output as far as the external real-time system is concerned; it doesn't matter how we express this within the program. The entire issue of paradigm seems irrelevant in this context. And introducing linear values is also nearly insignificant. It only offers greater efficiency of avoiding allocations and garbage collection for a significant portion of the work performed. And it makes working with arrays more tolerable, allowing update in a false "O(1)" instead of a naive O(N), so we might suddenly favor arrays instead of an intmap or whatever. The improved efficiency might indirectly enable live update for edge cases where raw performance was previously almost-sufficient to keep up with high frequency live inputs, but there are no guarantees. I'm curious what you believe is "very different".

Maybe

Mon, 19 Feb 2018 20:35:54 +0000

Yah, but it's still a band-aid solution to one particular problem. And the problem with band-aid solutions is that you don't know what other problem you're going to hit around the corner. Moreover, it also depends on the setting. Using linear types in a functional language to allow for efficient in-situ updates is very different from using them for live time analysis in an imperative language. I am not convinced.

Arrays are a polite fiction

Mon, 19 Feb 2018 19:50:17 +0000

Arrays are a polite fiction anyway. We don't really get "O(1)" update and access because of physical data layout and speed of transfer. If I were asked which is more fundamental - arrays vs. linear values - I'd say the latter. Hence, I attribute these "pains" you describe more to the fiction of flat arrays and random access memory. (An IntMap or finger tree zipper, for comparison, makes structurally clear which fragments are in "near" memory without relying on a hidden cache effect.) Regarding a matrix, partitioning works fine. We split one array, then the next, then operate on the value, according to structure. Swap is awkward because it doesn't generalize nicely (due to need for dummy values of the correct type, and the non-uniform overhead for swapping the dummy value for struct types). Partitioning with a gap generalizes easily. It's essentially zippers for arrays. The only issue is that "zippers for arrays" are a little troublesome to get "right" in a simple static type system when compared to zippers for trees or lists. (It would help a lot if the partition type contained the array size, for example, but that gets us into dependent types.) I've not encountered any difficulty mixing sharable values with linear ones. We can have records with both shared texts and linear components, for example. Can you illustrate the difficulty you're envisioning?

Hansaplast

Mon, 19 Feb 2018 19:26:27 +0000

Sure, there are some solutions to ease the pain of the most obvious problems. But swapping is going to hurt when you've modeled a matrix as a linear array of linear arrays of linear values. The problem becomes worse when mixing linear and shareable resources in a data structure. I am not sure you run into Rice. You're looking at some language inclusion problem, at best that means equivalent to deciding FSM membership, maybe intersection. At worst, you're looking at language inclusion.

linear arrays

Mon, 19 Feb 2018 19:17:13 +0000

My recommendation is to partition and append arrays. A runtime can implement append very efficiently in cases where we know (statically or dynamically) that the components are adjacent in memory. Also, because arrays are usually language primitives, it is reasonable to introduce primitive features to enforce O(1) logical append of adjacent array fragments, and to track "holes" - array fragments consisting of undefined entries. An advantage of partitioning compared to swap-and-modify is that partitions work nicely with fork-join parallelism. We can pass each partition to a separate task, update in place, then logically glue the pieces back together. My own language simply doesn't have arrays as a primitive data type. But I instead optimize some lists to semi-transparently use an array or array-fragment representation, controlling this optimization via annotations. The common list length, access, update, append, fold, scan, etc. functions are transparently replaced by the compiler or interpreter with with equivalent implementations for arrays. Of course, using an intmap or finger tree (or an LSM-tree variant thereof) is also a pretty good option given linear operations on these structures can also feasibly avoid allocations. Having small array fragments near the leaves might support greater efficiency, though.

Linear Array of Linear Values

Mon, 19 Feb 2018 18:17:45 +0000

Uhm. I need to reconstruct the observation from memory but the problem was as I remember a linear array of linear values. Since you can't reference a component two times you're stuck to swapping it out, modifying it, and swapping it back in. Since that can be translated to an in-situ update I imagine that that problem is solvable but hasn't been solved yet. Though it follows the general pattern of 'introduce type system X to solve problem Y to end up with non-trivial problem Z.'

composition of linear values

Mon, 19 Feb 2018 17:56:56 +0000

Can you explain your assertion? In my experience, linear values compose easily enough that I've never considered it a problem. We can use them with normal data structures. We can literally compose two linear functions into a larger linear function. And so on. I grant this: the presence of linear values in a language pervasively influences how we represent data structures and algorithms. Conventional data composition patterns might not be compatible with linear types. For example, for record types, we conventionally we use `foo.x` syntax to access a value at label `x` and discard the remainder of `foo`. However, this is problematic because there might be a `foo.y` property with a relevant or linear type which cannot be discarded. So instead we must (in general) use a linear destructuring of records, e.g. `match rec with {x=myVar | rem} -> body` like row-polymorphic records. For large, recursively structured composites, the Huet Zipper (data structure) has proven very widely applicable for developing algorithms to safely access, update, and process trees or lists that may contain linear values.

But linear values can

Mon, 19 Feb 2018 16:45:27 +0000

But linear values can fulfill this role admirably.
Linear values don't compose.

Algebraic effects

Mon, 19 Feb 2018 08:12:09 +0000

ST, Linearity

Mon, 19 Feb 2018 07:39:38 +0000

In Haskell, that would be in the ST monad. The impurity is encapsulated by runST. This is guaranteed by the type system by cleverly using a `forall` qualifier. The main disadvantage of ST is that we cannot use it to model continuations or generators (and hence concurrency) with impure implementations. This is ensured by the type system, but the fundamental issue is that the capability to "copy" a continuation value is incompatible with ongoing in-place mutation of captured STRefs. ST is only "safe" because we contained it to the linear context of a monad. Another useful technique for efficient in-place mutation in functional programming is to leverage unique references. When we have a unique reference to a value, mutation is not observed. This also allows for "copy on write" approaches when we might have shared references. Linear or affine types can protect uniqueness, but aren't strictly necessary. You have argued that objects should precede values, or at least be on equal footing. I'd call this goal a failure if we have major issues representing a pure interface to impurely implemented continuations. So ST and similar techniques won't work. (I suspect whatever you're envisioning would qualify as a "similar technique" in this regard.) But linear values can fulfill this role admirably. We can understand linear structures as objects in the computation, with spatial and temporal properties, a history and trajectory. We can model conventional object oriented systems by explicitly modeling an address space for message routing (separating concept of object from address). But the default is also interesting in its physical analog: mobile objects that have no fixed address and instead only interact with their local environment.

Algebraic Effects

Mon, 19 Feb 2018 07:12:04 +0000

Algebraic effects seem to be able to do all the things you list as important, without needing a monad as an explicit construct. You could use the argument that Monads are algebraic properties, so something that has the correct properties is still a monad whether you explicitly declare it as such or not (and I myself have made that argument in the past), but it does not require the programmer to understand Monads. The interesting question for me here is, if you have algebraic effects, what else do you need to have a concise self-consistent language. Do you need constructor classes? Do you need higher kinded types?

Objects based on values

Mon, 19 Feb 2018 06:50:03 +0000

I don't object to objects based on values, although I don't see it as necessary. I am happy to have two classes of thing, objects and values on equal footing. What I do think is important is the ability to abstract pure value-oriented interface from impure object-oriented code. Haskell only permits the reverse, I think you need both. To truly encapsulate state and tame the combinatorial explosion of complexity, being able to define a pure (message passing) API to a module is important. I want module implementations to be written in simple efficient imperative code, but I want the module interfaces to compose easily and encapsulate that implementation.

Encapsulation of Impurity

Mon, 19 Feb 2018 06:42:23 +0000

I like Ada, I especially like Ada's package and generics system, but I don't like the way they added the OO stuff using tagged objects. What I am interested in is the encapsulation of Impurity. The following:
```f(x, y) = {
t := 0
while x < y:
t += x
++x
return t
}
```
Has an impure implementation, but has a pure interface. In Haskell this would need to be in the State/IO monad, but what I would like to see is that we look at the interface not the implementation. I am interested in observable purity/impurity.