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 & logic

Topic: APG type theory

Julius Hamilton (Aug 24 2024 at 18:29):

apg.jpg

The set $\mathcal{V}$ of typed values are terms in the following grammar:

$v : t ::= () : 1 | inl_{t_2} (v : t_1) : t_1 + t_2 | inr_{t_1} (v : t_2) : t_1 + t_2 | (v_1 : t_1, v_2 : t_2) : t_1 \times t_2 | \text{ Prim }v_t : t (t \in P, v \in PV(p)) | \text{ Elmt }e : \lambda(e) (e \in \mathcal(E)$

This says:

There is a set $\mathcal{V}$ whose elements are values
Each value of $\mathcal{V}$ has a type $t$ .
- This is written $v : t$ .
- This collection of types is denoted $\mathcal{T}$ .
$v$ can be of any of the following types:
- The unit type $1$
- The sum type $t_1 + t_2$ , where $t1, t2$ are types in $\mathcal{T}$ .
- The product type $t_1 \times t_2$ .
- The primitive type $t$
- The label type $\lambda(e)$ , for an element $e$

Looking at the whole picture:

You have a schema $S$ , which is a pair $(\mathcal{L}, \sigma)$ . $\mathcal{L}$ is a set of labels, and $\sigma$ assigns each label to a type. Thus, a schema is a bunch of typed labels. Your labels could be “Car”, “Elizabeth”, “meets”. The only types are unit, sum, product, primitive, and label; so I guess $\sigma$ might assign individuals to $1$ , essential concepts to “primitive”, any sort of function, relation or grouping to a product type, any sort of “optional grouping” to a sum type, and I’m not sure what the label type is doing in there, since the labels should be in $\mathcal{L}$ , whereas all these other typed values should be in $\mathcal{V}$ .

2.jpg

You have elements.
You map elements to their labels.
You map values to their types.
You map elements to their values.

And I guess the takeaway here is that our labels have type annotations, and our values have type annotations, and every element has a label and a value.

Is this correct?

Ryan Wisnesky (Aug 24 2024 at 18:47):

sounds about right. there are some built-in examples in the CQL IDE ('APG' being the name of the example)

Julius Hamilton (Aug 24 2024 at 19:20):

Thanks.

These conjectures are unproven?

3.jpg

Ryan Wisnesky (Aug 24 2024 at 19:45):

I'm not sure. @Joshua Meyers would be the person to ask. An earlier version of the paper had a bunch of relatively easy theorems proved in Coq, https://arxiv.org/pdf/1909.04881v1 , and then in attempt to connect the work to Poly, which would have made for cooler theorems, progress stalled out, for reasons I don't remember but might be Coq related and not math related.