Home

Typed Concurrent Programming with Logic Variables

Typed Concurrent Programming with Logic Variables

We present a concurrent higher-order programming language called Plain and a
concomitant static type system. Plain is based on logic variables and computes
with possibly partial data structures. The data structures of Plain are procedures, cells, and records. Plain's type system features record-based subtyping, bounded existential polymorphism, and access modalities distinguishing between reading and writing.

You may want to compare this with The Oz Programming Model (OPM), which

... is a concurrent programming model subsuming higher-order functional and object-oriented programming as facets of a general model. This is particularly interesting for concurrent object-oriented programming, for which no comprehensive formal model existed until now. The model can be extended so that it can express encapsulated problem solvers generalizing the problem solving capabilities of constraint logic programming.

Another paper on OPM is The Operational Semantics of Oz.

In short, the model of Plain is based on that of Oz with the main differences being:

  1. Plain statically types programs using a type system with subtyping, while Oz is latently typed.
  2. Therefore Plain chooses to drop support for unification in favor of a single-assignment operation.
By Andris Birkmanis at 2006-05-05 08:33 | Functional | Logic/Declarative | Object-Functional | Semantics | Type Theory | other blogs | 8325 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Unification could be spared?

As the authors mentioned, unification per se is not incompatible with subtypes, it's just a total reliance on unification that makes subtyping unused (because variables engaged in unification are non-variant - similar to reference cells, or collections in Java; all for the same reason - bidirectional data flow).

Therefore, it might be possible to keep unification in the language, and leave decision of its usage to programmers - the same way as they decide whether or not to use cells.

By Andris Birkmanis at Fri, 2006-05-05 08:38 | login or register to post comments

The Operational Semantics of Oz

This paper is an early version of chapter 13 of CTM.

By Peter Van Roy at Fri, 2006-05-05 09:47 | login or register to post comments

Insider info?

I am intrigued by this paper (in the OP) not being cited anywhere.
What happened to Plain? Was it abandoned completely, or the ideas were brought to some other languages?
How is its history and team related to those of Oz/Alice?

By Andris Birkmanis at Fri, 2006-05-05 12:21 | login or register to post comments

Smolka's gang

Andreas, Guido, and the other current members of Smolka's gang decided to go the route of Alice rather than try to retrofit Oz with static typing. I assume that Plain was some initial exploration. The problem that I see is that if you don't have dataflow variables (i.e. unification variables), then even though the language might be made to look like Oz, you'd essentially have a much different language. In lieu of full unification, Alice came to use promises as the basis for logic variables.

By Chris Rathman at Fri, 2006-05-05 15:27 | login or register to post comments