Types and refinement

Every position in an Argon program has a type, and the type system answers one question at a time: may a value of type A stand where a value of type B is expected? The answer is governed by subtyping. On top of subtyping sits refinement — carving a concept into a narrower one by attaching a predicate — where the type system’s central choice falls: whether that predicate defines membership or merely constrains it.