Re: [PATCH] Disallow empty "or" type specifier
> Hi all, > > the attached patch makes the `(or)` type specifier invalid, as opposed > to being simplified to `*`. > This is more consistent with the mathematical interpretation of an empty > (sum) type being the bottom type having no inhabitants. > This is very explicit in OCaml, for example, where the empty type is > literally a sum (variant) of 0 types: `type t = |`. Thanks a lot! I've taken the freedom to push this directly, as the change is trivial and only affects validation of user-supplied type signatures. felix
Re: [PATCH] Disallow empty "or" type specifier
> It certainly shouldn't be *, nor should it be an error... technically an > empty union should be a null set, which would correspond to either a > non-extant type or to no return/value at all... Well, the problem is: there is no non-extant type, no "bottom": we simply use the Scheme type system (slightly extended) that clearly describes what types values can have and in Scheme every value has a type, there are no programs that are unsound on the type level - they may break at run-time, but are still valid Scheme code. There are meta-types like "undefined", which is the same as the union of all possible types, but explicitly declared as undefined by the standard. CHICKEN uses other meta types like "*" for convenience, and "or" and "forall" for limiting the possible set of types a value can have, but there are still very much concrete types for concrete values. The number of return values on the other hand is not a type-related concept, it is an operational thing (the number of arguments to pass to the continuation), so I would not mix these two issues. There can be no "(or)"-typed value in a Scheme system, there can be the absence of a return (like calling a continuation), but that is, I believe, the area of effect systems. felix
Re: [PATCH] Disallow empty "or" type specifier
On Tue, Sep 26, 2023 at 12:33:43PM +0300, elf wrote: > It certainly shouldn't be *, nor should it be an error... technically an > empty union should be a null set, which would correspond to either a > non-extant type or to no return/value at all... We've discussed this on IRC. Such a null type doesn't exist in Scheme, and "no return value" would correspond to a zero "multiple return values", which has a different notation in our type system. The (or) is an individual value, which could occur multiple times in a "multiple return values" list. We don't splice MV values together, so this is either a null type or an error. So in our case, it should definitely be an error since we don't have null types. Cheers, Peter signature.asc Description: PGP signature
Re: [PATCH] Disallow empty "or" type specifier
It certainly shouldn't be *, nor should it be an error... technically an empty union should be a null set, which would correspond to either a non-extant type or to no return/value at all... -elf On 26 September 2023 12:02:56 GMT+03:00, Pietro Cerutti wrote: >Hi all, > >the attached patch makes the `(or)` type specifier invalid, as opposed to >being simplified to `*`. >This is more consistent with the mathematical interpretation of an empty (sum) >type being the bottom type having no inhabitants. >This is very explicit in OCaml, for example, where the empty type is literally >a sum (variant) of 0 types: `type t = |`. >
[PATCH] Disallow empty "or" type specifier
Hi all,
the attached patch makes the `(or)` type specifier invalid, as opposed
to being simplified to `*`.
This is more consistent with the mathematical interpretation of an empty
(sum) type being the bottom type having no inhabitants.
This is very explicit in OCaml, for example, where the empty type is
literally a sum (variant) of 0 types: `type t = |`.
--
Pietro Cerutti
I have pledged to give 10% of income to effective charities
and invite you to join me - https://givingwhatwecan.org
>From 0b1d1a591edbb56054ad2ce7f9627aec5c82 Mon Sep 17 00:00:00 2001
From: Pietro Cerutti
Date: Thu, 21 Sep 2023 12:10:45 +
Subject: [PATCH] Disallow empty "or" type specifier
This fixes an inconsistency in the `or` type specifier when used with an empty
argument list, whereas, contrary to how the `(or)` function is `#f`, the `(or)`
type specifier is `*`.
---
manual/Types| 4 ++--
scrutinizer.scm | 3 ++-
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/manual/Types b/manual/Types
index f3fb6b7b..27ef0fc6 100644
--- a/manual/Types
+++ b/manual/Types
@@ -99,7 +99,7 @@ or {{:}} should follow the syntax given below:
VALUETYPEmeaning
-{{(or VALUETYPE ...)}}"union" or "sum" type
+{{(or VALUETYPE1 VALUETYPE2 ...)}}"union" or "sum"
type
{{(not VALUETYPE)}}non-matching type (*)
{{(struct STRUCTURENAME)}}record structure of given
kind
{{(procedure [NAME] (VALUETYPE ... [#!optional VALUETYPE ...] [#!rest
[VALUETYPE]]) . RESULTS)}}procedure type, optionally with
name
@@ -241,7 +241,7 @@ Procedure types are assumed to be not referentially
transparent and
are assumed to possibly modify locally held state. Using the
{{(... --> ...)}} syntax, you can declare a procedure to not modify
local state, i.e. not causing any side-effects on local variables or
-data contain in local variables. This gives more opportunities for
+data contained in local variables. This gives more opportunities for
optimization but may not be violated or the results are undefined.
diff --git a/scrutinizer.scm b/scrutinizer.scm
index cdf6f205..35f889e2 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -75,7 +75,7 @@
; result specifiers:
;
; SPEC = * | (TYPE1 ...)
-; TYPE = (or TYPE1 ...)
+; TYPE = (or TYPE1 TYPE2 ...)
;| (not TYPE)
;| (struct NAME)
;| (procedure [NAME] (TYPE1 ... [#!optional TYPE1 ...] [#!rest [TYPE |
values]]) . RESULTS)
@@ -1911,6 +1911,7 @@
v))
((eq? 'or (car t))
(and (list? t)
+ (not (null? (cdr t)))
(let ((ts (map validate (cdr t
(and (every identity ts)
`(or ,@ts)
--
2.42.0
