[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.swee...@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
