5
$\begingroup$

What is a weak function space and what does it have to do with higher order abstract syntax?

I mean I know what a weak function space is. It's that thing you use for HOAS in Lambda Prolog or toolkits like Beluga!

But what are the technical details here?

In category theory functions are abstracted away to exponential objects of closed Cartesian categories (not the same as a Cartesian closed category, STLC with product types is Cartesian closed, STLC without product types is closed Cartesian) and residuals/internal homs of closed monoidal categories.

I have a hunch weak function spaces don't really work like exponentials at all.

$\endgroup$
4
  • 1
    $\begingroup$ I'm curious where have you seen this term being used? $\endgroup$
    – Couchy
    Jun 7, 2022 at 23:16
  • $\begingroup$ @Couchy I was able to find link.springer.com/chapter/10.1007/978-3-030-45231-5_26 but that's definitely not where I heard this term. Not really sure where I read the term. $\endgroup$ Jun 7, 2022 at 23:36
  • 1
    $\begingroup$ I think weak functions still work like exponentials. It is more accurate to say that exponentials here don't work like sets. $\endgroup$
    – Trebor
    Jun 8, 2022 at 2:30
  • 2
    $\begingroup$ Look at the exponentials in the category of linear spaces. They are much, much smaller than set-theoretic functions. $\endgroup$
    – Trebor
    Jun 8, 2022 at 2:31

1 Answer 1

8
$\begingroup$

In category theory the adjective “weak” is used when the uniqueness parts of a universal property is removed.

For example, a weak product of $A$ and $B$ is an object $P$ with morphisms $p_1 : P \to A$ to $p_2 : P \to B$, such that, for all $f : C \to A$ and $g : C \to B$ there exists (not necessarily unique!) $h : C \to P$ satisfying $p_1 \circ h = f$ and $p_2 \circ h = g$.

We may apply the same idea to exponentials. A weak exponential of $A$ and $B$ is an object $E$ with a morphism $e : E \times A \to B$ such that, for all $f : C \times A \to B$ there exists (not necessarily unique!) $h : C \to E$ such that $e \circ (h \times \mathrm{id}_A) = h$. This is just the usual universal property of exponentials, with the uniqueness part removed.

An example of a category which has weak exponentials but no exponentials is the category of topological spaces and continuous maps. In more syntactic settings, such as logical frameworks, removing the uniqueness part from the definition of exponentials corresponds to removing the $\eta$-rule. Consequently, given a term $z : C, x : A \vdash f : B$, there may be many terms $z : C \vdash h : A \to B$ satisfying $$z : C, x : A \vdash f \equiv h\, x : B.$$

To see that the $\eta$-rule gives uniqueness, given $h_1$ and $h_2$ satisfying the above equation, observe that $$h_1 \equiv (\lambda x \,. h_1 \, x) \equiv (\lambda x \,.f) \equiv (\lambda x \,. h_2 \, x) \equiv h_2.$$ Conversely, from uniqueness we get $\eta$-rule as follows: given any $z : C \vdash h : A \to B$, observe that $$z : C, x : A \vdash h\,x \equiv h\,x : B$$ and by $\beta$-reduction $$z : C, x : A \vdash h\,x \equiv (\lambda y \,. h\,y) \, x : B$$ therefore by uniqueness $z : C \vdash h \equiv (\lambda y \,. h\,y) : A \to B$.

As an exercise you can verify that weakness of products correspond to absence of the $\eta$-rule $(\pi_1\,t, \pi_2\,t) \equiv t : A \times B$.

Let us also try to answer the question “what does it have to do with HOAS?“ Recall that in HOAS we use the meta-level function space to model binding in the object-level terms. Does the meta-level $\eta$-rule transfer to the object-level $\eta$-rule? For that we would need something like (I am using $\mathtt{typeface}$ to denote object-level syntactic constructs): $$\mathtt{lambda}(\lambda x \,. \mathtt{app}(h,x)) \equiv h,$$ which is not the case because “object-level application $\mathtt{app}$ is not meta-level application“. So in HOAS the object-level $\eta$-rule is not available, hence “weak” exponentials.

Incidentally, the meta-level $\beta$-reduction fails to transfer to object-level $\beta$-reduction also, because the object-level $\beta$-reduction is something like $$\mathtt{app}(\mathtt{lambda}(t), u) \equiv t \, u,$$ and once again the equation does not hold. Of course, one could consider HOAS with object-level equations, in which case both the $\beta$-reduction and the $\eta$-rule could be imposed.

$\endgroup$
3
  • $\begingroup$ If I understand you right rephrasing the product example as a multisorted first order theory the difference is between $\vdash \forall x\colon \tau_1. \forall y\colon \tau_2. \exists! z\colon \tau_1 \times \tau_2. x = \pi_1(z) \wedge y = \pi_2(z) $ and $\vdash \forall x\colon \tau_1. \forall y\colon \tau_2. \exists z\colon \tau_1 \times \tau_2. x = \pi_1(z) \wedge y = \pi_2(z) $. Wouldn't there also be a difference between weak positive and negative products? $\vdash \forall z\colon \tau_1 \times \tau_2. \exists x\colon \tau_1. \exists y\colon \tau_2. z = (x, y)$ $\endgroup$ Jun 8, 2022 at 17:53
  • $\begingroup$ Hold on eta rules can be used to encode induction right? So weak types are types you can't do induction/coinduction over basically? $\endgroup$ Jun 9, 2022 at 4:11
  • $\begingroup$ Typically once cannot do a straightforward induction on HOAS. Or to put it another way: if you attempt to define HOAS as an inductive type, then your HOAS will contain the so-call "exotic terms" that shouldn't be there. $\endgroup$ Jun 9, 2022 at 15:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.