[TYPES] Objects in type theory
Nicolai Kraus
nicolai.kraus at gmail.com
Mon Jan 15 19:25:43 EST 2018
Hello,
as Bas wrote (I think his message was not published on the list, but
thanks for notifying me!), Hickey's very dependent types have been of
some interest in homotopy type theory, and I have mentioned them in my
thesis [1]. However, the context is very different from Tim's and I am
not sure whether this is relevant to the question.
Not much has actually been said about very dependent types in HoTT, and
in my thesis, I only mention them in the "future directions" chapter. I
don't think anyone has made a suggestion of how to add very types to
HoTT (or basic MLTT) so far, and I also don't know how one might do
that. The reason why they came up is that, in HoTT, one problem is
whether type-valued diagrams/presheaves can be represented internally,
in particular if the index category is the simplex category Delta
restricted to injective maps [2]; this is known as the challenge of
defining semisimplicial types. The standard approach in HoTT is trying
to write down a Reedy fibrant diagram that encodes the dependency
structure, e.g. as:
Points : Type
Edges : Points -> Points -> Type
Triangles : (a b c : Points) -> Edges(a,b) -> Edges(b,c) ->
Edges(a,c) -> Type
and so on. (I have learned about this presentation of structures in
Shulman's work [3], and I suppose the general concept is better known in
the context of Makkai's FOLD [4] in this community.) Hickey's "very
dependent function types" (p5 in his paper) seem to be a type-theoretic
way of talking about Reedy fibrant diagrams, and that's the reason
behind the interest in HoTT that Bas has pointed out. But this has not
led to anything so far.
Best,
Nicolai Kraus
[1] http://www.cs.nott.ac.uk/~psznk/docs/thesis_nicolai.pdf
[2] https://ncatlab.org/nlab/show/simplex+category
[3] Shulman, https://arxiv.org/abs/1203.3253
[4] Makkai, http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
On 12/01/18 10:18, Bas Spitters wrote:
> There's a recent interest in them in HoTT, e.g. the discussion in the
> thesis by Nicolai Kraus.
> http://eprints.nottingham.ac.uk/28986/
>
> I am not sure what the best reference is for this, but I am sure
> Nicolai and Thorsten have more information.
>
> Bas
>
> On Fri, Jan 12, 2018 at 1:37 AM, Tim Sweeney <tim.sweeney at epicgames.com> wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> Hickey's 1996 "Formal Objects in Type Theory using Very Dependent Types" (
>> http://www.cs.cornell.edu/jyh/papers/fool3/paper.pdf) laid an interesting
>> type theoretical foundation for object oriented programming constructs.
>>
>> I'm seeking references on any later work in this direction. Of particular
>> value would be papers that explore the following:
>>
>> 1. Referencing superclass fields in derived classes. E.g. A Java
>> programmer might create a class with a member function like "void
>> updateObject() {updateNewThings(); super.updateObject();}". I can't see
>> how to patch this on top of Hickey's framework without losing the
>> straightforward classes-as-types mapping.
>>
>> 2. Virtual classes (https://en.wikipedia.org/wiki/Virtual_class). Perhaps
>> F-bounded polymorphism comes to the rescue.
>>
>> 3. Ensuring open-world forward-compatibility across modules. Java and C#
>> define a broad set of ways that a given module may evolve without breaking
>> compatibility with existing code in other modules which reference it. For
>> example, one may safely add a new member function to a class. The
>> supporting subtyping mechanisms are well-understood, but naming and
>> disambiguation are required too.
>>
>> Thanks,
>>
>> Tim Sweeney
More information about the Types-list
mailing list