Feat: Remove experimental type refinement

CLAUDE.md

@@ -121,29 +121,6 @@ The call-site "handle" construct for a call that may raise is `<expr> ! where <c
 `f(10) ! where err: MyErr => do ... end end` — the `!` marks the call as fallible and must be consumed before
 looking for `where` (`parse_expr_or_stmt` in `expr_or_stmt.rs`).
 
-### `type` vs `trait`
-
-Both start with `<keyword> X: Parent`, easy to conflate:
-
-- **`type`** is type refinement: narrowing a type by a boolean predicate over `self`.
-  `type X: Parent when <cond>` (or multi-line `when\n <cond>\n...\nend`) is the conditional type alias form
-  (`Node::TypeAlias`, binds `self` to `Parent`). `type X where <defs> end` (no `when`) is the plain
-  interface-signature form (`Node::TypeDef`, no `self`).
-- **`trait`** is an interface (Java/Rust-style): `trait X where <defs> end` / `trait X: Parent where <defs>
-  end` → `Node::Trait` (`parse_trait_def` in `src/parse/class.rs`), parsed like the signature form of `type`
-  but its own AST/`NodeTy` variant. No `when` form — `trait X when ...` is a parse error, use `type` instead.
-
-Wrong keyword, or `when` vs `where`, fails to parse or fails type-checking with a confusing "Undefined
-variable: self".
-
-**⚠️ Experimental.** The checker treats `Trait` and `TypeDef` identically (`Node::TypeDef { .. } |
-Node::Trait { .. }` throughout `src/check`/`src/generate`). Type *refinement* (`when <cond>`) is unenforced:
-`src/generate/convert/class.rs`'s `TypeAlias` codegen emits a plain `typing.NewType(...)` and silently drops
-the condition — nothing checks it at compile time or runtime. Doing this properly needs either
-abstract-interpretation at compile time or runtime checks at every call site (which the language explicitly
-avoids desugaring to); it's not obvious this is achievable in general. Treat `type ... when` as a sketch, not
-a working feature.
-
 ### Class arguments
 
 Class constructor arguments are always fields, stored on `self` — no `def` prefix (`class X(a: Int)`, not

README.md

@@ -28,7 +28,6 @@ This is the Mamba programming language.
 Mamba is similar to Python, but with a few key features:
 
 - Strict static typing rules, but with type inference so it doesn't get in the way too much
-- Type refinement features
 - Null safety
 - Explicit error handling
 - A distinction between mutability and immutability
@@ -280,13 +279,9 @@ These are similar to interfaces in Java and Kotlin, and near identical to traits
 In Mamba, we aim to have many small traits for a more idiomatic way to express the behaviour of objects/classes.
 For those familiar with object-oriented programming, we favour a trait-based system over inheritance (like Rust, Mamba doesn't have inheritance). 
 
-> **Status:** the basic shape works today — `trait Named where def name(self) -> Str end` plus
-> `class Person(name: Str): Named where end` parses, type-checks, and transpiles to an `abc.ABC`-based
-> Python class, exactly like the signature form of `type` (the checker currently treats `trait` and `type`
-> identically, since a trait really is structurally a type interface). Generics (`trait Iterator[T]`), the
-> `def <Trait> for <Class> where ...` external-implementation syntax, composing multiple parent traits, and
-> `meta`/`fin` modifiers — all shown in the examples below — are not implemented yet; only a single optional
-> parent trait via `trait X: Parent where ... end` works.
+> **Note** Generics (`trait Iterator[T]`), the `def <Trait> for <Class> where ...` external-implementation syntax,
+> composing multiple parent traits, and `meta`/`fin` modifiers are not implemented yet;
+> only a single optional parent trait via `trait X: Parent where ... end` works.
 
 Consider example with iterators (which briefly showcases language generics):
 
@@ -325,130 +320,6 @@ E.g.
 trait Ordered[T]: Equality, Comparable
 ```
 
