Style Guide

[phlegmaticprogrammer]

Nope, there is not going to be a style guide ;-) But here are some suggestions what I would do different in the bootstrap theories:

First, I notice that you prefer val over def a lot of times. Why? When defining a function you should really use def in almost all cases. One example is (in theory Syntax):

val destconj = '‹p› ∧ ‹q›' => [p, q]

could be replaced by

def destconj '‹p› ∧ ‹q›'  =  [p, q]

Also, why does desteq return a list? Do you want to emulate an option type? You could just use nil instead. So instead of

val desteq = tm =>
  match tm
    case '‹p› = ‹q›' => [[p,q]]
    case _           => []

I'd recommend

def 
  desteq '‹p› = ‹q›' => [p,q]
  desteq _ => nil 

One last example I came across when quickly glancing through the theories:

val [symThm,sym] =
  theorem symThm: '∀ x:ℙ, y. x = y → y = x'
    let 'x:ℙ'
    let 'y:ℙ'
    assume asm:'x = y'
    modusponens (reflexive 'x',combine (reflexive '(z ↦ z = x)', asm))
  [symThm, (thm =>
              match term thm
              case '‹x›=‹y›' => modusponens(thm,instantiate (symThm,x,y)))]

symThm and sym don't have to be defined in one val statement; symThm should be a theorem, and sym should be a def. Also note that you can match theorems, too:

theorem symThm: '∀ x:ℙ, y. x = y → y = x'
  let 'x:ℙ'
  let 'y:ℙ'
  assume asm:'x = y'
  modusponens (reflexive 'x',combine (reflexive '(z ↦ z = x)', asm))

def sym '‹x›=‹y›' as thm = modusponens(thm,instantiate (symThm,x,y))

Finally, let me say: It's pretty cool what you have already done with ProofScript!! :-D

[ghost]

1) I prefer val over def for the same reason I prefer let over letrec. It makes it clear that the function is non-recursive and allows you to shadow the function-name you are introducing. It's a habit I've taken from Ocaml.

2) I hadn't realised that there was a "nil" value in Proofscript. Still, there are uses for having [] represent failure. It means you can write

for x in foo y do
   ...something involving x...

And if foo y "fails" by returning [], then the whole expression will evaluate to [], propagating the failure.

[pikan]

Nope, there is not going to be a style guide

Let's not rule out anything at this early stage. This may be worth a discussion and more experimenting first, especially if the number of "suggestions" piles up as time goes by.

2) I hadn't realised that there was a "nil" value in Proofscript. Still, there are uses for having [] represent failure.

Although in the case of success, you end up -- as for your definition of desteq -- returning a (singleton) list of list, which, aside from being somewhat counterintuitive, is rather ugly.

All we need now is for you to use [] to represent false as well and we'll be in Lisp territory (which, added to your inherited habits from Ocaml, will surely make a style guide a must). :)

[ghost]

Although in the case of success, you end up -- as for your definition of desteq -- returning a (singleton) list of list, which, aside from being somewhat counterintuitive, is rather ugly.

A compromise would be to have nil propagate when appearing in for expressions: for x in nil do ... => nil

All we need now is for you to use [] to represent false as well and we'll be in Lisp territory (which, added to your inherited habits from Ocaml, will surely make a style guide a must). :)

Hey, Scheme doesn't use nil to represent false.

[phlegmaticprogrammer]

Lol. Yeah, if you insist on porting your Ocaml habits, then we actually need to have a Style guide :-)

Having [] represent nil is just horrible taste. There is nothing wrong with

if x <> nil then ... else nil

It also makes it much clearer what is actually going on.

Concerning val vs. def, if you actually have to overshadow, then use val by all means. Otherwise, please use def. There is no value in distinguishing recursive from non-recursive functions.

[ghost]

I'm not going to insist on anything. I'll make the changes.

[phlegmaticprogrammer]

Thanks!

[phlegmaticprogrammer]

After a soothing shower I realised that actually the style of my comments was not OK ... So, here we go again:

• If we didn't have nil, then using a list is actually a very good option (no pun intented). But as we have it now, there is no need to cling on to it.
• Distinguishing recursive from non-recursive functions can sometimes be useful, usually during debugging long and complex functions that somebody else has written. But a) this can actually easily be supported by the user interface (right click on the name of the function could give you information about it, like for example if it is recursive or non-recursive), and b) I think it is more important to make clear via def that it is a function in the first place. Usually, whether a function is recursive or not recursive is obvious and also not that interesting.

[phlegmaticprogrammer]

Concerning a style guide: My initial opposition is based on my experience that I hate to have to change how I write my code based on the stupid opinion of others. But now that WE are the others, and of course we have only sensible and well thought out opinions, it makes a lot of sense to have that style guide, I think :-D

[ghost]

Addendum on the val versus def question. In impure languages, it is typical to have function definitions which look like:

 let f =
    let foo = ... in
    fun x -> ... foo ... x ...

as opposed to:

let f x =
  let foo = ... in
  ... foo ... x ...

These are always equivalent in pure languages, but not in impure languages, where the right-hand side might contain side-effects. In the first instance, the right-hand side of foo must generally be evaluated once. In the second instance, it must be evaluated in every call to f.

They are also not equivalent in proof-script, because the context varies between calls to f, and this can alter the meaning of foo. To avoid wasted evaluation (suppose that the right-hand side of foo is a theorem with a complex proof), some of my top-level function definitions will be of the form

 val f =
   ...
   x => ...

On 19/09/14 12:16, Steven Obua wrote:

Concerning a style guide: My initial opposition is based on my experience that I hate to have to change how I write my code based on the stupid opinion of others. But now that WE are the others, and of course we have only sensible and well thought out opinions, it makes a lot of sense to have that style guide, I think :-D

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/38#issuecomment-56164745.