Talk:Combinator Junk

This language ought to embed cleanly in Cammy. I can hack up a compiler if necessary. Corbin (talk) 22:29, 17 May 2026 (UTC)

Looked at Cammy, I can see we were thinking among similar lines. In fact, your page's link to wikipedia:primitive recursive functional was rather enlightening. Since I can't work on a compiler for quite some time, that sounds splendid -- though my plans for the compiler did involve a few things not covered in the article, like being able to leave out signatures that are easily inferred. Junkshipp (talk) 23:55, 17 May 2026 (UTC)

Cammy's types are fully inferred and there's actually no syntax for explicit type signatures. I think that the main issue with CJ is a lack of algebraic laws, combined with a lack of categorical structure; while SK is able to form all of the various legal sentences of first-order predicate logic in a certain sense, and is among the complete systems that can do so, SK does not know about products or coproducts (to say nothing of a proper semiring of types which interleaves them) and can't prove that its NNO is the real deal. Cammy assumes that products, coproducts, lists, etc. are free over its builtin types, which are merely N and a wikipedia:IEEE 754 object F. Corbin (talk) 19:06, 20 May 2026 (UTC)

Questions I am planning to look into

[Comment made by User:Junkshipp on 18 May 2026.]

Can you encode pairs of all types A × B?

I consider one to be able to encode pairs of a specific type A × B when you can define the following functions as terms in CJ (named here for convenience)

(For some type C,)

• pair : A -> B -> C
• fst : C -> A
• snd : C -> B

such that

• fst (pair a b) = a
• snd (pair a b) = b

A positive answer to the question would mean having a similar construction for all types A and B.

Update: I believe this is possible, but haven't written a proof yet.

I believe it's not, but no proof yet either. --Blashyrkh (talk) 06:32, 20 May 2026 (UTC)

Just a vague idea why it's not possible: (pair a b)'s type is Function. The only way to introspect it somehow (A and B are encoded somewhere somehow in its type) is to call it. In your statically-typed system a call accepts some type (only one) and returns some type (only one as well), so neither A nor B can leak from the call. If function call doesn't allow A and B to leak separately, then what does? --Blashyrkh (talk) 07:07, 20 May 2026 (UTC)

Assuming all types are constructed from N and ->, I think this works:

First, the problem can be reduced to finding some type C such that the following four functions can be defined:

• mixA : A -> C
• mixB : B -> C
• unmixA : C -> A
• unmixB : C -> B

such that

• unmixA (mixA a) = a
• unmixB (mixB b) = b

This is because we can encode pairs as type (A -> B -> C) -> C, using (pair a b) = (\f. f a b), (fst p) = unmixA (p (\a. \b. mixA a)), (snd p) = unmixB (p (\a. \b. mixB b)).

Now, with the above assumption, every type is one of $\mathbb {N}$, $P\to \mathbb {N}$, $P\to Q\to \mathbb {N}$, etc. Given this, a corresponding type C exists for every pair of types A and B. If we take e.g. two types $A=P\to Q\to \mathbb {N}$ and $B=R\to S\to \mathbb {N}$, then this we could implement the four functions using $C=P\to Q\to R\to S\to \mathbb {N}$.

Given any four terms x_P, x_Q, x_R, x_S of type P, Q, R, and S respectively, we can use (mixA a) = (\p. \q. \r. \s. a p q), (mixB b) = (\p. \q. \r. \s. b r s), (unmixA c) = (\p. \q. c p q x_R x_S), and (unmixB c) = (\r. \s. c x_P x_Q r s). And such terms will always exist, since P, Q, R, and S all will be one of $\mathbb {N}$, $P\to \mathbb {N}$, $P\to Q\to \mathbb {N}$, etc., thus it's possible to use one of zero, K zero, K (K zero) for each. –PkmnQ (talk) 10:43, 20 May 2026 (UTC)

No, such encoding cannot be implied to exist, even though both K and KI are valid phrases. Categorically, CJ doesn't have enough internal structure to set up wikipedia:categorical products. The existence of exponentials doesn't imply products on their own; you'd need a second-order quantifier which can express the idea that, for all extractable types C, there exist products of A and B which could exist for each pair of mappings C → A and C → B. For similar reasons, even with products, you would need to introduce some extra laws to upgrade N into a genuine natural-numbers object. All that said, Church-encoded pairs should be available; they are continuation-passing versions of genuine products with (non-simple) type forall C, (A → (B → C)) → C. Corbin (talk) 19:06, 20 May 2026 (UTC)

Oh, I should point out that more generally, we know that there are isomorphisms N × N → N, like wikipedia:Morton codes, for any finite products. However, there is no classical isomorphism [N, N] → N (written in your style as (N → N) → N); see computable#Via category theory for that version of wikipedia:Cantor's theorem, where there turns out to be a distinction between "computational" universes which have that isomorphism but lack discrete decidability versus "classical" universes which lack that isomorphism but have discrete elements in their sets. So you could hack up some finite products, but not all of them! Corbin (talk) 19:06, 20 May 2026 (UTC)

I think you might've misunderstood what I mean by encoding. The goal is not to define 3 functions of types A -> B -> C, C -> A, and C -> A so that these 3 functions have these polymorphic types inside the system. Instead, the question is whether we can, from outside the system, for any types A and B, for some type C, define inside the system these three functions. The construction may be entirely different for different types. Note also that the types A × B and C need not be isomorphic or for us to have a bijection at all -- to give an example not using CJ, you could encode 2 × 2 with 2 × 2 × N, with 2 standing for Boolean. Here our "C" contains an extra natural's worth of information, but this is irrelevant as long as our functions pair, fst, and snd work properly. Also, note that CJ only has simple types, so Church-encoded pairs won't work. For a sketch of what a desired construction can look like, see PkmQ's post. Junkshipp (talk) 05:54, 22 May 2026 (UTC)

Is it possible to "reduce" certain more expressive yet non-Turing Complete systems into CJ?

Obviously, this is not literally possible. What I'm really after is a proof that all terms N -> N definable in some more expressive system have an equivalent in CJ, i.e. a CJ term that always gives the same output as it for the same input. Or maybe even the same for all terms with types CJ can represent? I'm not quite sure what I'm after.

Update: I think I will handle this by trying to write a more powerful language that can be compiled into this language.