Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: generating type theories

Christian Williams (Dec 22 2020 at 17:44):

Hello, hope your holiday is going well enough. I had a question about references, existing literature and implementations:
What has been done toward general methods of taking a programming language and generating a type system for it automatically? Any thoughts are appreciated.

Nathanael Arkor (Dec 22 2020 at 17:45):

Could you clarify what you mean by "programming language" if that doesn't already include the type system?

Christian Williams (Dec 22 2020 at 17:50):

The language may already have a type system of its own; but a motivating example would be a language which does not already have a prominent type system, and could still benefit from one, such as Javascript.

Nathanael Arkor (Dec 22 2020 at 17:52):

Would a motivating example be automatically generating the rules for the STLC, based on the rules for the untyped LC?

Christian Williams (Dec 22 2020 at 17:52):

In terms of generating a type system, I'm mainly thinking of the idea of "a logic over a type theory" from Jacobs' Categorical Logic. I am really impressed by the idea and I don't know how much it has been implemented in practice. But also, there may be other versions of the idea of generating a type system, and I'm wondering what people may know.

Christian Williams (Dec 22 2020 at 17:52):

Yes, I would say that's a good example.

Dan Doel (Dec 22 2020 at 18:09):

Why would STLC be automatically generated and not any of dozens of other possible type systems?

Christian Williams (Dec 22 2020 at 18:14):

It just depends on the method of generating. I think I know one that would produce that system, but I would need to work it out.

Christian Williams (Dec 22 2020 at 18:14):

This is meant to be a very open-ended question, so any answers are good. There may be many things that exist under different names than what I'm describing, like some tool that gives languages pattern-matching.

Christian Williams (Dec 22 2020 at 18:15):

I'm just wondering about any general-purpose ideas/tools that provide a broad class of programming languages with higher-level reasoning.

Dan Doel (Dec 22 2020 at 18:29):

I think in general a type system that correctly describes untyped code that people end up writing ends up being extremely complex. For instance, years ago, there was this one person working on a lisp dialect that had a very programmable type system. They ended up crafting a type system for the Tk bindings (UI toolkit), and it was extremely complicated.

Dan Doel (Dec 22 2020 at 18:30):

That isn't because you couldn't do the same thing in a way that would be less complicated with respect to types, but when people don't think about simple types from the start, they end up doing ad hoc things that end up very complicated to describe.

Dan Doel (Dec 22 2020 at 18:34):

But maybe you don't care about rejecting some things that people have written.

Christian Williams (Dec 22 2020 at 22:44):

I think I understand what you mean, but I'm not sure what it means to "correctly describe" untyped code.

Christian Williams (Dec 22 2020 at 22:52):

If an auto-generated type system is meant to be general-purpose, I think probably it should be purely descriptive/agnostic. The main examples I have in mind are akin to pattern-matching, regular expressions, predicate logic.

Christian Williams (Dec 22 2020 at 22:58):

For example in a concurrent language, we can specify the single-threaded processes by $\neg[0]\land \neg[par(\neg[0],\neg[0])]$: not the null process, and not the parallel of two non-null processes. This is a type (predicate) that's just built up from language constructors and logical constructors.

Nathanael Arkor (Dec 22 2020 at 23:03):

Do I understand the example correctly: you're defining a predicate that expresses something like the following pseudo-code single_threaded(term) := !matches(term, 0) && !(matches(term, par(x, y)) && !matches(x, 0) && !matches(y, 0))?

Nathanael Arkor (Dec 22 2020 at 23:05):

Adding pattern-matching along with a specified logic to a type theory automatically seems much more constrained and feasible than trying to construct a nontrivial type theory corresponding to an arbitrary single-sorted type theory.

Nathanael Arkor (Dec 22 2020 at 23:06):

(I know I've seen this example before, but I think I hadn't understood exactly what it was intended to express previously.)

Nathanael Arkor (Dec 22 2020 at 23:13):

In that case, it seems like it could be sufficient to add the operators $=$, $\neg$, $\exists$, $\land$ to the type theory, since that predicate can be expressed as $t \neq 0 \land \nexists x, y\ .\ (t = \mathsf{par}(x, y) \land x \neq 0 \land y \neq 0)$.

Dan Doel (Dec 22 2020 at 23:32):

In the case of something like Tk, if things are completely untyped, the most basic thing would be calling functions with the correct number of arguments. However, the way people do that in untyped settings could in itself be complicated to describe. There might be multiple acceptable numbers of arguments, and the total number expected might depend on the values of earlier arguments.

Dan Doel (Dec 22 2020 at 23:32):

And the types of arguments expected might depend on earlier or later values.

Dan Doel (Dec 22 2020 at 23:34):

For a more academic example, you might say that the 'correct' untyped lambda terms are the ones that normalize, and then a type system for that is not simple types, but intersection/union types on top of that.

Dan Doel (Dec 22 2020 at 23:36):

Like, you mentioned JavaScript, but that is in some ways less well structured than even untyped lambda calculus.

Christian Williams (Dec 22 2020 at 23:43):

Yes, those are good examples. I think there is a certain reasonable class of "correctness checking" that would not be overly complicated to derive, in the right framework.