Talk:Twelf style guide

From The Twelf Project
Jump to: navigation, search

Uninhabited type flame war goes here

I noticed there was some discussion about this in another place, but while I believe it would be a good idea to standardize on the name of the uninhabited type, "void" is not really standard or "common practice" yet. (I've seen false, falsity, absurd, and void. I use "uninhabited"). We probably need to have a "standards"/style guide meeting to decide these sorts of issues. --DanielKLee 23:33, 6 September 2006 (MST)

The spirit of the thing was to put something down and then we can argue about it. It will be expedient to any sort of "standards"/style guide if we have a document to argue from. Tom recommended void, I use absurd, we should pick something. I think void is best from a type-theory point of view, I think false is best from a readability point of view, I think uninhabited is best from a idiot-proof point of view. — this is a rob (a what?) 05:26, 7 September 2006 (MST)
I think false is bad, because it is the most natural judgment to use when defining classical logic.  — Tom 7 07:28, 7 September 2006 (MST)

Note: you *can* use uppercase identifiers

The following twelf code checks (1.5R1) (and in fact syntax highlights much more correctly than it does under the wiki syntax highlighter. I won't bother fixing the wiki syntax highlighting modules - the syntax module only needs to highlight code that is well-styled for me to be happy.

NAT : type.

Z : NAT.
S : NAT -> NAT.

SIX = (S (S (S (S (S (S Z)))))).

So we should not say the parser doesn't allow it, we should say that the parser doesn't allow it but use is punishable by eternal damnation. — this is a rob (a what?) 05:42, 7 September 2006 (MST)

%abbrev

Is there really any sense in which %abbrev is "local"? It seems to me that if you ever say %abbrev s nat/s you might as well have called it s in the first place.  — Tom 7 09:11, 7 September 2006 (MST)

I'm thinking about using libraries - if you're pulling in someone else's nat, you expect things to be named nat/s and nat/z. Also, if you define s with %abbrev as the successor to a natural number, and someone else defines it as the successor to an integer with %abbrev s = int/s., then both users can use their conceptual definition of s in their files without interfering with their ability to refer to nat/s and int/s directly. Or if I really like referring to the zero and successor constants as 0 and ++, then I can do that without interfering with anyone elses definition - as long as everyone else follows the naming convention those definitions will never shadow anything else. — this is a rob (a what?) 10:13, 7 September 2006 (MST)

Terms judgments with "/"

This occured to me during the presentation with Karl. His proofs would have been much more bulky if he had used the full "/" notation for his language (though you could argue either way as to whether it would have been more clear to represent what kind of object each piece of syntax belonged to).

In general, it seems to me like we use Twelf at three different levels. This is I (think) the best way to classify the groups.

  1. Object language (tp, nat, set, exp) - Constant defintions use forward arrows (abs : (exp T1 -> exp T2) -> exp (arr T1 T2)). I don't think there is consensus for using the /-notation for type constants here.
  2. Judgments and relations (typed,plus,in-set, selfify) - Constants use backwards arrows. I don't think there's strong opposition to using the /-notation for type constants here.
  3. Meta-judgments (progress,associative-plus,superset-trans) - The %total call is used in order to prove a meta theorem. Contstants here are all called "-", so the /-notation is besides the point.

The problem with using "/" in object language notation is that you'd need to use exp/abs instead of abs. If you did this, what would the evaluation rules be called? eval-e/abs or eval-e/exp/abs?

Perhaps this isn't an entirely complete thought, hopefully the point I'm making is somewhat evident. — Rob (and his talk) 13:04, 10 September 2006 (MST)

Using a "/" in the object language notation is probably not necessary if you are working in a small language without many strata. Karl's example was limited to the singleton calculus, so managing different strata wasn't necessary for him. In my own work, I've got lots of strata (5 different things called "unit", and pair/projection at 3 different levels, 2 different things called sigma etc) so I need to do what I can to organize things. In response to the eval-e/exp/abs issue, I've been known to pun it and call the judgment something like eval-exp and then the cases are eval-exp/abs. --DanielKLee 08:52, 23 September 2006 (MST)
What do you think about what I put there yesterday, then? It seems pretty compatible from my perspective - i.e. "feel free to use single identifiers at your own risk in an outermost strata." I think eval-exp/abs makes a great deal of sense - eval-exp/abs is reasonably close to eval-e-exp/abs, which is what I was trying to recommend yesterday. However, since I put that section in the context of judgment factoring, the only situation I've encounterd it in, that section would probably greatly benefit from a rewrite by you (the whole document would :) - but that section especially). — Rob (and his talk) 09:00, 23 September 2006 (MST)
Yeah, that looks fine. --DanielKLee 09:58, 23 September 2006 (MST)

Jargonwatch and types of equality

I was trying to write a section under "specific naming conventions" that talked about the two ways to describe equality - they should have standard, and different, names. It seems to me that eq1 (syntatic equality? default equality? meta-equality?) from the example should be the default equality (i.e. should get the distinction eq-nat, but what about the other kind (definitional equality? inductive equality? structrual equality?)?

What should its designation be? I want to avoid the use of eq'-nat or eq-nat', because previous experience with apostrophies in identifiers are that they are a terrible mistake. — Rob (and his talk) 15:54, 22 September 2006 (MST)

  • I believe that shallow and deep are other common terms. I think to call the first "equality" and the other "deep" or "structural" equality sounds good.  — Tom 7 18:47, 23 September 2006 (MST)
  • So an identifer "deq" for deep equailty instead of "eq" for shallow inequality might be in order? — Rob (and his talk) 17:51, 27 September 2006 (MST)
  • Dan Licata (and by transitivity me) has used "deq" for declarative/definitional equality in the past, and aeq for algorithmic equality. These equalties were type equalities in systems where you could have equivalent types that were written differently. I tend to use eq/seq for syntactic equality (what you call shallow). I've seen others use "id". Usually seq. What do you plan on writing about "deep" equality? Maybe there are object logics where it might be useful, but at the meta-level shallow equality is very flexible and all you need. --DanielKLee 18:15, 27 September 2006 (MST)
  • "Shallow" vs. "deep" equality already has a meaning in Lisp and imperative languages that copy this meaning from Lisp. The distinction is basically irrelevant in ML/Twelf. Semantic equality and syntactic/structural equality is what we're talking about here. And doesn't an "adequate" representation ensure that these kinds of equality co-incide? So maybe "semantic equality" should instead be called an "equivalence" ? Boyland 01:44, 12 March 2007 (EDT)
  • Since "identity" is what we mean most of the time, I think that calling it "equivalence" of a certain sort when that is what we mean is the right solution. — Rob (and his talk) 11:20, 12 March 2007 (EDT)

Whitespace

This is nitpicking, but if I have a really stupid lemma I may just want to get it out of the way as quickly as possible:
nat-neq-symm : nat-neq N1 N2 -> nat-neq N2 N1 -> type.
%mode nat-neq-symm +D1 -D2.
- : nat-neq-symm nat-neq/gt nat-neq/lt.
- : nat-neq-symm nat-neq/lt nat-neq/gt.
- : nat-neq-symm (nat-neq/s N1) (nat-neq/s N2)
     <- nat-neq-symm N1 N2.
%worlds () (nat-neq-symm _ _).
%total T (nat-neq-symm T _).

Do you think the whitespace currently recommended in the document is necessary in these cases? — Rob (and his talk) 16:15, 22 September 2006 (MST)


Necessary to make the proof understandable? Probably not. Necessary to keep the structure of the code-base uniform? Probably. I try not to differentiate between how I format stupid lemmas and lemmas that make me feel stupid, out of karmic fear that the lemmas will catch on and I'll have to do more of the second kind. --DanielKLee 09:58, 23 September 2006 (MST)
I'll buy it. So is this the style we're going for? — Rob (and his talk) 12:49, 23 September 2006 (MST)
nat-neq-symm : nat-neq N1 N2 -> nat-neq N2 N1 -> type.
%mode nat-neq-symm +D1 -D2.

- : nat-neq-symm nat-neq/gt nat-neq/lt.

- : nat-neq-symm nat-neq/lt nat-neq/gt.

- : nat-neq-symm (nat-neq/s N1) (nat-neq/s N2)
     <- nat-neq-symm N1 N2.

%worlds () (nat-neq-symm _ _).
%total T (nat-neq-symm T _).


Yes. --DanielKLee 12:57, 23 September 2006 (MST)
I actually prefer the less-space version. I wrote the rational signature with 200+ theorems. By omitting blank lines except between theorems, it easily parses into a series of chunks. If I used two blank lines between each theorem and one line between each case, the whole thing would turn into a horrid mess. Boyland 23:55, 11 March 2007 (EDT)
After some testing, I realize I was wrong. It looks fine with more whitespace. Boyland 19:06, 25 April 2007 (EDT)

Word order

I'm going to just start the word order argument now. I'm not positive if the style guide should be making suggestions about word order. If there is a consensus that the style guide should be making such suggestions, then I'll detail my preferences (which happen to deviate from the guidelines given). --DanielKLee 09:58, 23 September 2006 (MST)

My motivation on word order is code reuse in general, and this floaty idea of a Twelf Standard Library in specific. If we're going to ever have something that approaches a common base version of nat, there needs to be clarity over whether it's nat-plus or plus-nat, and whether it's nat-plus-assoc, assoc-plus-nat, plus-nat-assoc, or assoc-nat-plus. Furthermore, it would be helpful if there were predective guidelines by which someone could then figure out, with a high degree of accuracy, what the metatheorem establishing the associtivity property for lists of natural numbers is (by my rules I beleive it would be append-list-nat-assoc). However, and I probably can't emphasize this enough, I see no reason to go with my preferences - if by writing down my preferences I get you to write down yours in disagreement, I'm, in general, peachy keen on going with yours (especially if it's somewhat predictive). I also hold the belief that if we can point to where the rationale for our naming conventions is, it will make our proofs more readable by others.
'Consensus' is going to be a funny animal in this world - unless by consensus you mean Tom, could you weigh in ;-) — Rob (and his talk) 12:40, 23 September 2006 (MST)
I'll concede for a Twelf Standard Library, naming conventions would make it more organized.
My preferences for the naming judgments is to usually do what best "organizes" things in the absence of a module system. For operations over natural numbers, I like to frontload the nat, so nat-plus instead of plus-nat. That way, all my definitions about arithmetic over natural numbers begins with nat- and I can sort of pretend its a nice little module.
But I'll deviate from this if there is a family of judgments that is mutually recursively defined over two levels of an object language. So I would prefer step-exp and step-md over exp-step and md-step because I sort of consider the family of step judgments to be their own module. I personally fluctuate between whether - or / is the correct seperator in these cases. As a result, my ML stuff is actually a little inconsistent between - and / and at some point I need to go back and clean that up.
Theorems can be pretty hard to name, especially when you have lots of them that don't really have canonical names. My rationale with them is whatever "organizes" them best, but that is subjective and not necessarily consistent from day to day. --DanielKLee 13:33, 23 September 2006 (MST)
I actually don't have much opinion on this at all. For the standard library we will need a naming convention, in the absense of a module system; with a module system the convention will be less important. For code written by programmers at the leaves, I don't think there is any particular need to enforce a naming convention. But, if we had to choose something, I would suggest that we use least general to most general, as if the / were . in the SML module system.  — Tom 7 18:46, 23 September 2006 (MST)

Forking off naming conventions

I was looking over the style guide, and I noticed the stuff about "word-order" and "specific naming conventions" really throws off the flow of the article. In particular, it pushes the stuff on whitespace pretty low on the page. Karl-style whitespace makes Twelf code a lot easier to read, so I feel it shouldn't get pushed too low on the article. Any disagreement on this? --DanielKLee 15:30, 27 September 2006 (MST)

None - I'd leave the "naming convention" stuff about using hyphens instead of underscores and the forward slash to present individual cases, so we have two large sections: "Identifiers" and "Whitespace" - the details can get moved to the artice on Twelf naming conventions. This has the added advantage of putting largely non-controversial stuff in this article. You'll probably get around to this before me but I may try to do it before the weekend if you don't. Another thought is that it's not necessarily a bad idea to move whitespace up above the section on identifiers. — Rob (and his talk) 17:49, 27 September 2006 (MST)

Anticipating modules

I'd like to use a naming convention that simulates modules: short names that are then abbrev'ed at the end to have a name like SIG.name, except that of course you can't use ".". Any opinions on what character would be used as a module separator, should modules ever be added? It'd be nice if the character were low-impact (ink-wise). Currently I'm experimenting with backquote.

%%%% Imports

%abbrev nat = nat`nat.
%abbrev rat = rat`rat.
%abbrev equ = rat`equ.
%abbrev gre = rat`gre.


%%%% Definitions


frv : type.

one : rat -> nat -> frv.


eq : frv -> frv -> type.

eq/ : frv_eq F F.


ge : frv -> frv -> type.

ge/ : frv_ge (one X O) (one Y O')
    <- nat`eq O O'           %% abbreviated import not necessary
    <- gre X Y.

...

%%%% Exports

%abbrev frv`frv = frv.
%abbrev frv`eq = eq.
%abbrev frv`ge = ge.

(Module names can't be UPPERCASE without a lot of pain.) To those abbrev-sceptics, it makes a difference because identifiers (like "eq") can be reused between "modules" if there is an "abbrev"iated (!) long name. Boyland 00:18, 12 March 2007 (EDT)

Just need to add that slash (the character recommended by the existing style guide for this purpose) doesn't seem like a good idea since it is already (over-)used for other things. Boyland 00:23, 12 March 2007 (EDT)
In the current planned concrete syntax for the module system, the separator will in fact be "." (and, just like in SML, whitespace won't be permitted in long identifiers, so you'll be able to tell it from the declaration-ending period, which must be followed by whitespace). Drl 00:33, 12 March 2007 (EDT)
I think it was an idea to use the slash for roughly this purpose; however if it seems overused, I think `-_+/\ all make equally decent separators, so I would say do whatever works in terms of this.
I've used an "abbrev import" style before myself, but not quite the same way. If you use short names (eq) and then re-declare them as long names with abbrev (frv`eq) as you do, then the emacs buffer is going to be filled with shadowed %eq%, and you may have to go back into your "module" to export 50 more things like gt/ in order to prove metatheorems later. If, alternatively, you write things in "long style" and then try to abbrev them down when you need them in a particular place (so you do "abbrev import" but not "abbrev export"), you don't have that metatheorem problem (you can always access anything with the long name). From my experience trying this, it is sometimes hard to read error messages when you write down as (s (s (s (s z)))) and the emacs buffer displays (nat/s (nat/s (nat/s (nat/s nat/z)))) - but you may find that this is not a significant problem for you. — Rob (and his talk) 11:16, 12 March 2007 (EDT)
Of `-_+/\, only `-/, can be typed on a US keyboard without modifiers, so I think those are to be slightly preferred. I use / since I like - as a word separator.  — Tom 7 14:05, 12 March 2007 (EDT)
Right, I'd forgotten that that was why _ fell out of favor, good point. — Rob (and his talk) 19:06, 12 March 2007 (EDT)
Regarding the need the reload a whole buffer to export an additional thing; in my current code where I use this convention, I use a perl script to export *everything*. Regarding ` vs. / vs -: I also use '-' as a word separator in theorems. I don't want / since I want something that can clearly be substituted with . (the character shouldn't be overloaded) when real modules arrive. (It seems modules have been heralded since 2001. What's their status?). Boyland 20:50, 12 March 2007 (EDT)