I see what you mean and I can agree that rendering that with a D in this instance would have the meaning that people expect it to have.
Nevertheless, contemplating changing the pattern language in that way is daunting and since you have a way around this, maybe best to just take it for now. Sorry, Robby On Fri, Mar 25, 2016 at 11:15 AM, William J. Bowman <w...@williamjbowman.com> wrote: > On Fri, Mar 25, 2016 at 07:05:52AM -0500, Robby Findler wrote: >> I think the right way to approach such questions is to start from a more >> realistic example and then ask "what do we want the typeset version of this >> to look like?". > I like this advice. > Unfortunate, I think I want the typeset version to look like the same > pattern variable in two places but at different depths. > > For real example, I have a model of a dependent type system with > inductive type families. > To check that the declared inductive types are valid, I check that > a) the declared constructors actually return the declared type > b) the types of the constructors are strictly positive. > > Here is a snippet: > > (define-judgment-form tt-typingL > #:mode (valid I) > #:contract (valid Δ) > > [-------- "Valid-Empty" > (valid ∅)] > > [(valid Δ) > (type-infer Δ ∅ t_D U_D) > (type-infer Δ (∅ D : t_D) t_c U_c) ... > ;; NB: Ugh this should be possible with pattern matching alone .... > (side-condition ,(andmap (curry equal? (term D)) (term (D_0 ...)))) > ;; positive* should probably be a judgment so I can ... it > (side-condition (positive* D (t_c ...))) > ----------------- "Valid-Inductive" > (valid (Δ (D : t_D > ((c : (name t_c (in-hole Ξ (in-hole Θ D_0)))) > ...))))]) > > I would prefer to write as this as follows. > Notice the D_0 in the conclusion has changed to a D, and the > side-condition that escapes into Racket disappears. > > (define-judgment-form tt-typingL > #:mode (valid I) > #:contract (valid Δ) > > [-------- "Valid-Empty" > (valid ∅)] > > [(valid Δ) > (type-infer Δ ∅ t_D U_D) > (type-infer Δ (∅ D : t_D) t_c U_c) ... > ;; positive* should probably be a judgment so I can ... it > (side-condition (positive* D (t_c ...))) > ----------------- "Valid-Inductive" > (valid (Δ (D : t_D > ((c : (name t_c (in-hole Ξ (in-hole Θ D)))) > ...))))]) > > In this instance, I suppose I could create a new judgment or > metafunction that checks each constructor's type separately w.r.t. D. > Since both instances would be at depth 0, this would be fine. > Maybe even easier to read.. > > -- > William J. Bowman > > PS: You cannot run this email :( -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
