In the papers you link to, derivation seems to only be defined for positive types but $A\to B$ is a negative type. Do you know a specific paper defining the derivative on function types? I'd expect things to still kind of work for coinductive types but it looks really weird for function types. The zipper uses the tree-like structure of the term and a function has no such structure.

Ah, interesting, good catch. I do not. That might well be where these problems stem from, then. Though to a good extent it does still seem to work out. I feel like I'm at least close with my interpretation at the end there.

The problem is that I don't see a good way of interpreting minus. For division, in the presentation of bags at the end of this paper, they quotient by automorphisms instead of dividing by the factorial. You could also try to use the series expansion of the logarithm. But really, if you want to extend the zipper to functions, you probably should just set $\partial_A B^A\cong B^A$ because the whole point of the zipper is to move around to edit the structure in a functional way, and this can be done directly for functions.

It does kind of make sense to have $\partial_B B^A=B \times B^{A-1}$: you represent $f:A\to B$ as $(f(x),f_{|A\setminus\{x\}})$ for some $x\in A$. So maybe it's more that you can't differentiate with respect to types that are in a contravariant position.

I'm honestly not sure that this is relevant but this paper offers an interpretation of negative types under certain conditions. Under that interpretation, the negatives are a form of backtracking to ensure, in the case of $2^a$, that no value is used more than once.

Perhaps what you say is more practical (I'm not sure I follow though, what do you mean by $\partial_A B^A \cong B^A$, Can you elaborate, please?), though I'd still like to know whether and how this can be interpreted in a sound, rigorous way.

If you see a zipper as some way of moving around and modifying the structure in a functional way, then for functions, you don't need to move around and $\operatorname{change_value}(f, k, v):=\lambda x. \operatorname{if} x = k \operatorname{then} v \operatorname{else} f(x)$ allows you to change the value. So if by $\partial_A B^A$ you mean "the zipper-like structure on $B^A$", it makes sense to set $\partial_A B^A \equiv B^A$.

But if you think of $\partial_A X$ as "the zipper-like structure on $X$ that edits $A$s", then $\partial_B B^A$ makes sense because you change the values of the function but $\partial_A B^A$ doesn't because you shouldn't change values of type $A$ in a function: you take all of them.

hi

crap

there is no mathjax in chat -.-

yeah

there are some scripts to change that which I thought I had in place but alas they do not work for some reason

Btw, it should be $\partial B^A=\partial B \times B^{A-1}$:

Or more precisely $\partial_X B(X)^A=\partial_X B(X) \times B(X)^{A-1}$.

but d_A B^A makes no sense because I shouldn't change values of type A in a function since they are all used up.

That makes sense

It really is a strange notion to start from A -> B and then replace a single value in A to arrive at A' -> B

Exactly. In a way, a function A->B doesn't contain elements of A, it only uses them. It does "contain" elements on B though.

Hmm

I guess a set doesn't even have a notion of what its elements are, does it?

Like, if you took the set {1, 2, 3} and changed it into the set {1, 2, 4}, that change might matter relative to other sets, but as long as it's just that set on its own, that's really just a relabelling

Not represented as A->bool, no.

It's more like, since A may not be recursively enumerable, unless you are given a key, you can't do anything with a A->bool.

If A is not recursively enumerable, A->bool isn't really a set because you can't enumerate its elements.

an element of A->bool*

I'm sorry if these questions are dumb. I'm honestly at a very beginner stage of these things

Well... I guess it depends what you call a set. But I'd expect enumerating elements to be part of the interface.

Another argument to say that the zipper shouldn't touch elements of type A. You can think of elements of an inductive types as labeled trees, where nodes are labeled by constructor and have as subtrees the arguments given to those constructors. Similarly, f:A->B can be though of a tree of depth one where there is a single constructor of arity |A| at the root. So while for inductive types the zipper does have to move, for functions, since the depth is only one it doesn't have to move.

And when looking at it this way, modifying an element of type A doesn't really make sense.

interesting

one constructor c of arity |{1,2,3}|=3

and then f is represented as c(f(1),f(2),f(3))

All I'm saying is that a function can be seen as a big product type / record.

right, you could, in principle, memoize the entire function

yeah, of course

(in my example it is)

given infinite time and memory, you could technically do it for an infinite domain too, right? - At least countably-infinite

but anyway

In conclusion, I don't think zippers are relevant for functions ^.^

heh

I suppose

Not sure what to do with my question though

Can you write a proper answer or something?

Also, if you write $B^A = B x B x ... x B$, it feels weird to differentiat with respect to A.

hmm, it's like having a space with a variable number of dimensions

which certainly is unusual

I'll can try to write an answer summarizing what has been said in chat, but not right now.

That's fine

I'll be there

cu later then. Thanks!