question: are refinement types viable?

what

Refined types allow producing new types by limiting some values of the base type by predicates.

Wuffs is one industry-successful example of an application. Jolie is something like WIT, but not popular.

I do not know what the exact best syntax is,
or if it should be mixed with attributes.

Most typical refinements are ranges, and possibly we can define a dictionary via refinements too.

I will share some examples, and then some reflection on who should validate refinement.

examples

type a = u8; // unrefined base type
type b = u8  where range(1..42]; // refined type, assumed 8-bit on the wire and in mem, but limited in usage
type c = u32 where range[1..42]; // refined type, different from b by size in mem or on the wire

record x {
   a: a,
   b: c,
}

type z = list<(a, b)> where sorted by 0; # sorted by tuple property of its first element

type y = list<x> where sorted by a; # just sorted, in any direction

type k = list<x> where sorted asc by a; # sorted asc

type u = list<x> where sorted by a, b; # sorted by a and by b

type d = list<x> where sorted by a unique by a; # dictionary

type o = x where a < b; // some equality for a and b to be possible

type l = list<u8> where length(2..42);

type p  = x where a + b < u64::MAX ; // fails to compile because max cannot be reached ever

type t = x where  a + b < 4096;

how to validate

Validating numeric ranges is easy.

Validating sorted is easy too; the first 2 elements define order.

Requires < or > refinements too (need to do comparison for sortedness).

Sorted can be desc or asc if needed.

Sorted unique is also easy to validate.

IMHO it should fail to allow defining unique but not sorted, at least feature-gate it behind a DDoS flag :).

who to validate

By default, nobody should validate; there is no spec.

If the reader trusts the writer of ABI, then the reader does not need to validate.

If the reader does not trust the writer, it should validate.

The wit-bindgen generator can generate code, or the reader can do manual validation.

Wit-bindgen can validate data provided by the writer, maybe in debug mode.

type system

It may be safe to allow validation only of fixed-size entities by default, other features gated.
Except length, it specifically for variable length.

Generators for target languages which support some kind of narrowing,
for example via inheritance.
Can generate code for each refinement type, and allow a function for a broader type to receive a more narrow type.
Implementer which reads refined type data, can decide to store refined u8 in u5 as part of some stucture if that fits, for example.

But that is optional to add type safety to targets.

So refinements act as:

- documentation (always)
- generation of validator for reader or writer (optional)
- for type systems of target languages (optional)

Refinements will be less ad hoc and more clear, rather than people start put refinements into https://github.com/WebAssembly/component-model/issues/58 .

options

Seems Wuffs and https://github.com/dfinity/candid/blob/master/spec/Candid.md and Jolie do not come with dependent types.

So many of validation types are attempts on refinements.

WIT does not have in place backward compatiblity. Protobuf has it implicitly embedded and ad hoc.
Candid has has in place versioning, but seems it pays with extra bytes https://github.com/dfinity/candid/blob/master/spec/Candid.md.
May be refinements give other option for versioning without binary overhead.

links

https://en.wikipedia.org/wiki/Refinement_type
https://www.jolie-lang.org/index.html
https://github.com/google/wuffs/blob/main/doc/glossary.md#refinement-type
https://www.reddit.com/r/dependent_types/comments/ay7d86/what_can_refinement_types_do_that_dependent_types/
https://ucsd-progsys.github.io/liquidhaskell/
https://json-schema.org/understanding-json-schema/reference
https://zod.dev/
https://github.com/gcanti/io-ts
https://github.com/stefan-hoeck/idris2-refined/blob/main/docs/src/Intro.md
https://dafny.org/dafny/DafnyRef/DafnyRef#sec-module-refinement
https://flux-rs.github.io/flux/
https://plv.mpi-sws.org/refinedrust/
https://github.com/microsoft/TypeScript/issues/43505
https://github.com/Microsoft/TypeScript/issues/4895
https://fstar-lang.org/tutorial/book/part1/part1_getting_off_the_ground.html
https://www.w3.org/TR/xmlschema11-1/
https://smithy.io/2.0/spec/constraint-traits.html
https://yoric.github.io/post/rust-refinement-types/

Start by reviewing the proposed WIT syntax and the related component-model issue 58, then compare the refinement approaches and validation responsibilities described here. Done would require a decided design and agreed scope for refinement types, rather than a self-contained code change.