In a previous post I posed the challenge of coming up with polymorphic types admitting certain numbers of linear inhabitants. (If you didn’t see the previous post and want to puzzle over an interesting lambda-calculus based problem, stop reading now and go read the previous post first.) In this post I’ll outline some solutions and some further questions.

First, we can make the easy observation that if we have polymorphic types admitting and linear inhabitants respectively, we can easily construct a type with inhabitants, by first alpha-varying the types so they have disjoint type parameters, then concatenating their inputs and pairing their outputs. For example, we can use , with two linear inhabitants, to construct the type with four.

OK, so we can construct types with any power of two number of inhabitants. In fact, we can get any factorial number of linear inhabitants with functions from n-tuples to n-tuples, whose linear inhabitants correspond to permutations. For example, has linear inhabitants. So now we can get any number which can be decomposed as a product of factorials.

But what about 3, or 5, or 7, or…? After thinking for several days I finally stumbled upon this type:

which has exactly three linear inhabitants, namely

That is, we can pair up the function inputs with the other inputs, or we can apply both functions to one input, or both functions (in the other order) to the other input. In each of these cases, the types ensure that we have no further choice — for example, we can’t swap the order of the outputs since then they would have the wrong types.

Generalizing a bit, consider the type

That is, we take as inputs functions arranged in a cycle (the first function maps from to , the second from to , and so on, with the th function mapping from back to ), and inputs of types through , and output an -tuple of values with types to . How many linear inhabitants does this type have, as a function of ?

Well, if we compose all the functions together we can make them into a function for any , depending on the order in which we compose them. So we can take all the functions and apply them to any one of the other inputs, passing through the remaining inputs unchanged. We can also apply each function individually to its matching input, “shifting” the types of all the inputs by one. Is there anything else we can do?

Indeed there is. For example, we could chain together some of the functions to make a function (say) , and if we compose the remaining functions we get a function — so we can apply these functions to the inputs of type and respectively, swapping their positions in the output, and passing through the remaining inputs unchanged. In fact, given a choice of *any* non-empty subset of the non-function inputs, there is exactly one way to use the given functions to cyclically permute them and pass through the other inputs unchanged. For example, if we choose , , and , then we must apply the first two functions to the to give an , the next three functions to the which will give us an , and the remaining functions applied to the will give us an again.

So the linear inhabitants of this type are in one-to-one correspondence with the non-empty subsets of , which means there are inhabitants. This gives us 3, as we saw before, and it also tells us that

has 7 linear inhabitants.

Great, so now we can create arbitrary products of factorials and Mersenne numbers. But what about, say, 5?

Well… I conjecture that no types with five linear inhabitants exist, but I don’t have a proof yet!

I just wanted to say that I find this a very interesting exploration and I enjoy reading about this a lot. This question has occurred to me in the past, but I never took the time to explore it in detail. Thanks!

What about:

∀α₁α₂α₃α₄.(∀β.β→β)→(α₁,α₂,α₃,α₄)→(α₁,α₂,α₃,α₄)

Gah, I forgot that they had to be observationally different. I liked the (∀β.β→β) trick but as it’s the identity, it doesn’t change the observable behaviour.

Yeah, too bad! After reading your comment for about 20 seconds I was thinking, “Oh, that’s so simple! Why didn’t I think of that?” …and then I realized that there was only one possible behavior.

If you liked that one, I have another solution which is “too bad” for a different reason.

∀α.(α)⁵→(α→∀β.β→β)⁴→α

(where (σ)ⁿ is a notation for the tuple (σ,σ,…,σ) of size n)

Hmm, intriguing. So the problem here is that the functions provided as arguments in the 4-tuple are necessarily nonlinear? I guess whether this is a solution depends on how precisely you interpret the original formulation of the problem!

Do you foresee any interesting theory and/or application out of this exercise?

Nope, not really! That’s not to say there isn’t. But I’m just playing around.

Have you given any thought to (deriving and) applying the free theorems from Jianzhou’s paper? They seem able to disprove the existence of functions with certain linear types…

I hadn’t, but that’s a great suggestion.

What about the following type:

`forall a . (a -> a) -> (a -> a, a -> a, a -> a, a -> a, a -> a)`

Linear inhabitants of this term need to return the argument in one of the five components of the result. The other components can only be identity functions. So we seem to have five different linear inhabitants.

Yes, I believe this works! Brilliant!

So it seems that

corresponds to

in the sense that there is an isomorphism between the linear inhabitants of

`ψ`

and the usual inhabitants of`φ`

. This isomorphism is witnessed by the Λ-termsand

Can this observation be extended to yield an encoding of structural typing in linear typing and/or the other way around?

Such an encoding could play a similar role as double negation for classical and intuitionistic logics:

`τ`

has a classical proof if and only if`not (not τ)`

has an intuitionistic proof.Very interesting observation! I will have to think about this more…

Pingback: Counting linear lambda terms: choice and correspondence « blog :: Brent -> [String]

Pingback: Counting linear lambda terms: choice and correspondence « blog :: Brent -> [String]

Pingback: Enumerating linear inhabitants « blog :: Brent -> [String]

Pingback: Enumerating linear inhabitants « blog :: Brent -> [String]