From ab6608063d2c7aaa948f4c48f77ba111c9cfcd83 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 10 Oct 2023 15:22:10 -0400 Subject: [PATCH] update description of validation in RFC 5 --- text/0005-is-operator.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/text/0005-is-operator.md b/text/0005-is-operator.md index 329ae832..d25d9f7a 100644 --- a/text/0005-is-operator.md +++ b/text/0005-is-operator.md @@ -94,8 +94,9 @@ Namespaces are considered "part of" the entity type. So: ### Changes required to validator -`e is et` will be typed as `True` if the validator can guarantee that expression `e` is an entity of type `et`, or `False` if the validator can guarantee that `e` is a non-entity type or an entity not of type `et`. -Otherwise, the validator gives `e is et` type `Bool`. +`e is et` will be typed as `True` if the validator can guarantee that expression `e` is an entity of type `et`, or `False` if the validator can guarantee that `e` is an entity not of type `et`. +If the validator can guarantee that `e` is an entity, but not determine the exact type, then `e is et` is given type `Bool`. +Otherwise, the validator produces a type error. To improve typing precision, we can extend the current notion of "effects" to track information about entity types. Currently, the validator uses effects to know whether an expression is guaranteed to have an attribute.