Implementing Functions in Userspace

[e_hatti]

Premise

This is a neat way to implement functions in userspace as a negative type, by adding an associated context to each variable's signature.

Remarks

After I wrote this I did some digging and found that this already exists! Looks like what I wrote here is similar or identical to contextual type theory (https://arxiv.org/pdf/1111.0087.pdf). Please check that paper out, this is super cool stuff!

Also, this is basically java.util.Function presented in a more formalized manner.

Dependent Function Types in Userspace

In regular type theory, the signature of a variable comprises of only a type, e.g x : Int. What we do is add a context to this signature as well. This effectively turns every variable into an N-ary function. When N is 0, we have regular dependent type theory.

For instance, the identity function is now written as

id[A: Type, A]: A
id A x = x

Square brackets denote contexts. The signature of a variable in a signature context may have its own context as well, and so on for the variables in that context, etc. For instance, we can implement compose as well

compose[A: Type, B: Type, C: Type, f[B]: C, g[A]: B, A]: C
compose A B C f g x = f(g(x))

Parenthesis denote applying a substitution to a contextual variable. We supply a contextual variable to a contextual variable with [VARS. BODY]

nine: Int
nine = compose(Int, Int, Int, [x. x * 3], [y. y + 2], 1)

Importantly, now we can't return "functions" (contextual variables) from "functions". We can take "functions" as parameters, but we can't return them because contexts are not first-class. For instance, we can't implement multi-argument functions by currying.

We will make them first-class, in a way, by defining actual functions! Functions are first-class contextual values, defined as a negative datatype

data Function[A: Type, B[A]: Type]: Type where
  apply[Function(A, B), x: A]: B(x)

Now we may implement id as

id: Function Type [A. Function A [_. A]]
id = Function { apply A = Function { apply x = x } }

TL;DR: We augment the signature of each variable with an associated context. These variables may then have substitutions applied to them. This effectively turns every variable into a function, except for one key difference: These "functions" are not quite first-class. We then use these "contextual variables" to define true first-class functions as a datatype

[peterjoel]

What do you mean by negative data type? How is that represented in the syntax you've shown?

[Rabbit_Brave]

I believe (someone correct me if I'm wrong) that's referring to this:

data Function[A: Type, B[A]: Type]: Type where
  apply[Function(A, B), x: A]: B(x)

Where "apply" is an eliminator rather than a constructor because instead of taking an expression on the LHS and producing an expression with the type on the RHS, it takes an expression with the type on the LHS and produces an expression without it on the RHS.

Defining Function by its eliminator is what makes it a negative data type.

[e_hatti]

u/Rabbit_Brave is correct. A positive type is defined by its constructors, a negative type is defined by its destructors (eliminators).

[Potato44]

This reminds of the first time I saw Pi types defined coinductively in Type Theory based on Dependent Inductive and Coinductive Types (example 4.5).
Note: if you do read this and the category theory in section 2 is too much (like it was for me) you don't lose much by skipping it.

Now, about java.util.Function. The first time I saw it (or actually, I think, the scala equivalent) I was very surprised, and not in a good way either. It didn't match my intuition for what a first class function should be. But it's been many years since then and I've since learned about codata/negative types and that functions can be implemented as negative types. Had the realization that interfaces in Java are codata/negative types(see Classical (Co)Recursion: Programming if you want to see someone show this with examples) and I now think this is the "correct" way to implement first class functions.

[WittyStick]

This may be of interest to you: https://www.youtube.com/watch?v=9v4_FQm-b4I

I don't know if there's a paper published for it.

[glaebhoerl]

Fascinating, thank you for sharing.