7
$\begingroup$

I will distinguish between mathematical functions and computational functions which I will think of for concreteness as $\lambda$-functions.

In every context I’ve encountered, the type signature of a lambda function depends only on its input-output relation. However, it seems to me that we can distinguish between two functions of the same input output types on the basis that they use a different set of types in their computation:

$f:\mathbb N\to \mathbb N \quad f=\lambda x:\mathbb N, (x+1)$

$g:\mathbb N\to \mathbb N \quad g=\lambda x:\mathbb N, (\text{toNat}\, (\text{toInt}\,x) + 1)$

Where $\text{toNat}:\mathbb Z \to \mathbb N, \text{toInt}:\mathbb N \to \mathbb Z$ do the obvious thing. (Note that $g$'s computations "depend on type $\mathbb Z$" but $f$'s do not).

In my own words, $f$ and $g$ have the same type signature but don’t have the same “type dependence” because $g$ depends on $\mathbb Z$.

Primary question: Is there a standard term for what I've called "type dependence"? Is there a standard theory of how to distinguish between $f$ and $g$ in terms of their “type dependence”?

Note: my question is not about "extentionality vs intentionality". See the comments.

—————

Secondary question:

I want to think about the difference between “type signature” and “type dependence” in categorical terms.

If we have morphisms (which we will think of as $\lambda$-functions) $f:A\to B$ and $g:B\to C$, then $g\circ f$ has type signature $g\circ f:A\to C$, but in a sense, the function $g\circ f$ has a type dependency on $B$.

Let’s say we have a $\lambda$-function $h:A\to C$, such that $h$ computes the same as $g\circ f$, which we will denote as an equivalence $h\equiv g\circ f$, but $h$ does not have a type dependence on $B$.

We want to be able to say: “the diagram containing $f,g,h$ commutes” while only referring to the equivalence in terms of "input-output equivalence" of $h$ and $g\circ f$, not their equivalence in terms of "type dependence".

Secondary question. Is there some kind of pre-existing theory within category theory about these things related to what I’ve been calling “type dependence”?

$\endgroup$
5
  • 2
    $\begingroup$ W.r.t. your first question, this isn't really a "dependency" thing in any sense in which the word is usually used. Rather it seems like you're discovering the difference between extensional equality, and intensional equality; your example $f,g$ are extensionally the same, but intensionally different. And I don't think there's a singular, simple mathematical description of what this difference looks like. $\endgroup$
    – Malice Vidrine
    Commented Mar 3, 2019 at 21:47
  • 1
    $\begingroup$ @MaliceVidrine It is correct that they are extensionally the same but intensionally different, but that is not the concept I’m looking for. It is possible for them to be intensionally different but have the same (what I call) type dependency: e.g.: $\lambda x:\mathbb N, x+1$ and $\lambda x:\mathbb N, x+1-1+1$ have (1) the same extensionality, (2) a different intensionality, but (3) the same type dependency (they only use the type$\mathbb N$ in their computation). Again, I don’t know what the right term is for what I’m calling type dependency. $\endgroup$
    – user56834
    Commented Mar 4, 2019 at 6:07
  • $\begingroup$ The thing one may note (I don't know how relevant it is to your question) is that this is not a matter of the function itself, even up to judgmental equality, but rather a matter of the construction of the function, which one may describe by a term in the language. That is, you're not taking $f: \mathbb {N\to N}$ and asking what is its type dependency, you're taking a term of this type and asking what it is. But then couldn't you just add this in the definition by induction of terms ? That is, define a "term with type dependencies" by induction ? $\endgroup$
    – Maxime Ramzi
    Commented Jul 1, 2019 at 11:40
  • $\begingroup$ @Max, yes this is precisely the direction in which I'm interested, and wondering if there is a type theory about this. $\endgroup$
    – user56834
    Commented Jul 1, 2019 at 11:54
  • $\begingroup$ So you're more looking for references/names than for an account ? (I can't give either, but just trying to make it perhaps clearer for people who could) $\endgroup$
    – Maxime Ramzi
    Commented Jul 1, 2019 at 12:03

1 Answer 1

Reset to default
1
$\begingroup$

The standard categorical model of types and terms "forgets" a lot of information that it is reasonable for us to be interested in. It even renders equivalent all terms up to $\beta \eta$ equivalence, which sweeps all the difficulties of normalization, weak confluence under the rug and pretends they don't exist. So you may have a hard time finding categorical constructions where a morphism "remembers" all the objects that it passed through on the way; the usual impetus leads towards collapsing away all easily observed distinguishing features between "computationally equivalent" morphisms and coding the important information we want to use to reason about them into the domain and codomain.

If you plan to experiment with this, you could try using the "classifying space" of the category of types/terms, or the "nerve/realization" construction, to model your ideas. This would return a simplicial complex (or if you just want the combinatorial data, a simplicial set) where the sequence of morphisms $\lambda x:\mathbb N, (\text{toNat}\, (\text{toInt}\,x) + 1):\mathbb{N}\to\mathbb{N}\to \mathbb{Z}\to\mathbb{N}$ returns a three-dimensional simplex whose vertices are the types involved, the edges somehow represent the individual morphisms, and the composition of all of them somehow represents the whole simplex joining them all together.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .