René's URL Explorer Experiment

Title: Compile-time refinement type for validation · Issue #194 · rowscript/rowscript · GitHub

Open Graph Title: Compile-time refinement type for validation · Issue #194 · rowscript/rowscript

X Title: Compile-time refinement type for validation · Issue #194 · rowscript/rowscript

Description: This issue describes a raw user requirement for an existing feature request, i.e., #34. As our user suggests, one should use type refinement to eliminate error-prone uses of types, like this: type User = { id: number.ge(0) // greater or ...

Open Graph Description: This issue describes a raw user requirement for an existing feature request, i.e., #34. As our user suggests, one should use type refinement to eliminate error-prone uses of types, like this: type ...

X Description: This issue describes a raw user requirement for an existing feature request, i.e., #34. As our user suggests, one should use type refinement to eliminate error-prone uses of types, like this: type ...

Opengraph URL: https://github.com/rowscript/rowscript/issues/194

X: @github

direct link

Domain: github.com

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Compile-time refinement type for validation","articleBody":"This issue describes a raw user requirement for an existing feature request, i.e., #34.\n\nAs our user suggests, one should use type refinement to eliminate error-prone uses of types, like this:\n\n```ts\ntype User = {\n    id: number.ge(0) // greater or equal to 0\n};\n\ntype Admin = {\n    id: typeof(Usesr::id).lt(100) // less than 100, but greater or equal to 0\n};\n```\n\n* The predicate type should be flexible to place.\n* Proof terms should be easy to manipulate, automatically or manually.\n\nFor my own reference, Lean 4's [Subtype](https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Subtype) looks pretty much like the extension type we're looking for. Should investigate and cross-examine the usability of both.","author":{"url":"https://github.com/anqur","@type":"Person","name":"anqur"},"datePublished":"2025-04-27T07:37:06Z","url":"https://github.com/rowscript/rowscript/issues/194"}

Links:

Viewport: width=device-width