Hacker News new | past | comments | ask | show | jobs | submit login

This algebraic approach to program semantics is basically how categorical semantics works. The syntactic equational theory of the simply typed lambda calculus with pairs, for example, is that of the "free" cartesian closed category. It can be mapped (in a way that respects the cartesian closed structure) into any cartesian closed category, giving you a semantics.

A monoid can be seen as a one-object category (the monoid elements are the morphisms on that object, and the monoid operator is morphism composition), so perhaps concatenative languages have categorical semantics too. (Although it seems like the semantics of "quote", or whatever [ foo bar baz ] is in forth, might make things a little interesting - ie. require more structure than a monoid homomorphism. I expect you really want cartesian closed categories, and quote is probably curry or apply.)




I don’t know how concatenative languages fit into category theory—I would guess Cartesian closed categories are the place to start, but that’s not really my area of expertise.

Maybe you can offer some insight if I tell you that the quotation syntax “[ … ]” in a concatenative language corresponds to lambda abstraction:

    e : a
    ---------------------
    [ e ] : ∀s. s → s × a
And the quotation operator “quote”, which takes a value on the stack and returns it quoted, corresponds to eta-expansion (or lifting lambda abstraction into a term, if you like) and has the type:

    quote : ∀sa. s × a → s × (∀t. t → t × a)
Generally the standard Turing-complete basis in concatenative calculus is the following set of combinators:

    compose : ∀rstu. r × (s → t) × (t → u) → r × (s → u)
    swap : ∀sab. s × a × b → s × b × a
    drop : ∀sa. s × a → s
    dup : ∀sa. s × a → s × a × a
    quote : ∀sa. s × a → s × (∀t. t → t × a)
    apply : ∀st. s × (s → t) → t
(Although you can get away with fewer if they’re equivalent in power.)

The first three correspond to the standard B, C, K, and W combinators from combinatory logic, which give you all the substructural rules from logic—swapping is exchange, dropping is weakening, and copying is contraction. Without swap/drop/dup, it’s equivalent to ordered linear lambda calculus, which can be interpreted in any category (since it’s just B and I); what are the categorical equivalents of linear (BC), affine (BCK), ordered (BKW), and relevant (BCW) logics?




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: