Syntax for Typechecked Values

hostilefork · September 8, 2024, 12:45am

One of the things you can do with Generalized Accessors, is that assignments to any value can be typechecked. You get this "for free" because accessors pair a function with a variable slot, and that function can use typechecking:

Writing the accessor boilerplate is laborious...

checked: accessor lambda [^:value [your! types! here!] <static> actual] [
    either value [actual: value.] [actual.]  ; terminal dot allows unset vars
]

If you want to be truly generic and support storing actions in the variable, you need slashes:

checked: accessor lambda [^:/value [your! types! here!] <static> actual] [
    either value [/actual: value.] [actual.]
]

Not only is that a nuisance to get typechecking, it's also not native code, so you're running that EITHER and its branches.

So we could make it a feature of ACCESSOR, maybe just when you give it a block...and it could do a particularly cheap and special form. I think this is actually the right way to go about it... it would put a "pairing" cell in the variable's location, which would pair up the stored value with a PARAMETER! (which does preoptimized calculations on the typeset:

checked: accessor [your! types! here!]
checked: initial-value

That's all fine and good but seems we need a shorter way to say it...that doesn't repeat the variable name and doesn't have to say ACCESSOR.

We want whatever this is to still get collected as a SET-WORD! (if it is one), so this probably has to be something like:

checked: typed [your! types! here!] initial-value

I don't hate it. Alternate ideas?

Interaction With Syntax For Locals

This would now be able to work:

foo: func [x [text!] <local> y [integer!]] [...]

This would need to be lenient in terms of letting the Y be unset prior to its first assignment. So it can contain nothing at the outset, but any future assignments have to assign integers.

But this would get a bit of a problem if we want to mix it with a form that lets you assign the local:

foo: func [x [text!] <local> y: [integer!]] [...]

That would give you Y with the BLOCK! [integer!] in it. You'd have to say:

foo: func [x [text!] <local> y: typed [integer!] 10] [...]

We could keep the historical "groups to initialize" idea

foo: func [x [text!] <local> y (10)] [...]  ; not typechecked

foo: func [x [text!] <local> y [integer!] (10)] [...]  ; typechecked

And maybe the idea of making a place to put the type constraints vindicates that syntax for this context.

Typechecking will slow down the code. But it would be running through the same checking mechanisms that functions use. As that code got better, so would this.

There could be some sort of "enable typechecking only in debug mode" property of functions where you could turn it on or off.

bradrn · September 8, 2024, 1:03am

I don’t hate it either. But I do have an alternate thought: why not use a sigil? You were wondering what to do with ~~, and this looks like a good opportunity to use it:

checked: initial-value ~~ [your! types! here!]

It doesn’t look that bad to me. Or it could be reversed:

checked: [your! types! here!] ~~ initial-value

(Even better would be ::, which has already been used for the purpose in Haskell. But sadly that’s no longer available.)

hostilefork · September 8, 2024, 1:26am

Mechanically whatever this is has to be in the position after the SET-WORD!

Setting things to the accessor is a special out-of-band operation, that by definition can't be done through the assignment of a normal value:

set-accessor $checked func [...] [...]

So the trick in ACCESSOR is to get the left hand side literally and assign it:

accessor: infix func [
    return: [~]
    var [set-word! set-tuple!]  ; support SET-GROUP! at some point
    action [action?]
][
    set-accessor var get $action
]

Currently I'm having it return nothing. But if it wanted to be "consistent" with what drops out of other SET-WORD!s it would run the accessor and give back whatever the accessor wants to say the value is now.

Actually, these situations that do "weird" things should probably be giving back antiform TAG!. So you still get the ornery response, but with a clarifying message about the weird thing that happened.

accessor: infix func [
    return: [hole?]
    var [set-word! set-tuple!]
    action [action?]
][
    set-accessor var get $action
    return ~<set-accessor succeeded>~  ; mentioning SET-ACCESSOR is useful
]

Anyway... you only get that one unit of lookback to find the variable to bless with this property. So we can't do:

Whatever happens needs the form:

checked: xxx ...

xxx takes 3 arguments: one from the left, two from the right.

So we could put the types after the value.

checked: xxx initial-value [your! types! here!]

And we could require a sigil of some kind with that...as a literal throwaway parameter to help you find the separation point:

checked: xxx initial-value :: [your! types! here!]

But so long as the XXX is there, I don't see the value in it.

~~ and :: are still available, and we could do:

checked: :: [your! types! here!] initial-value

checked: ~~ [your! types! here!] initial-value

But I don't particularly like the :: after the :

We do control the gathering, so could theoretically make it look for non-SET-WORD! patterns, and the :: sigil can't be reassigned, letting the :: imply assignment:

checked :: [your! types! here!] initial-value

But that's one of those irregularities that doesn't really buy enough to make it worth it.

TYPED is a Rebol-y enough thing that you can abbreviate to T or something if you like.

T: typed.

checked: T [your! types! here!] initial-value

But usually there's higher return factorings you can do if you're repeating yourself a lot.

bradrn · September 8, 2024, 1:31am

Ah, I didn’t realise it had to be next to the SET-WORD!. I guess checked: ~~ type! value is acceptable, though I don’t love it.

But… I just had another idea: now that we have CHAIN!, why not co-opt the SET-WORD! itself?

checked:your!:types!:here!: initial-value

Or perhaps, if this is syntactically valid (which I hope it is):

checked:[your! types! here!]: initial-value

I actually really like this idea, for a couple of reasons:

Within Ren-C, one could say that typechecking is to values as refinements are to functions — a small modification to their behaviour. From this point of view, it makes sense to make their syntax consistent.
Outside Ren-C, colons are very widely used for type signatures. This is consistent with that too.

On the other hand, this syntax could be used for something already. Or simply impossible to fit into current Ren-C. I don’t know.

EDIT: Another thought on this — it could be extended to GET-WORD!s too, if that syntax isn’t already taken. :value:type! could mean, ‘get value and assert it has type type!’. Could be useful to have for some tricky situations.

hostilefork · September 8, 2024, 1:37am

bradrn:

now that we have CHAIN!, why not co-opt the SET-WORD! itself?
checked:your!:types!:here!: initial-value
Or perhaps, if this is syntactically valid (which I hope it is):
checked:[your! types! here!]: initial-value

That would be possible. It looks a bit like a function call notation being a CHAIN!, but by ending in : it is differentiated.

Syntax coloring could make it clear (through bolding the whole thing) that it was an assignment.

It would help with the locals problem...

foo: func [x [text!] <local> y:[integer!]: 10] [...]`

Though it deviates from the argument spec which just uses space in the dialect, it's a different section.

We can try it. But TYPED could also be available if one wanted it (or wanted to build some variation that was similar-to, but not exactly the same).

bradrn · September 8, 2024, 1:38am

Well, it could be made an option in the argument spec too, for those who like the syntax (or dislike square brackets):

foo: func [x:text! <local> y:integer!: 10] […]

I like the lightness of it.

hostilefork · September 8, 2024, 1:46am

In terms of "Object Field Gathering Rules", this means taking the old rule:

"look for length 2 CHAIN! with WORD! at head and terminal BLANK!"  ("SET-WORD?")

And turns it into:

"look for any length CHAIN! with WORD! at head and BLANK! at tail"

For this to be useful, the meaning of all WORD!-headed, BLANK!-tailed CHAIN!s (conceptually SET-CHAIN!, though that's not a fundamental type, could be a constraint e.g. SET-CHAIN?)...must have the contents of the chain pertain to some constraint or property of that WORD! at the head.

(As is always the case, these are evaluator rules. In your dialect, means whatever you want.)

Curiously, you can change the typing of your variables midstream in code if you want.

 var:integer!: 10
 var: 20
 ; var: "hello" would be an error

 var:[integer! text!]: var  ; should there be a syntax for retype, but keep value?
 var: 30
 var: "goodbye"

hostilefork · September 8, 2024, 2:06am

It may be that TYPED not take an initial value by default, but typecheck the value in its current state if not unset...

var:integer!: 10
var: 20
; var: "hello" would be an error

var: typed [integer! text!]  ; == 20 ?
assert [var = 20]
var: 30
var: "goodbye"

Also better than a CHAIN! when you have line breaks and want to explain things:

 state: typed [
     integer!    ; if state is integer, we are exiting (UNIX exit status)
     tag!        ; a TAG! is used for non-terminal states
     issue!      ; issue is used for terminal states
     ...
 ]

If that goes on for a while, you might be better to not have a dangling thing to assign at the end bracket, but do a separate assignment.

hostilefork · September 8, 2024, 2:45am

So there are two senses of type checking, the checking of what you get into that function, and whether you want that to be applied to changes to the frame variable once you get it.

(The practice of using function arguments destructively is part of Rebol's pursuit-of-"efficiency" history, although it makes debugging harder.)

Rebol has only had the first form (checking arguments) with no checking after that.

Now that we'll be having the ability to do the checking after, this could be a notational way of distingiushing the two, saying you actually want modifications to keep the type of the argument in that set.

bradrn · September 8, 2024, 2:47am

Hmm… yeah, that seems reasonable to me.

hostilefork · September 9, 2024, 7:08pm

It looks like Red has looked into "typed contexts", and discussed some of the syntax issues there:

github.com/red/REP

Typed contexts

opened 09:38PM - 21 Apr 23 UTC

dockimbel

Discussion

After the changes made in the `apply` branch on red/red repo, it is now possible… to add an array of typesets to Red contexts, so that additional type-checking can be enforced for datatypes relying on contexts. Such extra checks would help make Red code more robust when needed and ease debugging. Such extra typing is an optional feature, the current untyped versions are still allowed. # Typed function contexts * Arguments are type-checked at function call (no change on that). * All function spec words could be type-checked on word setting (new feature). Example: ``` foo: func [a [integer!] b /local c [string!] d [integer!]][ a: none ; error! c: 'hi ; error! ] foo 1 27 ; type-checking arguments ``` That strict type-checking for argument words is not back-compatible with words setting semantics in "non-typed" functions. So, we would need to explicitly specify when we want type-checking on each set-word inside the function's body (including when words are set using `set`, as long as they are bound to a typed function or typed object). Proposal: use `typed` or `strict` attribute to force type-checking on word setting. ``` foo: func [[typed] a [integer!] b /local c [string!] d [integer!]][ a: none ; error! c: 'hi ; error! ] foo 1 27 ; type-check ``` So without such attribute, usual word setting semantics is preserved (local words type spec in such case would be ignored): ``` foo: func [a [integer!] b /local c [string!] d [integer!]][ a: none ; allowed c: 'hi ; allowed ] foo 1 27 ; type-check ``` The implementation cost for such feature is very low, as all word settings boil down to a call to `_context/set-in` function, which can be trivially extended to check the corresponding typeset. ### General questions 1. What is the default value of typed local words? We either need to allow `none` as a preset value, or provide a way to specify default values (can be tedious in practice)? # Typed object contexts The implementation cost is the same as for typed functions. Though, coming up with a clear, intuitive and minimal syntax is challenging. Here are several propositions: In several of the propositions, we need a flag to mark the fact that the object needs to be processed for type information. Convention: ``` <flag>: @typed | [typed] ``` ### 1. Prefixed inline type spec ``` make object! [ <flag> [string!] name: "John" [integer!] age: 25 [string!] city: "Boston" ] ``` Pros: * Evaluation-transparent. * Keeps set-words with their referred value together (good readability). Cons: * Reversed type/word order compared to function spec. * Possible multiple conflicting type specs for same word. ### 2. Infixed inline type spec ``` make object! [ <flag> name: [string!] "John" age: [integer!] 25 city: [string!] "Boston" ] ``` Pros: * Consistent type definition order with function spec block. Cons: * Possible multiple conflicting type specs for same word. * Body block needs to be modified to be able to evaluate it, which is costly (many values removal needed) * Type spec blocks can be confused with valid data. (Though, risks can be reduced by adding an extra marker, like `#type` inside or outside each spec block.) * Values are not directly following their assigned word. With long type definition, values can be pushed far away on the right. (bad readability) ### 3. Postfix inline type spec ``` make object! [ <flag> name: "John" [string!] age: 25 [integer!] city: "Boston" [string!] ] ``` Pros: * Evaluation-transparent. * Loosely consistent type definition order with function spec block. * Keeps set-words with their referred value together (good readability). Cons: * Type spec blocks cannot be reliably located! (e.g. `name: foo 123 [string!]`, is it a spec block or an argument to `foo`?). (Though, risks can be reduced by adding an extra marker, like `#type` inside or outside each spec block.) * Possible multiple conflicting type specs for same word. * With long or multi-line expressions, type spec block can be pushed far away right or down, beyond visibility (very bad readability). ### 4. Spec block as first value ``` make object! [ [name: city: [string!] age: [integer!]] name: "John" age: 25 city: "Boston" ] ``` Pros: * Evaluation-transparent. * Follows the attribute model in function spec block or in callbacks body blocks (e.g. filter block in event callbacks). * Does not require a special flag/attribute value to notify the object constructor that fields can be typed. * Multiple words can share the same type spec (enforces DRY principle). * Up front list of object's words (can improve readability for big objects). Cons: * Double definition, problem for keeping in sync spec and body code (e.g. spec words not used in body block). ### 5. Prototype typed object Let's add a new `declare` constructor function that takes a typed object spec and returns an object value with all fields preset to `none` (except for functions), ready to be used as a prototype for new typed objects. Internally, symbol and type arrays could be shared by default, as long as the context is not extended with new symbols. ``` obj: declare [name: city: [string!] age: [integer!] foo: func [...][...]] make obj [ name: "John" age: 25 city: "Boston" foo: func [...][...] ] ``` Pros: * Clean separation between specification and instantiation/evaluation. * Same approach can be used for struct! values too. * Could be evolved to implement a full class-based model. Cons: * Requires a new literal form for serialization round-trip! (Text serialization could drop typing info entirely, leaving it to Redbin for accurate serialization.) * How to specify the type spec for new words for an object extending a typed proto? (The rule could be that extra words created that way are untyped.) * Adds a new mezz/native to the core language. ### General questions 1. How to solve conflicting type definitions on multiple inheritance? (Should not happen in 5. as the proto object is the one providing the typing information.) 2. What is the default value of typed local words? We either need to allow `none` as a preset value, or provide a way to specify default values (can be tedious in practice)? 3. Allow changing typesets on a given word? (Personally, I think the stricter the rule in typing, the simpler it is for end users.) 4. `function!` values should not need to be typed, though, a typed object could protect such word of `function!` type from being modified to a different datatype. 5. How much the new typed object syntax needs to be back-compatible with untyped objects? 6. Should typed object also support a way to specify words protection from modification or should that be deferred to `protect/unprotect` functions? 7. Could the selected typed object syntax provide a clean way to support specifying object event handlers? (The current `on-change*/on-deep-change*` convention has always been temporary until a better solution is found.) ## References * http://www.rebol.net/cgi-bin/r3blog.r?view=0016#comments

Seems that their lack of CHAIN! to unify the type with the declaration forces them to choose between various bad options.

hostilefork · June 25, 2025, 3:17pm

bradrn:

hostilefork:
Mechanically whatever this is has to be in the position after the SET-WORD!

Setting things to the accessor is a special out-of-band operation, that by definition can't be done through the assignment of a normal value:
set-accessor $checked func [...] [...]
So the trick in ACCESSOR is to get the left hand side literally and assign it:
Ah, I didn’t realise it had to be next to the SET-WORD!. I guess checked: ~~ type! value is acceptable, though I don’t love it.

So there's a new possibility on the table now, which is the trick of using PACK! to slipstream "dual" states into the normal SET machinery.

I explained early on the reason why PACK! holds lifted values... it's because it needs to be able to represent antiforms, inside a BLOCK! structure. So QUOTED! means it's not an antiform (just whatever the quoted thing is, one level removed), and QUASIFORM! means it's an antiform:

>> [a b]: pack [1020 ~null~]
== \~['1020 ~null~]~\  ; antiform (pack!)

>> a
== 1020

>> b
== \~null~\  ; antiform

But hold on a minute... this means that non-antiform, non-quasiform states are available in PACK!. This is the "dual band"... where states like "true unset", or GETTER functions, or SETTER functions... or typechecked values live.

A typechecked value indicator could be simply a BLOCK! with a PARAMETER! and a lifted value in it. So... what if functions could return that as a PACK! item?

The TYPED function could return a 1-element PACK!, with a plain BLOCK! (not QUOTED!, not QUASIFORM!) in it.

>> typed [integer! tag!] 1020
== \~[[&[parameter! [integer! tag!]] '1020]]~\  ; antiform

If things like SET and SET-WORD!/SET-BLOCK! interpreted this to mean "assign in the dual band", we get some pretty wild possibilities.

It cracks open the door for multiple assignment of typed values:

>> x: y: z: typed [integer! tag!] 1020
== \~[[&[parameter! [integer! tag!]] '1020]]~\  ; antiform

>> z: <good>
== <demo>

>> z: [not good]
** Panic: Z has type constraint [integer! tag!]

>> x: <good>
== <good>

>> x: [not good]
** Panic: X has type constraint [integer! tag!]

And just in general, it makes it possible to abstract things like TYPED--and build more things like them easily.

To Returning Dual Band Values

Cool as this seems, it's a subversion of what I thought was the "rule"... that evaluations cannot return dual band values.

Mechanically that's still true. A PACK! is not dual band.

But conceptually it's kind of strange that a function can return a "state" to you that can get absorbed into a variable and constrain how that variable acts... just through the normal mechanics of assignment (var: ...) and not some special operation in which you have to be complicit (tweak $var ...)

However... once you find the chains restricting and invent infix function hacks to work around this in syntax, you've already crossed the line to trying to make it look like you're doing an assignment of a dual-band property.

 >> x: (print "Might as well actually work..." typed [integer! tag!] 1020)
 Might as well actually work...
 == \~[[&[parameter! [integer! tag!]] '1020]]~\  ; antiform

 >> x
 1020

 >> x: [with great power comes great conundrums]
 ** Panic: X has type constraint [integer! tag!]

But Not All Dual Band Signals Should Work...

Some dual-band signals accepted by TWEAK, e.g. the PROTECT or UNPROTECT signals, do not belong in PACK! as something that you can assign.

>> x: ~[protect]~
== ???

Semantically, the product of an assignment expression should always be whatever was on the right-hand side. And you don't want an assignment to X to synthesize something that's not reflective of the value of X.

It's reasonable to argue that a TYPED pack result could decay to the typed value without a problem:

>> 1020 = x: typed [integer! tag!] 1020
== \~okay~\  ; antiform

But... let's say UNSET tried to switch to being one of these dual pack things:

>> unset
== \~[*unset*]~\  ; antiform

>> x: unset
== \~[*unset*]~\  ; antiform

That's great, but what does it decay to? It can't decay, it's less than nothing.

So basically you have to throw it away at some point. The evaluator just has to toss it without trying to decay it if you never use it in a non-assignment expression:

>> 1 + 2 unset 3 + 4
== 7

How About ACCESSOR (GETTER, SETTER...)

Generic accessors are raising a lot of questions.

My gut instinct is they're going to be more in the category of things like the protect/unprotect signals, where you need to use TWEAK, and the infix hacks, vs. be able to make something semantically coherent out of the pack trick.

I don't know yet. Type checking is the poster child for SETTER, but specializing it has advantages in performance as well as semantics (always same value out as in), so I'm going to try hammering that out first.

hostilefork · December 30, 2025, 3:34pm

Another typechecking concept would be "I'm assigning a value of the type I want to constrain this to, use that type".

This might be the right sense for the word TYPED.

>> x: typed 1020
== 1020

>> x: 304
== 304

>> x: "string"
** PANIC: X is typed [integer!], tried to assign ~{text!}~

And maybe CONSTRAIN is used for assignments. It might even be better to do it on the outside:

constrain [integer! tag!] x: 1000 + 20

So it would be arity-3, quote the SET-WORD and take its third parameter evaluatively, then do the dual assignment.

It could be variadic, like LET, and allow you to constrain without assigning.

constrain [integer! tag!] x

Maybe it should use a $ on that so you get a better idea of what's going on?

constrain [integer! tag!] $x

Though may be not. The reason LET doesn't do it is that let [$x y]: pack [1 2] means "don't create a new variable for X, only Y. So presumably let $x needs to be consistent with that.

(I doubt it would be very frequent you'd want to use the non-assigning form.)

bradrn:

checked: initial-value ~~ [your! types! here!]
It doesn’t look that bad to me. Or it could be reversed:
checked: [your! types! here!] ~~ initial-value
(Even better would be ::, which has already been used for the purpose in Haskell. But sadly that’s no longer available.)

So :: is available now, as a WORD! (just a weird one you can't put in CHAIN!s)

(As an aside, ~~ is no longer available, as it is a quasi-blank of two space characters. You can dialect it, but its evaluator behavior is fixed to produce its antiform...although RebindableSyntax for QUASIFORM! could change that...)

And I've described the possible backdoor mechanic for putting unlifted states in a PACK! and having that be the way to assign "duals".

checked: 0 :: [your! types! here!]

checked: [your! types! here!] :: 0

If this were to be done, I think I like it better when the types are after. It sort of follows that news-story writing principle that you don't want to mislead people who only read the first part.

There's a bit of an issue if the value is on the left, due to infix... but you can make the operator INFIX:POSTPONE and it should work.

bradrn:

I just had another idea: now that we have CHAIN!, why not co-opt the SET-WORD! itself?
checked:your!:types!:here!: initial-value
Or perhaps, if this is syntactically valid (which I hope it is):

checked:[your! types! here!]: initial-value

Think I'm going to have to pan this notational concept, due to what it does to the logic of locals gathering. It makes it not as easy to spot things that need to be collected. Having a more complex rule is not desirable--we need to be able to spot the SET-WORD.

Also, it's more contentious with dialected function calls.

TYPED, CONSTRAIN and :: could probably cover most cases, and all authorable in usermode... with people able to create their own concepts.

hostilefork · December 30, 2025, 3:41pm

If PACK!s are able to carry duals via the unlifted band, the notion I've talked about elsewhere is what do you get with multiple assignments:

x: y: typed 1020

Is X constrained? Or just Y?

This is tricky, but it may be that we just have to say that X does get constrained too... and if you don't want that you have to do something like:

x: decay y: typed 1020

And then a typechecking dual decays to the value.