[boltyx0]

Interesting approach to constraining what agents can express syntactically. I've been thinking about a related but different problem: it's not just about how agents write code, it's about what they do at runtime. I've been building agents that call external APIs (ticket systems, chat tools, cloud infra) and the bigger risk I keep hitting isn't bad code, it's bad data flowing through correct code. An agent can write perfectly valid, type-safe code that reads a customer record and posts it somewhere, and the code is fine but the payload has an SSN in it. Curious whether Sigil's contract system could extend to runtime data constraints on API call payloads, not just function inputs. Like requires payload contains no PII as a contract on an external call. That would be genuinely novel.

[inerte]

I haven't solved runtime data yet. Every time I try, my tendency to demand everything during compile time ends up with me adding an additional compiler rule, and kicking off the can down the road.

When I added type constraints, it fit really well with validating values. If you specify:

  t BirthYear=Int where value>1800

Then it's pretty obvious if you get 1500 you can throw an error, and I considered doing it, but didn't want to tackle runtime validation at the time.

Maybe dealing specifically with "never send PII to the outside world", there are possible 3 things Sigil could have.

Since Effects are explicit (and Http and Filesystem are effects in Sigil), maybe validate before the effect is performed by calling a function to see if a particular type (Ssn) is not empty or straight up validate the value of every field.

Or with topologies, which is Sigil's way to specify external dependencies (I am not considering the filesystem one here). Same idea as effects, somewhere during the data flow some kinda of validation happens.

Maybe a third way would be to be able on a Type, specify where the data can go to. Something like:

  t Ssn=String where isValidSsn(value) transit logApi

`transit` in this case can tell where this type can live. Then, we can validate during compilation time if `Ssn` is only going to `logApi`, and not to the `mailApi` or any other external dependency.

Thanks for the suggestion, I will explore this idea.

[inerte]

So, an update, I took at stab and came up with this: https://inerte.github.io/sigil/articles/labelled-types-and-b...