# Tip: pitfalls with using \`in\` for typechecking

**URL:** <https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420>\
**Category:** Alloy 6\
**Created:** [December 14, 2023, 10:01pm UTC](https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420 "2023-12-14T22:01:57Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![hwayne](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/hwayne/32/67_2.png) [@hwayne](https://alloytools.discourse.group/u/hwayne)\
**Post date:** [December 14, 2023, 10:01pm UTC](https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420/1 "2023-12-14T22:01:57Z")

</div>

Say you have this:

```auto
sig Person {
  pet: lone Animal
}

abstract sig Animal {}
sig Cat, Dog, Bird extends Animal {}

```

You want to check if `alice` has a Dog. The obvious thing to do would be

```auto
alice.pet in Dog

```

Be careful! Since `pet` is `lone`, it’s possible that alice _doesn’t have_ a pet, in which case `alie.pet in Dog` is true!

If you actually want to check “alice’s pet is a Dog”, you instead have to write

```auto
some alice.pet & Dog

```

This problem cropped up in a couple of models I’m working on, so this is a PSA about it 🙂

(I had a similar problem with `foo.bar = baz.qux` when both were empty, I needed `some foo.bar & baz.qux` instead.)

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [December 15, 2023, 7:34pm UTC](https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420/2 "2023-12-15T19:34:13Z")

</div>

Yes! Note that the claim that S is a subset of T is conventionally written in logic as

`all e: univ | e in S implies e in T`

which becomes vacuously true when S is empty. This treatment of partial functions and empty sets is one of Alloy’s key innovations, and it avoids the nastiness of undefined values that complicated many languages before Alloy.

For those not familiar with that whole rats nest, consider that the formula

`some p: Person | p.dog = Rex`

becomes undefined in most standard logics if there is any person who doesn’t have a dog, even if Rex is Alice’s dog!

A downside of this is indeed that you need to sometimes strengthen a constraint if you don’t want to subsume the empty case. In an early version of Alloy there was a special operator that you could use to say S is a non-empty subset of T, but I can’t remember what it was. It was a bad idea anyway :-).

---

<div class="post-metadata">

**Author:** ![mica](https://avatars.discourse-cdn.com/v4/letter/m/85e7bf/32.png) [@mica](https://alloytools.discourse.group/u/mica)\
**Post date:** [January 10, 2024, 10:55am UTC](https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420/3 "2024-01-10T10:55:30Z")

</div>

Hitting this pitfall already in Exercise 1.d of Structural design with Alloy in Formal Software Design with Alloy 6.

---

<div class="post-metadata">

**Author:** ![mica](https://avatars.discourse-cdn.com/v4/letter/m/85e7bf/32.png) [@mica](https://alloytools.discourse.group/u/mica)\
**Post date:** [September 13, 2024, 9:04am UTC](https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420/4 "2024-09-13T09:04:05Z")

</div>

Hit this again trying to write a proper temporal model.  
Can we maybe have a lint against this? or is it related to any other vacuous stuff? lol

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [September 14, 2024, 1:13pm UTC](https://alloytools.discourse.group/t/tip-pitfalls-with-using-in-for-typechecking/420/5 "2024-09-14T13:13:22Z")

</div>

Since partial fields (i.e yielding none or set) and joins are so common, you would likely end up with tons of warnings, even when you would have checked beforehand that there’s no risk of vacuousness.