Re: [racket-dev] [plt] Push #23181: master branch updated

[Casey Klein]

On Mon, Aug 8, 2011 at 2:26 AM, Eli Barzilay e...@barzilay.org wrote:
 Two days ago, Casey Klein wrote:

 Oh, I see. I like that. How do you feel about using the same style
 for contracts? For example:

 (define-judgment-form nats
     #:mode (sum I I O)
     #:contract (sum n n n)

 Not a party I'm familiar with, but separating the IOs from the types
 seems bad.  Can't they be specified together?


That could work:

(define-judgment-form nats
(sum [n I] [n I] [n O])
)

Or if you choose not to supply a contract:

(define-judgment-form nats
(sum I I O)
)

I think you're right that something like this would be better.

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Matthias Felleisen]

Good, now change define-judgment-form to define-judgment. 


On Aug 6, 2011, at 3:47 PM, Casey Klein wrote:

 On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler
 ro...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein
 clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
 matth...@ccs.neu.edu wrote:
 
 1. I like Robby's mode suggestion.
 2. I prefer shorter keywords, e.g., define-judgment.
 
 I'm having trouble reconciling these comments. Robby's suggestion, if
 I understand it correctly, is to overload the `define-relation' name
 instead of choosing a new one. If you supply the #:mode keyword, you
 get the `define-judgment-form' behavior (inputs and outputs, static
 checking, the `judgment-holds' syntax for application); if not, you
 get the current `define-relation' behavior.
 
 My suggestion was meant to be separate from the overloading thing. You
 could use a #:mode even for define-judgment.
 
 
 Oh, I see. I like that. How do you feel about using the same style for
 contracts? For example:
 
 (define-judgment-form nats
#:mode (sum I I O)
#:contract (sum n n n)
[(sum z n n)]
[(sum (s n_1) n_2 (s n_3))
 (sum n_1 n_2 n_3)])

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Casey Klein]

On Sun, Aug 7, 2011 at 10:50 AM, Matthias Felleisen
matth...@ccs.neu.edu wrote:

 Good, now change define-judgment-form to define-judgment.


Did you miss my objection to that name?
_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Matthias Felleisen]

Yes. 

On Aug 7, 2011, at 12:09 PM, Casey Klein wrote:

 On Sun, Aug 7, 2011 at 10:50 AM, Matthias Felleisen
 matth...@ccs.neu.edu wrote:
 
 Good, now change define-judgment-form to define-judgment.
 
 
 Did you miss my objection to that name?

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Casey Klein]

On Sat, Aug 6, 2011 at 2:47 PM, Casey Klein
clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler
 ro...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein
 clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
 matth...@ccs.neu.edu wrote:

 1. I like Robby's mode suggestion.
 2. I prefer shorter keywords, e.g., define-judgment.

 I'm having trouble reconciling these comments. Robby's suggestion, if
 I understand it correctly, is to overload the `define-relation' name
 instead of choosing a new one. If you supply the #:mode keyword, you
 get the `define-judgment-form' behavior (inputs and outputs, static
 checking, the `judgment-holds' syntax for application); if not, you
 get the current `define-relation' behavior.

 My suggestion was meant to be separate from the overloading thing. You
 could use a #:mode even for define-judgment.


 Oh, I see. I like that. How do you feel about using the same style for
 contracts? For example:

 (define-judgment-form nats
    #:mode (sum I I O)
    #:contract (sum n n n)
    [(sum z n n)]
    [(sum (s n_1) n_2 (s n_3))
     (sum n_1 n_2 n_3)])


I'm having trouble getting syntax/parse to produce good error messages
for this grammar. Here's a stripped down version of my best attempt:

(define-for-syntax (mode-keyword stx)
  (raise-syntax-error #f keyword invalid outside of mode specification stx))
(define-syntax I mode-keyword)
(define-syntax O mode-keyword)

(define-syntax (define-judgment-form stx)
  (define-syntax-class mode
#:literals (I O)
(pattern I)
(pattern O))
  (define-syntax-class rule
#:description rule
(pattern [conc:expr prem:expr ...]))
  (syntax-parse stx
[(_ (~or (~once (~seq #:mode (name-mode:id pos-mode:mode ...))
#:name mode specification)
 (~optional (~seq #:contract (name-ctc:id pos-ctc:expr ...))
#:name contract specification))
...
rule:rule ...)
 #''OK]))

This definition rejects the right uses, but I'm not satisfied with the
error message produced in this case:

(define-judgment-form
  #:contract (sum n n n)
  [(sum z n n )]
  [(sum (s n_1) n_2 (s n_3))
   (sum n_1 n_2 n_3)])

The error points to the first rule and says, expected the literal
#:contract or expected the literal #:mode. I'd like it to say that
the mode spec is missing, since another contract spec just leads to a
different error.

I can get what I want by doing more of the parsing by hand, but I
wonder if there's an easier way than this:

(define-syntax (define-judgment-form stx)
  (define-syntax-class mode
#:literals (I O)
(pattern I)
(pattern O))
  (define-syntax-class mode-spec
#:description mode specification
(pattern (name:id modes:mode ...)))
  (define-syntax-class contract-spec
#:description contract specification
(pattern (name:id contracts:expr ...)))
  (syntax-parse stx
[(_ (~or (~seq #:mode mode:mode-spec)
 (~seq #:contract contract:contract-spec))
...
rule ...)
 (let-values ([(name/mode mode)
   (syntax-parse #'(mode ...)
 [((name . mode)) (values #'name #'mode)]
 [_ (raise-syntax-error #f expected a mode
specification stx)])]
  [(name/ctc ctc)
   (syntax-parse #'(contract ...)
 [() (values #f #f)]
 [((name . contract)) (values #'name #'contract)]
 [(_ . dups)
  (raise-syntax-error #f expected at most one
contract specification
  #f #f (syntax-list #'dups))])])
   #''OK)]))

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Matthias Felleisen]

1. I like Robby's mode suggestion. 

2. I prefer shorter keywords, e.g., define-judgment. 

3. Why is this in github and not in the docs? 


On Aug 5, 2011, at 9:56 PM, Robby Findler wrote:

 How about 
 
  #:mode (sum I I O)
 
 for the mode spec where the #:mode keyword is optional but, if present must 
 be followed by what looks like a use of the relation but with a
 Mode?
 
 Robby
 
 On Friday, August 5, 2011, Casey Klein clkl...@eecs.northwestern.edu wrote:
  On Fri, Aug 5, 2011 at 8:13 AM,  clkl...@racket-lang.org wrote:
  clklein has updated `master' from 1a65678924 to 576272362b.
   http://git.racket-lang.org/plt/1a65678924..576272362b
 
 
  This push adds a more general way to define relations in Redex,
  currently under the name define-judgment-form. For those of you
  familiar with the existing define-relation form, this new form lifts
  the restriction that relations have no outputs when executed. In
  particular, it lets you specify which positions are inputs and which
  are outputs, and it statically checks that the outputs can be computed
  from the inputs without guessing any intermediate values.
 
  Here's a simple example:
 
  (define-language nats
   (n z (s n)))
 
  (define-judgment-form nats
   mode : O O I
   sum ⊆ n × n × n
   [(sum z n n)]
   [(sum (s n_1) n_2 (s n_3))
(sum n_1 n_2 n_3)])
 
  (judgment-holds (sum (s (s z)) (s z) (s (s (s z)
  true
  (judgment-holds (sum (s (s z)) (s z) (s (s z
  false
  (judgment-holds (sum (s z) n (s (s z))) n)
  `((s z))
  (judgment-holds (sum n_1 n_2 (s (s z))) (n_1 n_2))
  `(((s (s z)) z) ((s z) (s z)) (z (s (s z
 
  I see three use cases:
 
  1. Defining type systems in a way that supports mechanized
  typesetting. Here's an example:
 
  https://gist.github.com/1128672
 
  There are still plenty of type systems Redex can't express, but the
  new form gets a lot of low-hanging fruit.
 
  2. Defining structural operational semantics in a way that supports
  mechanized typesetting. Here's an example:
 
  https://gist.github.com/1128685
 
  Relations defined in this way don't work directly with traces. You can
  embed them in reduction-relation, as the example demonstrates, but you
  lose out on edge labels. It shouldn't be too difficult to rig up
  something better, if this turns out to be important.
 
  3. Defining relations using something like multi-valued metafunctions.
  Here's an example in which (add1 e) may reduce to 0.
 
  https://gist.github.com/1128692
 
  Any feedback is welcome, but I'm especially interested in opinions on
  two points:
 
  1. Is there a better name than define-judgment-form? I would have
  liked the name define-relation, if it weren't already taken. Is it OK
  to overload it?
 
  2. Should mode declarations use a different syntax? I tried to do
  something in the paren-free style of define-relation contracts, but I
  don't like the result -- partially because I personally like parens,
  partially because it makes it harder to give good error messages.
 
  _
   For list-related administrative tasks:
   http://lists.racket-lang.org/listinfo/dev 
  _
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Robby Findler]

On Sat, Aug 6, 2011 at 8:43 AM, Matthias Felleisen matth...@ccs.neu.edu wrote:
 3. Why is this in github and not in the docs?

I think you're mistaken here. It is in the head on our git servers.

Robby
_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Casey Klein]

On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
matth...@ccs.neu.edu wrote:

 1. I like Robby's mode suggestion.
 2. I prefer shorter keywords, e.g., define-judgment.

I'm having trouble reconciling these comments. Robby's suggestion, if
I understand it correctly, is to overload the `define-relation' name
instead of choosing a new one. If you supply the #:mode keyword, you
get the `define-judgment-form' behavior (inputs and outputs, static
checking, the `judgment-holds' syntax for application); if not, you
get the current `define-relation' behavior.

Do you mean keep the forms separate but use the name `define-judgment'
for the new one? I intentionally avoided that name because what it
defines, for example `sum', is not itself a judgment. Judgments are
uses of that thing, i.e., assertions about particular objects, for
example (sum z z z).

 3. Why is this in github and not in the docs?


Oh, good idea!
_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Robby Findler]

On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein
clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
 matth...@ccs.neu.edu wrote:

 1. I like Robby's mode suggestion.
 2. I prefer shorter keywords, e.g., define-judgment.

 I'm having trouble reconciling these comments. Robby's suggestion, if
 I understand it correctly, is to overload the `define-relation' name
 instead of choosing a new one. If you supply the #:mode keyword, you
 get the `define-judgment-form' behavior (inputs and outputs, static
 checking, the `judgment-holds' syntax for application); if not, you
 get the current `define-relation' behavior.

My suggestion was meant to be separate from the overloading thing. You
could use a #:mode even for define-judgment.

(Casey is referring to the idea that define-relation is kind of like
define-judgment but where you have an all-output mode as the default.)

 Do you mean keep the forms separate but use the name `define-judgment'
 for the new one? I intentionally avoided that name because what it
 defines, for example `sum', is not itself a judgment. Judgments are
 uses of that thing, i.e., assertions about particular objects, for
 example (sum z z z).

 3. Why is this in github and not in the docs?


 Oh, good idea!

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Casey Klein]

On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler
ro...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein
 clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
 matth...@ccs.neu.edu wrote:

 1. I like Robby's mode suggestion.
 2. I prefer shorter keywords, e.g., define-judgment.

 I'm having trouble reconciling these comments. Robby's suggestion, if
 I understand it correctly, is to overload the `define-relation' name
 instead of choosing a new one. If you supply the #:mode keyword, you
 get the `define-judgment-form' behavior (inputs and outputs, static
 checking, the `judgment-holds' syntax for application); if not, you
 get the current `define-relation' behavior.

 My suggestion was meant to be separate from the overloading thing. You
 could use a #:mode even for define-judgment.


Oh, I see. I like that. How do you feel about using the same style for
contracts? For example:

(define-judgment-form nats
#:mode (sum I I O)
#:contract (sum n n n)
[(sum z n n)]
[(sum (s n_1) n_2 (s n_3))
 (sum n_1 n_2 n_3)])
_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Robby Findler]

I like it.

Robby

On Sat, Aug 6, 2011 at 2:47 PM, Casey Klein
clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler
 ro...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein
 clkl...@eecs.northwestern.edu wrote:
 On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen
 matth...@ccs.neu.edu wrote:

 1. I like Robby's mode suggestion.
 2. I prefer shorter keywords, e.g., define-judgment.

 I'm having trouble reconciling these comments. Robby's suggestion, if
 I understand it correctly, is to overload the `define-relation' name
 instead of choosing a new one. If you supply the #:mode keyword, you
 get the `define-judgment-form' behavior (inputs and outputs, static
 checking, the `judgment-holds' syntax for application); if not, you
 get the current `define-relation' behavior.

 My suggestion was meant to be separate from the overloading thing. You
 could use a #:mode even for define-judgment.


 Oh, I see. I like that. How do you feel about using the same style for
 contracts? For example:

 (define-judgment-form nats
    #:mode (sum I I O)
    #:contract (sum n n n)
    [(sum z n n)]
    [(sum (s n_1) n_2 (s n_3))
     (sum n_1 n_2 n_3)])


_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Casey Klein]

On Fri, Aug 5, 2011 at 8:13 AM,  clkl...@racket-lang.org wrote:
 clklein has updated `master' from 1a65678924 to 576272362b.
  http://git.racket-lang.org/plt/1a65678924..576272362b


This push adds a more general way to define relations in Redex,
currently under the name define-judgment-form. For those of you
familiar with the existing define-relation form, this new form lifts
the restriction that relations have no outputs when executed. In
particular, it lets you specify which positions are inputs and which
are outputs, and it statically checks that the outputs can be computed
from the inputs without guessing any intermediate values.

Here's a simple example:

(define-language nats
  (n z (s n)))

(define-judgment-form nats
  mode : O O I
  sum ⊆ n × n × n
  [(sum z n n)]
  [(sum (s n_1) n_2 (s n_3))
   (sum n_1 n_2 n_3)])

 (judgment-holds (sum (s (s z)) (s z) (s (s (s z)
true
 (judgment-holds (sum (s (s z)) (s z) (s (s z
false
 (judgment-holds (sum (s z) n (s (s z))) n)
`((s z))
 (judgment-holds (sum n_1 n_2 (s (s z))) (n_1 n_2))
`(((s (s z)) z) ((s z) (s z)) (z (s (s z

I see three use cases:

1. Defining type systems in a way that supports mechanized
typesetting. Here's an example:

https://gist.github.com/1128672

There are still plenty of type systems Redex can't express, but the
new form gets a lot of low-hanging fruit.

2. Defining structural operational semantics in a way that supports
mechanized typesetting. Here's an example:

https://gist.github.com/1128685

Relations defined in this way don't work directly with traces. You can
embed them in reduction-relation, as the example demonstrates, but you
lose out on edge labels. It shouldn't be too difficult to rig up
something better, if this turns out to be important.

3. Defining relations using something like multi-valued metafunctions.
Here's an example in which (add1 e) may reduce to 0.

https://gist.github.com/1128692

Any feedback is welcome, but I'm especially interested in opinions on
two points:

1. Is there a better name than define-judgment-form? I would have
liked the name define-relation, if it weren't already taken. Is it OK
to overload it?

2. Should mode declarations use a different syntax? I tried to do
something in the paren-free style of define-relation contracts, but I
don't like the result -- partially because I personally like parens,
partially because it makes it harder to give good error messages.

_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev

Re: [racket-dev] [plt] Push #23181: master branch updated

[Robby Findler]

How about

 #:mode (sum I I O)

for the mode spec where the #:mode keyword is optional but, if present must
be followed by what looks like a use of the relation but with a
Mode?

Robby

On Friday, August 5, 2011, Casey Klein clkl...@eecs.northwestern.edu
wrote:
 On Fri, Aug 5, 2011 at 8:13 AM,  clkl...@racket-lang.org wrote:
 clklein has updated `master' from 1a65678924 to 576272362b.
  http://git.racket-lang.org/plt/1a65678924..576272362b


 This push adds a more general way to define relations in Redex,
 currently under the name define-judgment-form. For those of you
 familiar with the existing define-relation form, this new form lifts
 the restriction that relations have no outputs when executed. In
 particular, it lets you specify which positions are inputs and which
 are outputs, and it statically checks that the outputs can be computed
 from the inputs without guessing any intermediate values.

 Here's a simple example:

 (define-language nats
  (n z (s n)))

 (define-judgment-form nats
  mode : O O I
  sum ⊆ n × n × n
  [(sum z n n)]
  [(sum (s n_1) n_2 (s n_3))
   (sum n_1 n_2 n_3)])

 (judgment-holds (sum (s (s z)) (s z) (s (s (s z)
 true
 (judgment-holds (sum (s (s z)) (s z) (s (s z
 false
 (judgment-holds (sum (s z) n (s (s z))) n)
 `((s z))
 (judgment-holds (sum n_1 n_2 (s (s z))) (n_1 n_2))
 `(((s (s z)) z) ((s z) (s z)) (z (s (s z

 I see three use cases:

 1. Defining type systems in a way that supports mechanized
 typesetting. Here's an example:

 https://gist.github.com/1128672

 There are still plenty of type systems Redex can't express, but the
 new form gets a lot of low-hanging fruit.

 2. Defining structural operational semantics in a way that supports
 mechanized typesetting. Here's an example:

 https://gist.github.com/1128685

 Relations defined in this way don't work directly with traces. You can
 embed them in reduction-relation, as the example demonstrates, but you
 lose out on edge labels. It shouldn't be too difficult to rig up
 something better, if this turns out to be important.

 3. Defining relations using something like multi-valued metafunctions.
 Here's an example in which (add1 e) may reduce to 0.

 https://gist.github.com/1128692

 Any feedback is welcome, but I'm especially interested in opinions on
 two points:

 1. Is there a better name than define-judgment-form? I would have
 liked the name define-relation, if it weren't already taken. Is it OK
 to overload it?

 2. Should mode declarations use a different syntax? I tried to do
 something in the paren-free style of define-relation contracts, but I
 don't like the result -- partially because I personally like parens,
 partially because it makes it harder to give good error messages.

 _
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev
_
  For list-related administrative tasks:
  http://lists.racket-lang.org/listinfo/dev