Re: [racket-dev] [plt] Push #23181: master branch updated
On Mon, Aug 8, 2011 at 2:26 AM, Eli Barzilay 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
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? -- ((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay: http://barzilay.org/ Maze is Life! _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] [plt] Push #23181: master branch updated
On Sat, Aug 6, 2011 at 2:47 PM, Casey Klein wrote: > On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler > wrote: >> On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein >> wrote: >>> On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen >>> 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
Yes. On Aug 7, 2011, at 12:09 PM, Casey Klein wrote: > On Sun, Aug 7, 2011 at 10:50 AM, Matthias Felleisen > 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
On Sun, Aug 7, 2011 at 10:50 AM, Matthias Felleisen 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
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 > wrote: >> On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein >> wrote: >>> On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen >>> 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
I like it. Robby On Sat, Aug 6, 2011 at 2:47 PM, Casey Klein wrote: > On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler > wrote: >> On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein >> wrote: >>> On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen >>> 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
On Sat, Aug 6, 2011 at 1:58 PM, Robby Findler wrote: > On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein > wrote: >> On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen >> 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
On Sat, Aug 6, 2011 at 1:53 PM, Casey Klein wrote: > On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen > 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
On Sat, Aug 6, 2011 at 10:43 AM, Matthias Felleisen 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
On Sat, Aug 6, 2011 at 8:43 AM, Matthias Felleisen 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
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 wrote: > > On Fri, Aug 5, 2011 at 8:13 AM, 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
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 wrote: > On Fri, Aug 5, 2011 at 8:13 AM, 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
Re: [racket-dev] [plt] Push #23181: master branch updated
On Fri, Aug 5, 2011 at 8:13 AM, 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
