Zulip Chat Archive

Stream: Type theory

Topic: coq's type theory


view this post on Zulip 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

view this post on Zulip 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(?)

view this post on Zulip Reid Barton (May 26 2020 at 00:26):

Hmm actually I just see a lot of Scala files

view this post on Zulip Mario Carneiro (May 26 2020 at 00:26):

yep, their codebase is huge and unreadable

view this post on Zulip Mario Carneiro (May 26 2020 at 00:27):

and I still don't really understand what it does

view this post on Zulip Reid Barton (May 26 2020 at 00:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2020 at 01:39):

Which MMT paper is this?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2020 at 01:46):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 01:47):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Reid Barton (May 26 2020 at 09:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2020 at 09:31):

oh, gzipped xml, what a format

view this post on Zulip Mario Carneiro (May 26 2020 at 09:33):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 09:33):

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

view this post on Zulip Reid Barton (May 26 2020 at 09:34):

I bet it's like an ML module

view this post on Zulip Reid Barton (May 26 2020 at 09:34):

I also have no idea what those are though

view this post on Zulip Mario Carneiro (May 26 2020 at 09:34):

I also think it's like an ML module

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2020 at 09:35):

they seem kind of like existential types?

view this post on Zulip 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

view this post on Zulip Reid Barton (May 26 2020 at 09:39):

ML has them so they must be good

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 26 2020 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 26 2020 at 10:41):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2020 at 11:31):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 11:32):

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

view this post on Zulip 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.

view this post on Zulip 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