## Stream: Type theory

### Topic: coq's type theory

#### Reid Barton (May 25 2020 at 23:57):

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 (May 26 2020 at 00:02):

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 (May 26 2020 at 00:26):

Hmm actually I just see a lot of Scala files

#### Mario Carneiro (May 26 2020 at 00:26):

yep, their codebase is huge and unreadable

#### Mario Carneiro (May 26 2020 at 00:27):

and I still don't really understand what it does

#### Reid Barton (May 26 2020 at 00:31):

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

#### Reid Barton (May 26 2020 at 00:53):

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

#### Reid Barton (May 26 2020 at 00:53):

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

#### Mario Carneiro (May 26 2020 at 01:39):

Which MMT paper is this?

#### Mario Carneiro (May 26 2020 at 01:44):

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

#### Mario Carneiro (May 26 2020 at 01:47):

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


#### Mario Carneiro (May 26 2020 at 01:49):

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 (May 26 2020 at 07:27):

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 (May 26 2020 at 09:10):

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

#### Reid Barton (May 26 2020 at 09:12):

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 (May 26 2020 at 09:27):

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 (May 26 2020 at 09:31):

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 (May 26 2020 at 09:31):

oh, gzipped xml, what a format

#### Mario Carneiro (May 26 2020 at 09:33):

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

#### Mario Carneiro (May 26 2020 at 09:33):

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

#### Reid Barton (May 26 2020 at 09:34):

I bet it's like an ML module

#### Reid Barton (May 26 2020 at 09:34):

I also have no idea what those are though

#### Mario Carneiro (May 26 2020 at 09:34):

I also think it's like an ML module

#### Mario Carneiro (May 26 2020 at 09:35):

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

#### Mario Carneiro (May 26 2020 at 09:35):

they seem kind of like existential types?

#### Mario Carneiro (May 26 2020 at 09:36):

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

#### Reid Barton (May 26 2020 at 09:39):

ML has them so they must be good

#### Reid Barton (May 26 2020 at 09:40):

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 (May 26 2020 at 09:41):

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 (May 26 2020 at 09:57):

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 (May 26 2020 at 10:22):

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 (May 26 2020 at 10:25):

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

#### Sebastian Ullrich (May 26 2020 at 10:40):

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 (May 26 2020 at 10:41):

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

#### Sebastian Ullrich (May 26 2020 at 11:30):

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 (May 26 2020 at 11:31):

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

#### Mario Carneiro (May 26 2020 at 11:32):

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

#### Sebastian Ullrich (May 26 2020 at 11:36):

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 (May 26 2020 at 11:37):

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

Last updated: May 08 2021 at 21:09 UTC