# How to type amb in the redex exercise?

**URL:** <https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954>\
**Category:** General\
**Tags:** question, redex\
**Created:** [June 6, 2024, 12:45pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954 "2024-06-06T12:45:58Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![benknoble](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/benknoble/32/16_2.png) [@benknoble](https://racket.discourse.group/u/benknoble)\
**Post date:** [June 6, 2024, 12:45pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954/1 "2024-06-06T12:45:58Z")

</div>

[A long time ago](https://discord.com/channels/571040468092321801/667522224823205889/906280189707821138) I was looking at [Exercise 6 in the Redex tutorial](https://docs.racket-lang.org/redex/tutorial.html#%28part._.Testing_.Typing%29), 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

```scheme
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)`?

---

<div class="post-metadata">

**Author:** ![robby](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/robby/32/7_2.png) [@robby](https://racket.discourse.group/u/robby)\
**Post date:** [June 6, 2024, 1:00pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954/2 "2024-06-06T13:00:33Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![B0B](https://avatars.discourse-cdn.com/v4/letter/b/34f0e0/32.png) [@B0B](https://racket.discourse.group/u/B0B)\
**Post date:** [June 6, 2024, 1:49pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954/3 "2024-06-06T13:49:01Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![B0B](https://avatars.discourse-cdn.com/v4/letter/b/34f0e0/32.png) [@B0B](https://racket.discourse.group/u/B0B)\
**Post date:** [June 6, 2024, 3:08pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954/4 "2024-06-06T15:08:39Z")

</div>

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:

```scheme
  [-------------------------- 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?

---

<div class="post-metadata">

**Author:** ![robby](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/robby/32/7_2.png) [@robby](https://racket.discourse.group/u/robby)\
**Post date:** [June 6, 2024, 5:18pm UTC](https://racket.discourse.group/t/how-to-type-amb-in-the-redex-exercise/2954/5 "2024-06-06T17:18:43Z")

</div>

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!)