How to type amb in the redex exercise?

General
,
1

A long time ago I was looking at Exercise 6 in the Redex tutorial, and I stumbled on to the following:

I though it would be straightforward to modify the grammar to accept a type (e.g. , (amb t e ...) or (amb e ... : t) ) and then add the type in the corresponding judgement rule (e.g. , (types Γ e t) ... --- (types Γ (amb e ... : t) t) ), but I get

amb.rkt:78:25: define-judgment-form: found the same binder, t, at different depths, 1 and 0
  at: t

In the intervening 3 years, I guess I got to know Racket a bit better because I suspect now that the solution involves a syntax more like (amb [e : t] ...) (though I haven't actually tried it).

I'm still curious, though: is there a way to use the notation that I want, which provides a single type t that is checked against every e in (amb e ... : t)?

1 Like
2

When an ellipsis is used inside the arguments to a judgment, redex is more sophisticated about when to duplicate bindings that are used in shallower depths of ellipses than it is when the ellipsis is located between premises above the line in a judgment. That's probably what's going on in your example, I guess.

1 Like
3

What is a good solution to that exercise then?

What @benknoble suggests ((amb [e : t] ...)) doesn't seem to work either, since an amb expression might have no [e : t].

The closest solution I could find is to force amb to contain at least an expression: (amb e e ...), however it doesn't quite match the requirements, since the request is to:

Fix this by annotating amb expressions with their types

1 Like
4

Found a satisfying solution:

The grammar uses (amb e ... : t) and then I have two rules to handle a base case and a recursive one:

  [-------------------------- amb
   (types Γ (amb : t) t)]
  
  [(types Γ e_1 t)
   (types Γ (amb e ... : t) t)
   -------------------------- amb-rec
   (types Γ (amb e_1 e ... : t) t)]

Can this be expressed in better ways?

1 Like
5

I think that's the way I solved it (or something very similar).

Fundamentally, since the types judgment has the mode it has, there needs to be something that actually coughs up the type in the case that the amb has nothing inside. Unless you use a modeless judgment form (which comes with its own complexities...) there needs to be something that actually produces the type.

I don't recall if I tried it, but it might make sense to see how things play out if you always require at least one subexpression in amb (like you suggest above!)

1 Like