-### 🗃 Type refinement (🇻 0.4.1+) (Experimental!)
-
-> **Status:** this section describes a design, not a shipped feature. Today, `type X: Y when <cond>` parses
-> and type-checks, but the transpiler **silently drops `<cond>` at codegen time** — it currently just emits a
-> plain `typing.NewType("X", Y)`, with no compile-time proof and no runtime check anywhere. None of the
-> `isa PosInt` / `isa InvertibleMatrix` flow-typing examples below are checked or enforced by the compiler
-> yet. We're deliberately keeping `type` (refinement) and `trait` (interfaces, see above) as separate
-> keywords/AST nodes so refinement can grow into this design later without disturbing traits, but whether
-> refinement can be done *well* — soundly, without either a real theorem prover or scattering runtime checks
-> through every call site — is genuinely an open question, and it's possible the honest answer ends up being
-> "no, not in general." Treat everything below as a sketch of where the language might go, not a guarantee.
-
-Mamba also has type refinement features to assign additional properties to types.
-
-Note: Having this as a first-class language feature and incorporating it into the grammar may have benefits, but does increase the complexity of the language.
-Arguably, it might detract from the elegance of the type system as well;
-A different solution could be to just have a dedicated interface baked into the standard library for this purpose.
-
-The general syntax is `type MyType: MainType when <expression>`.
-The expression can be of any form (and size), but **must** evaluate to a boolean.
-
-```mamba
-type SpecialInt: Int where self >= 0 and self <= 100 or self mod 2 = 0
-```
-
-_Note on performance: In terms of correctness, the order of the conjunctions obviously doesn't matter, but those who care about performance should know they are evaluated in order, so best to have simple ones first._
-
-```mamba
-type SpecialInt: Int when
-    self >= 0
-    self <= 100 or self mod 2 = 0
-end
-```
-
-Type refinement also allows us to specify the domain and co-domain of a function, say, one that only takes and returns positive integers:
-
-```mamba
-# we list the conditions below, which are a list of boolean expressions.
-# this first-class language feature desugars to an list of checks which are done at the call site.
-# we avoid desugaring to a function (at least when transpiling to Python) as to not clash with existing functions.
-type PosInt: Int when self >= 0
-
-def factorial(x: PosInt) -> PosInt := match x with
-    0 => 1
-    n => n * factorial(n - 1)
-end
-```
-
-At the call site, one could do
-
-```mamba
-def x := -42 # some value
-
-# currently this is a compilation error, x is type Int
-# we cannot yet evaluate refined types at compile time, only runtime
-# factorial(x) # error: 'x' is type Int, but signature is factorial(PosInt)
-
-if x isa PosInt then
-    print(factorial(x))
-else
-    print("x must be positive")
-```
-In short, types allow us to specify the domain and co-domain of functions with regards to the type of input, say, `Int` or `Str`.
-
-Let's expand our matrix example from above, and rewrite it slightly:
-
-```mamba
-type InvertibleMatrix: Matrix when self.determinant() != 0.0
-
-class MatrixErr(message: Str): Exception(message)
-
-## Matrix, which now takes floats as argument
-class Matrix2x2(a: Float, b: Float, c: Float, d: Float) where
-    def _last_op: Str? := None
-
-    def determinant(fin self) -> Float := self.a * self.d - self.b * self.c
-
-    def inverse(self: InvertibleMatrix) -> Matrix := do
-        def det := self.determinant()
-        self._last_op := "inverse"
-
-        Matrix(self.d / det, -self.b / det, -self.c / det, self.a / det)
-    end
-
-    def last_op(fin self) -> Str ! MatrixErr :=
-        if self._last_op != None then self._last_op
-        else ! MatrixErr("No operation performed")
-end
-```
-
-Within the then branch of the if statement, we know that `self._last_message` is a `Str`.
-This is because we performed a check in the if condition.
-
-We now define the type of `self`.
-Each type effectively denotes another state that `self` can be in.
-For each type, we use `when` to show that it is a type refinement, which certain conditions.
-
-```mamba
-def m := Matrix(1.0, 2.0, 3.0, 4.0)
-
-if m isa InvertibleMatrix then do
-    def m_inv := m.inverse()
-    print("Original matrix: {m}")
-    print("Inverse: {m_inv}")
-end else
-    print("Matrix is singular (not invertible).")
-
-def last_op = m.last_op()!
-print("Last operation was: {last_op}")
-```
-
-Type refinement, in the context of object-oriented programming, thus allows us to also explicitly name the possible states of an object. 
-This means that we don't constantly have to check that certain conditions hold.
-We can simply ask whether a given object is a certain state by checking whether it is a certain type.
-
-In general, the goal of the compiler will become:
-
-- Limit the amount of checks that need to be done
-- Detect when it becomes impossible to raise an exception, i.e. if it is impossible to break an invariant then we will never raise an exception.
-
-Overall, the goal of type refinement is to allow us to express in greater detail the expected behaviour of functions in a more concise manner.
-This is somewhat similar to "design by contract", though baked more into the language itself.
-This should help us to express more clearly domains and codomains of functions.
-
 ### 🔒 Pure functions (🇻 0.4.1+)
 
 Mamba has features to ensure that functions are pure, meaning that if `x = y`, for a pure function `f`, `f(x) = f(y)`.

