Stream: Hierarchy Builder devs & users

Topic: Indexed carriers?

Shea Levy (Oct 09 2020 at 11:57):

I'd like to implement a hierarchy of languages where type indices ensure we have well-formed formulae by construction. E.g. if I have some two-sorted theory and some predicate P over terms of sort x, I'd like to be able to construct terms like $\forall (v : x), P(v)$ but not terms like $P(P)$ or even $\forall (v:y), P(v)$. Can this be done with hierarchy builder? I'm assuming the "carrier" would be an indexed family in this case?

Cyril Cohen (Oct 09 2020 at 12:00):

Dear @Shea Levy I am not sure I understand, can you explain what your hierarchy would look like informally?

Paolo Giarrusso (Oct 09 2020 at 12:02):

And are you trying to implement languages or their models? For context, when you implement groups, you are implementing models of group theory, not the language of group theory.

Paolo Giarrusso (Oct 09 2020 at 12:03):

(Presumably, in algebra you need to formalize the language when dealing with word problems, but that’s the only use case)

Shea Levy (Oct 09 2020 at 12:04):

Cyril Cohen said:

Dear Shea Levy I am not sure I understand, can you explain what your hierarchy would look like informally?

Could be something like propositional logic, first order logic, first order logic with equality...

Shea Levy (Oct 09 2020 at 12:05):

Paolo Giarrusso said:

And are you trying to implement languages or their models? For context, when you implement groups, you are implementing models of group theory, not the language of group theory.

I'm not completely sure but I think languages. I want to be able to construct formulae, sound arguments given inference rules, etc.

Paolo Giarrusso (Oct 09 2020 at 12:05):

do you need to do induction on syntax?

Shea Levy (Oct 09 2020 at 12:06):

Can you give an example?

Shea Levy (Oct 09 2020 at 12:07):

I may want to e.g. reason about proofs or formulae themselves, not just the mathematical objects they represent

Paolo Giarrusso (Oct 09 2020 at 12:07):

Lemma foo (P : objectProposition) : .... Proof. induction P.

Paolo Giarrusso (Oct 09 2020 at 12:08):

well, it doesn’t sound like you’re doing algebra, it sounds more like the material in SF . vol 2.

Paolo Giarrusso (Oct 09 2020 at 12:09):

And using a hierarchy here sounds odd.

Shea Levy (Oct 09 2020 at 12:10):

It's a relationship between the languages though. E.g. the kind of thing I might use recursion schemes for in Haskell

Paolo Giarrusso (Oct 09 2020 at 12:12):

Not sure how recursion schemes are relevant here.

Shea Levy (Oct 09 2020 at 12:12):

Maybe a red herring. I just want to be able to define languages that have some common syntax/semantics but some extend others.

Cyril Cohen (Oct 09 2020 at 12:13):

So I guess the carrier is a type for languages ? The operations would be the constructions of the language (connectives, atoms, etc), and the axioms would be the laws of the logic... Right?

Shea Levy (Oct 09 2020 at 12:13):

Yeah

Cyril Cohen (Oct 09 2020 at 12:13):

The think I do not get, is the indexed part

Paolo Giarrusso (Oct 09 2020 at 12:14):

@Cyril Cohen but having axioms seems not enough, since Shea needs induction on formulas

Cyril Cohen (Oct 09 2020 at 12:14):

The way I would implement variable binding would be having a function fvar : L -> set X where X is the parameter holding the type of variables.

Cyril Cohen (Oct 09 2020 at 12:14):

Paolo Giarrusso said:

Cyril Cohen but having axioms seems not enough, since Shea needs induction on formulas

Induction could be an axiom

Paolo Giarrusso (Oct 09 2020 at 12:16):

technically, induction _could_ be an axiom, but then this discussion has a problem

Cyril Cohen (Oct 09 2020 at 12:16):

But indeed, by inserting induction as an axiom you are asserting you are dealing with an initial object, and this trivializes each structure and makes inheritance impossible

Cyril Cohen (Oct 09 2020 at 12:16):

Yep, there is a problem indeed

Paolo Giarrusso (Oct 09 2020 at 12:16):

that’s a nice way to put it indeed

Paolo Giarrusso (Oct 09 2020 at 12:16):

before discussing implementation details, we should figure out if the mathematics to do is algebra or proof theory.

Paolo Giarrusso (Oct 09 2020 at 12:17):

Algebraic approaches to logic exist, but they look very different — there you’re formalizing Heyting/Boolean algebras

Cyril Cohen (Oct 09 2020 at 12:19):

I was focusing on the "indexed" carrier part (because replacing carrier with arbitrary types is indeed a next step for HB)

Paolo Giarrusso (Oct 09 2020 at 12:20):

that certainly has usecases — the obvious formalization of categories uses an indexed/parametric type of arrows?

Paolo Giarrusso (Oct 09 2020 at 12:21):

for the original question by @Shea Levy , I have 2 answers:

Paolo Giarrusso (Oct 09 2020 at 12:24):

1) indexed types might be inappropriate — even if GADTs might be appropriate in Haskell, in Coq they’re often annoying, and you typically rather want separate definitions for “terms” (not-indexed) and “proofs that terms are well-formed” (indexed)

Paolo Giarrusso (Oct 09 2020 at 12:24):

2) it sounds like you want extensible syntax — in Haskell you’d be using “Data types à la carte”. That’s not impossible in Coq (see “meta theory à la carte”), but it’s not worth it.

Paolo Giarrusso (Oct 09 2020 at 12:26):

it’s also not worth it because in proof theory there is often limited reuse when going from a small theory (like propositional logic) to a bigger theory (like FOL).

Paolo Giarrusso (Oct 09 2020 at 12:30):

on answer 1), a needed footnote is that using indexed types “GADT-style” is useful in Agda and has some support in Coq through the Equations plugin. Even then, I’d only recommend that to a pretty small group of specialists, as it’s too easy to paint yourself into a corner that you can’t get out of.

Shea Levy (Oct 09 2020 at 12:44):

Hmm, OK, thanks! I guess I need to get more clarity on exactly what I'm trying to do

Christian Doczkal (Oct 09 2020 at 12:55):

Paolo Giarrusso said:

2) it sounds like you want extensible syntax — in Haskell you’d be using “Data types à la carte”. That’s not impossible in Coq (see “meta theory à la carte”), but it’s not worth it.

Hmm, a while ago I proved soundness and completeness of axiomatizations for Propositional Dynamic Logic (PDL) and PDL with Converse. The diff between the two formalizations is maybe 5% or so, and I would have really liked to have extensible syntax back then, but the paper you mention does not make me eager to look at this more closely. The approach looks really heavy. Still makes me sad though.

Paolo Giarrusso (Oct 09 2020 at 16:49):

@Christian Doczkal I’ve spent significant time on extensible algebraic datatypes/the expression problem — that was not in Coq/Agda but in Scala/Haskell, where more reasonable solutions exist. Therefore, I’d recommend indexing your syntax by a boolean “has_converse” flag, potentially wrapped in a typeclass.

Paolo Giarrusso (Oct 09 2020 at 16:50):

And that’s exactly because a good solution is an open research problem, which I think is really important.

Paolo Giarrusso (Oct 09 2020 at 16:51):

However, supporting arbitrary extensions is much harder than specific extensions (e.g. FOL -> FOL with equality).

Paolo Giarrusso (Oct 09 2020 at 16:52):

While going from propositional logic to FOL seems likely to require starting over and using a different interface, because of binding (disclaimer: I’m actually thinking of STLC -> System F, never actually dealt with FOL)

Last updated: Sep 25 2023 at 12:01 UTC