coq's type theory

Stream: Type theory

[Reid Barton]

If I understand this MMT talk correctly, they must have a formal specification of Coq's type theory somewhere in their project @Mario Carneiro

[Mario Carneiro]

Indeed, it is interesting that they seem to have been successful in acquiring exports in an almost disjoint set from my attempts. Coq and isabelle in particular seem quite difficult but they have managed it(?)

[Reid Barton]

Hmm actually I just see a lot of Scala files

[Mario Carneiro]

yep, their codebase is huge and unreadable

[Mario Carneiro]

and I still don't really understand what it does

[Reid Barton]

From the demo I expected to see a description in LF or something

[Reid Barton]

ok, looking at their paper, I don't think they actually have a declarative description of the typing rules

[Reid Barton]

I did find some nice mmt files in a separate repository though
https://gl.mathhub.info/MMT/LATIN2/-/tree/master/source

[Mario Carneiro]

Which MMT paper is this?

[Mario Carneiro]

The relevant reference for Coq export appears to be https://kwarc.info/people/frabe/Research/MRS_coq_19.pdf

[Mario Carneiro]

Which links to https://gl.mathhub.info/Coq/foundation/blob/master/source/Coq.mmt

[Mario Carneiro]

theory Coq : ur:?LF =
  include ?CoqSyntax❙
  /T We omit the typing rules of Coq.❙
❚

[Mario Carneiro]

by the way, if you are curious about the funny characters at the end of each line, that is because MMT made the slightly nutty decision that all MMT keywords should be low ASCII unprintable characters like RS (record separator)

[Kevin Buzzard]

It's nice to see low ASCII unprintable characters again. They were very popular in the late 80s. Character 7 used to make my Acorn Atom beep. Printing non text files could get quite noisy

[Reid Barton]

Ah, I was looking at https://arxiv.org/pdf/2005.03089.pdf

[Reid Barton]

Yes, I was curious about those. At first I thought they were just something the IDE showed for some reason, not actual source characters! Then when I found the mmt files online, I thought they were Unicode box-drawing characters

[Mario Carneiro]

I believe the reason for the design is that because MMT is a metalanguage, it tries to maximize the flexibility of the second level language, and I guess that means all regular characters are reserved and so they have to use a character no one would ever use. I think this is a self-refuting proposition though

[Mario Carneiro]

But you could also skip the MMT part and just focus on the "getting things out of Coq" part, which leads to http://www.cs.unibo.it/~sacerdot/cicm19/xmlexport.pdf

[Mario Carneiro]

oh, gzipped xml, what a format

[Mario Carneiro]

I wish someone who knows Coq internals could explain to me what a Coq module is

[Mario Carneiro]

my lean experience does very little to help me understand what is going on there

[Reid Barton]

I bet it's like an ML module

[Reid Barton]

I also have no idea what those are though

[Mario Carneiro]

I also think it's like an ML module

[Mario Carneiro]

I wrote an ML compiler for a class and I still have no idea what ML modules are

[Mario Carneiro]

they seem kind of like existential types?

[Mario Carneiro]

It's really not clear to me why a DTT theorem prover like Coq can gain a benefit from more elaborate typing

[Reid Barton]

ML has them so they must be good

[Reid Barton]

I'm also confused by that though. I thought it was something like: give me an implementation of < and I'll give you an implementation of balanced binary search trees. Aren't dependent types enough for that already?

[Mario Carneiro]

The only thing I can think is that the necessary structure declarations to do this get unwieldy, and they want a piecemeal definition using several top level statements

[Jannis Limperg]

I get the impression that the Coq people don't really like modules either. Afaik they are hardly used in modern developments. What they give you is strong implementation hiding, but that turns out to be more cumbersome than helpful in a dependently typed language.

[Sebastian Ullrich]

Definitions inside modules, like regular definitions and unlike structure fields, can be universe polymorphic. Which means that modules cannot be first-class objects.

[Mario Carneiro]

Can they be modeled by regular definitions by just not hiding the definition?

[Sebastian Ullrich]

If you also simulate instantiating modules and applying functors by copying and instantiating/applying all definitions, I think so, yes. It's a very fancy, reusable section more or less.

[Mario Carneiro]

Could you explain that part? I don't really get why copying is involved

[Sebastian Ullrich]

You probably don't have to copy the definition body, just the signature.

def Mod.Nat.foo.{u} := @Mod.foo.{u} Nat
def Mod.Nat.bar.{u} := @Mod.bar.{u} Nat

Well now I haven't even copied most of the signature

[Mario Carneiro]

Is there a reason that downstream uses can't just say Mod.foo Nat?

[Mario Carneiro]

like do the new definitions get attributes or custom names or something?

[Sebastian Ullrich]

Yes, in Coq you would write Module ModNat := Mod Nat and then you have ModNat.foo etc. ... I think. I don't know much more than that but if this were Lean I guess you might want to register some instantiated defs as simp lemmas, for example.

[Sebastian Ullrich]

There's also this amusing page about modules vs records: https://github.com/coq/coq/wiki/ModuleSystem