[TYPES] Objects in type theory

[Nicolai Kraus]

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