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

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: