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.
signature.asc
Description: PGP signature
