11 posts tagged “language design”
I haven't posted much here lately because I've been consumed with a programming hobby project that has taken up almost all of my discretionary time. (I haven't been writing any fiction, mostly because I don't have any ideas I like as much as I liked Arts Of The Wize, which hasn't gotten any more publishable since I stopped fussing with it. I don't write here about personal and family matters. I've got other places to do that. And the programming project isn't in a place yet where it makes much sense to talk about it.)
The Problem With Software Transactional Memory: Your Languages Still Suck.
Classic threads and locks (or threads and synchronized, for you Java programmers) lead to the worst sort of Heisenbugs. True story: I once had to trace down a race condition that, doing several thousand tests per second, only manifested itself once every four days on average. The vast majority of the time it’d work just fine- the rate of failure was small enough it had escaped testing (think about it- you’ve been running the same test, thousands of times a second, for three days, and it hasn’t failed yet- when do you declare that it looks like the test is working?), but it was common enough that it was causing our customer to lock up about once a week, so it had to get fixed. Oh, and threads and locks aren’t compositional- you can’t take two hunks of code which are individually correct, and combine them to form one large, correct, piece of code. But hey, it’s not like code reuse is that important to programmers, is it?
I seem to have one. Here's the OCaml signature. The module file is all of 250 lines at this point, but I expect to define a lot of built-in processes for the preamble. That will bloat out the module file.
type 'a t
module Op: sig
val ( >>= ): 'a t -> ('a -> 'b t) -> 'b t
endval return: 'a -> 'a t
val eval: unit t -> unittype n
type repeat = Once | Alwaysval nil: unit t
val start: unit t -> unit t
val lambda: n t
val nu: n t
val fusion: n -> repeat -> n list -> unit t -> unit tval v_void: n
val v_true: n
val v_false: nval if_then_else: n -> unit t -> unit t -> unit t
type dio = D_in | D_out
val def: dio list -> (n array -> unit t) -> n tval preamble: n Name.Map.t t
I continue to noodle around with an abstract syntax for types in my internal language. (Sigh. This is taking forever.) Here's what I'm looking at now:
τ ::= α | ν⟨σ⟩ | λ(σ)
σ ::= ∀δ,σ | ∃α,σ | τ,σ | ϵ
δ ::= α | α = τ | α > τ
While I was in the shower this morning, it occurred to me that I should make a note for myself about how monads work in the polyadic D-fusion calculus.
- The type construction is simply a channel (να) for sending a value of the underlying type.
- The unit function is a channel (να λ(λ(να))) for sending a value of the underlying type and receiving a responsive channel that carries the resulting monadic value.
- The binding operation is a channel (να ν(να λ(λ(νβ)))) λ(λ(νβ))) for sending two values, 1) a monadic value of type α and 2) a channel for sending a value of the underlying type α and receiving a responsive channel that carries the resulting value of monadic type β; the binding operation channel also permits receiving a responsive channel that carries the resulting value of monadic type β.
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.
∀α β. α → β → α
A :: ⟦ ∀α β. να νβ λ⟦ λα ⟧⟧
B :: ⟦ ∀α. να λ⟦ ∀β. νβ λ⟦ λα ⟧⟧⟧
Last night, I think I figured out some important things about the π-calculus.
I just got through writing up my initial notes for a concurrent, real-time garbage collector for the parallel systems programming language I'm designing. (I've got a well-thumbed copy of Richard Jones's and Rafael Lins's book in front of me while I do this.) This is a short note to describe where I'm going.
I should have known the Eurozone would have done what I've been trying to do.
This is one of the most important sections of the present paper. In it we report a very substantial case-study of formal verification development in Coq, namely the theory of the π-calculus developed in [Milner92, section 2]. This enterprise is significant from various viewpoints. To our knowledge, it is one of the largest case-studies involving co-inductive types. But furthermore, it is perhaps the first serious attempt of using higher order syntax á la Church in metatheoretical studies outside type theory.
I'm still climbing the Twelf learning curve.