docs/spec/grammar.md

@@ -16,10 +16,6 @@ The grammar of the language in Extended Backus-Naur Form (EBNF).
                          ( import-as | "{" import-as "," "}" | "{" import-as "," import-as { "," import-as } "}" )
     import-as        ::= id ( "as" id )
 
-    # type refinement, experimental: "when" parses and type-checks but conditions go unenforced
-    type-def         ::= "type" type-not-fun [ ":" type-not-fun ] ( "when" conditions | [ code-set ] )
-    conditions       ::= expression | newline { expression newline } "end"
-    # interface, a la Java/Rust traits; only a single optional parent for now
     trait-def        ::= "trait" type-not-fun [ ":" type-not-fun ] [ code-set ]
     class-def        ::= "class" type-not-fun [ fun-args ] [ ":" type-not-fun ] [ code-set ]
 

docs/spec/keywords.md

@@ -18,10 +18,8 @@ Keyword | Use
 
 Keyword | Use
 ---|---
-`type`  | Type refinement: a conditional type alias (`when`), or a plain interface-signature body (experimental — see README "Type refinement")
 `trait` | Denote an interface (à la Java interfaces / Rust traits), which a `class` can implement
 `class` | Denote a class
-`isa`   | Check whether an object is an instance of a class
 `when`  | Conditional types (used with `type`, not `trait`)
 
 ## Classes and Utils

src/backend/python/convert/class.rs

