Curried Actions In The Polyadic π-Calculus
When you're building a concurrent functional programming language around an internal language derived from the π-calculus, it's a known strategy [c.f. Pict, by Pierce and Turner] to allow applicative expressions to be used in the place of π-names in action prefixes. These are a kind of syntactic sugar that expand to a concurrent process that produces the result of function application on an ephemerally bound name that takes the place of the expression.
I've been thinking lately about how currying might work in this syntax. It's doable, but I'm not sure it can be done implicitly the way OCaml and Haskell do it, i.e. where it always makes sense for the programmer to use the curried syntax over the uncurried syntax, because A) it's more flexible and B) it's faster (the uncurried form involves more boxing).
In OCaml, you can define a function like this:
let f u : int -> int -> int =
printf "u=%u\n" u;
fun v -> u + v
When you call that function with a partial application of only one argument, as in let x : int -> int = f 5 in ..., the printf function is called and the result is a function object that adds 5 to its integer argument and returns the result without printing any further output.
I'm not sure how OCaml does this, but it does.
What I want is a similar thing in the D-fusion calculus [a derivative of the π-calculus I've mentioned previously]. I think it might be doable, but I haven't figured it out yet. It seems like the arrow type operator actually needs to be a constructor in the derived syntax. The core internal syntax needs to allow for various principle channel sorts to appear in the derived syntax as expressions involving the arrow operator.
In other words, consider this derived type expression for a binary function in two polymorphic types:
∀α β. α → β → α
It can be derived from two different internal language principle type expressions that can be used equivalently in functional expressions so long as the compiler keeps track of things properly:
A :: ⟦ ∀α β. να νβ λ⟦ λα ⟧⟧
B :: ⟦ ∀α. να λ⟦ ∀β. νβ λ⟦ λα ⟧⟧⟧
The type expression in A) means send two names, one of type α and the other of type β, and receive one name of type ⟦ λα ⟧ where the response will arrive. The type expression in B) means send one name of type α and receive a name of type ⟦ ∀β. νβ λ⟦ λα ⟧⟧ where to send another name of type β and receive a name where the response will arrive. A functional definition where B and A are not equivalent processes would need to be recorded in the compiled module in pretty much the same way that OCaml does its magic.
I need to figure out how to handle that. I think, but I'm not sure, that this is what goes on inside compile interface files in OCaml. The signature says 'a b. 'a -> 'b -> 'a, but the .cmi file says the moral equivalent of "here is the address for partial applications in one variable, and here is another address for full applications in both variables."
My Groups
-
Amnesty International Updated: 3 hours ago
-
Writers Hub Updated: 3 days ago
Neighborhood
Explore friends, family, friends & family, or entire neighborhood.
