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.
Robin Piedeleu (Mar 01 2021 at 10:17):I just came across the notion of self-types in this paper: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf
As far as I understand, they are dependent types where a type can depend on the value it types. Their introduction/elimination rules are on p.4 of the paper. The authors show that this allows typing dependent elimination from lambda encodings (avoiding the addition of specific rules for inductive types on top of vanilla CoC for example).
Does anyone have any idea what a (categorical) model of a dependent type theory with self-types would look like? I'm struggling with what they mean...
Verity Scheel (Mar 01 2021 at 18:58):I haven’t gone through the details of the paper thoroughly, but isn’t the simplest option just to model self types by the corresponding inductive types? Maybe with W types in general?
Verity Scheel (Mar 01 2021 at 19:02):In some sense, my thinking on the matter is that inductive types are models of parametric functions (namely, of the shape of their induction principles). For example, there are cases where the inductive type inhabits a lower universe than the type of the recursor. And so if we have those inductive types, we can use that to make the functions more polymorphic over universes or something like that. (Vague thoughts.)
Verity Scheel (Mar 01 2021 at 20:42):Perhaps you would ask that the recursors of the inductive types are the identity or the identity up to conversion or something. (I’m not too familiar with the particulars of constructing models.)
Robin Piedeleu (Mar 02 2021 at 10:59):Nick Scheel said:
I haven’t gone through the details of the paper thoroughly, but isn’t the simplest option just to model self types by the corresponding inductive types? Maybe with W types in general?
I guess you're right if all self-types have a corresponding inductive version in a canonical way. It is not clear to me that this is the case but I'm very much a type theory noob so a lot of this goes over my head.
Verity Scheel (Mar 02 2021 at 11:35):This is the part where the details I skipped would matter, but I think they were restricting self types to shapes that made sense as inductive types. (Strictly positive, etc.) I’m not sure the translation to Fω would have worked otherwise.
Sam Kuhn (Mar 06 2021 at 11:12):You may already be aware but the Kind language (recently renamed from “Formality”) has an implementation of self types if it helps at all. The language targets JS, Haskell and also an experimental interaction net (optimal reduction) based backend.
I am also interested in a categorical interpretation of self types but that is beyond my abilities at the moment.
Sam Kuhn (Mar 06 2021 at 11:22):This is quite a nice informal summary from Victor Maia (the main author of Kind):
The main insight behind self types is easy to explain. Simple functions can be written as A -> B, and an application f a has type B. Dependent functions can be written as (x: A) -> B x, and an application f a has type B a. The insight is that the type returned by an application has access to the value of the argument a. Self dependent functions can be written as s(x: A) -> B s x, and an application f a has type B f a. The insight is that the type returned by an application can also access the value of the function f! This simple, elegant extension allow us to construct inductive datatypes with lambdas.
Original article here.
Mike Shulman (Mar 06 2021 at 15:08):But the problem is that this "insight" doesn't make much sense in category theory, where you have to have the codomain of a morphism before you can talk about the morphism.