@@ -25,22 +25,7 @@ use crate::{ASTTy, Context};
 /// We add arguments and calls to super for parents.
 pub fn convert_class(ast: &ASTTy, imp: &mut Imports, state: &State, ctx: &Context) -> GenResult {
     match &ast.node {
-        NodeTy::TypeAlias { ty, isa, .. } => {
-            imp.add_from_import("typing", "NewType");
-            let lit = ty.name.clone();
-
-            Ok(PythonCore::Assign {
-                left: Box::new(PythonCore::Id { lit: lit.clone() }),
-                right: Box::new(PythonCore::FunctionCall {
-                    function: Box::new(PythonCore::Id {
-                        lit: String::from("NewType"),
-                    }),
-                    args: vec![PythonCore::Str { string: lit }, isa.to_py(imp)],
-                }),
-                op: CoreOp::Assign,
-            })
-        }
-        NodeTy::TypeDef { ty, body, isa } | NodeTy::Trait { ty, body, isa } => {
+        NodeTy::Trait { ty, body, isa } => {
             let parents = isa
                 .as_ref()
                 .map_or_else(Vec::new, |isa| vec![isa.to_py(imp)]);

src/backend/python/convert/mod.rs

@@ -241,9 +241,7 @@ pub fn convert_node(ast: &ASTTy, imp: &mut Imports, state: &State, ctx: &Context
             right: Box::from(convert_node(right, imp, state, ctx)?),
         },
 
-        NodeTy::TypeDef { .. } | NodeTy::Trait { .. } | NodeTy::TypeAlias { .. } => {
-            convert_class(ast, imp, state, ctx)?
-        }
+        NodeTy::Trait { .. } => convert_class(ast, imp, state, ctx)?,
         NodeTy::Class { .. } => convert_class(ast, imp, state, ctx)?,
         NodeTy::Parent { .. } => convert_class(ast, imp, state, ctx)?,
 

src/check/ast/mod.rs

@@ -149,23 +149,11 @@ pub enum NodeTy {
         mutable: bool,
         ty: OptName,
     },
-    TypeDef {
-        ty: StringName,
-        isa: OptName,
-        body: OptASTTy,
-    },
-    /// See `parse::ast::Node::Trait`.
-    /// Treated identically to `TypeDef` by the checker for now.
     Trait {
         ty: StringName,
         isa: OptName,
         body: OptASTTy,
     },
-    TypeAlias {
-        ty: StringName,
-        isa: Name,
-        conditions: Vec<ASTTy>,
-    },
     Condition {
         cond: Box<ASTTy>,
         el: OptASTTy,

src/check/ast/node.rs

@@ -163,16 +163,6 @@ impl From<(&Node, &Finished)> for NodeTy {
                     pos_to_name.get(&expr.pos).cloned()
                 },
             },
-            Node::TypeDef { ty, isa, body } => NodeTy::TypeDef {
-                ty: StringName::try_from(ty)
-                    .ok()
-                    .unwrap_or_else(StringName::empty),
-                isa: isa.as_ref().and_then(|isa| Name::try_from(isa).ok()),
-                body: body
-                    .clone()
-                    .map(|ast| ASTTy::from((ast, finished)))
-                    .map(Box::from),
-            },
             Node::Trait { ty, isa, body } => NodeTy::Trait {
                 ty: StringName::try_from(ty)
                     .ok()
@@ -183,18 +173,6 @@ impl From<(&Node, &Finished)> for NodeTy {
                     .map(|ast| ASTTy::from((ast, finished)))
                     .map(Box::from),
             },
-            Node::TypeAlias {
-                ty,
-                isa,
-                conditions,
-            } => NodeTy::TypeAlias {
-                ty: StringName::try_from(ty).unwrap_or_else(|_| StringName::empty()),
-                isa: Name::try_from(isa).unwrap_or_else(|_| Name::empty()),
-                conditions: conditions
-                    .iter()
-                    .map(|ast| ASTTy::from((ast, finished)))
-                    .collect(),
-            },
             Node::Condition { cond, el } => NodeTy::Condition {
                 cond: Box::from(ASTTy::from((cond, finished))),
                 el: el

src/check/constrain/generate/class.rs

@@ -39,38 +39,16 @@ pub fn gen_class(
             }
             _ => Err(vec![TypeErr::new(body.pos, "Expected code block")]),
         },
-        Node::TypeDef {
-            body: Some(body),
-            ty,
-            ..
-        }
-        | Node::Trait {
+        Node::Trait {
             body: Some(body),
             ty,
             ..
         } => match &body.node {
             Node::Block { statements } => constrain_class_body(statements, ty, env, ctx, constr),
             _ => Err(vec![TypeErr::new(body.pos, "Expected code block")]),
         },
-        Node::Class { .. } | Node::TypeDef { .. } | Node::Trait { .. } => Ok(env.clone()),
+        Node::Class { .. } | Node::Trait { .. } => Ok(env.clone()),
 
-        Node::TypeAlias {
-            conditions,
-            isa,
-            ty,
-        } => {
-            // Self is defined top level in type alias
-            let var = AST::new(
-                ty.pos,
-                Id {
-                    lit: String::from(SELF),
-                },
-            );
-            let name = Some(Name::try_from(isa)?); // For now assume super
-            let env = id_from_var(&var, &name, &None, false, ctx, constr, env)?;
-
-            constrain_class_body(conditions, isa, &env, ctx, constr)
-        }
         Node::Condition { cond, el: Some(el) } => {
             generate(cond, env, ctx, constr)?;
             generate(el, env, ctx, constr)

src/check/constrain/generate/mod.rs

@@ -48,8 +48,8 @@ pub fn generate(
     match &ast.node {
         Block { statements } => gen_vec(statements, env, true, ctx, constr),
 
-        Class { .. } | TypeDef { .. } | Trait { .. } => gen_class(ast, env, ctx, constr),
-        TypeAlias { .. } | Condition { .. } => gen_class(ast, env, ctx, constr),
+        Class { .. } | Trait { .. } => gen_class(ast, env, ctx, constr),
+        Condition { .. } => gen_class(ast, env, ctx, constr),
 
         VariableDef { .. } | FunDef { .. } | FunArg { .. } => gen_def(ast, env, ctx, constr),