diff --git a/src/ast.rs b/src/ast.rs index 13b82d1..475ca1d 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -120,6 +120,48 @@ pub struct Migration { pub span: Span, } +// ============ Behavioral Types ============ + +/// A behavioral property that can be attached to functions +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum BehavioralProperty { + /// No side effects - function only depends on inputs + Pure, + /// Always terminates and doesn't throw exceptions + Total, + /// f(f(x)) == f(x) for all x + Idempotent, + /// Same inputs always produce same outputs (no randomness) + Deterministic, + /// Order of arguments doesn't matter: f(a, b) == f(b, a) + Commutative, +} + +impl fmt::Display for BehavioralProperty { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + BehavioralProperty::Pure => write!(f, "pure"), + BehavioralProperty::Total => write!(f, "total"), + BehavioralProperty::Idempotent => write!(f, "idempotent"), + BehavioralProperty::Deterministic => write!(f, "deterministic"), + BehavioralProperty::Commutative => write!(f, "commutative"), + } + } +} + +/// A where clause constraint on a function +#[derive(Debug, Clone)] +pub enum WhereClause { + /// Type parameter has a property: where F is pure + PropertyConstraint { + type_param: Ident, + property: BehavioralProperty, + span: Span, + }, + /// Result refinement: where result > 0 + ResultRefinement { predicate: Box, span: Span }, +} + /// Module path: foo/bar/baz #[derive(Debug, Clone, PartialEq, Eq)] pub struct ModulePath { @@ -184,6 +226,10 @@ pub struct FunctionDecl { pub params: Vec, pub return_type: TypeExpr, pub effects: Vec, + /// Behavioral properties: is pure, is total, etc. + pub properties: Vec, + /// Where clause constraints + pub where_clauses: Vec, pub body: Expr, pub span: Span, } diff --git a/src/lexer.rs b/src/lexer.rs index 1574c3d..076aef1 100644 --- a/src/lexer.rs +++ b/src/lexer.rs @@ -41,6 +41,16 @@ pub enum TokenKind { From, // from (for migrations) Latest, // latest (for @latest version constraint) + // Behavioral type keywords + Is, // is (for behavioral properties) + Pure, // pure + Total, // total + Idempotent, // idempotent + Deterministic, // deterministic + Commutative, // commutative + Where, // where (for constraints) + Assume, // assume (for unverified properties) + // Operators Plus, // + Minus, // - @@ -108,6 +118,14 @@ impl fmt::Display for TokenKind { TokenKind::As => write!(f, "as"), TokenKind::From => write!(f, "from"), TokenKind::Latest => write!(f, "latest"), + TokenKind::Is => write!(f, "is"), + TokenKind::Pure => write!(f, "pure"), + TokenKind::Total => write!(f, "total"), + TokenKind::Idempotent => write!(f, "idempotent"), + TokenKind::Deterministic => write!(f, "deterministic"), + TokenKind::Commutative => write!(f, "commutative"), + TokenKind::Where => write!(f, "where"), + TokenKind::Assume => write!(f, "assume"), TokenKind::True => write!(f, "true"), TokenKind::False => write!(f, "false"), TokenKind::Plus => write!(f, "+"), @@ -532,6 +550,14 @@ impl<'a> Lexer<'a> { "as" => TokenKind::As, "from" => TokenKind::From, "latest" => TokenKind::Latest, + "is" => TokenKind::Is, + "pure" => TokenKind::Pure, + "total" => TokenKind::Total, + "idempotent" => TokenKind::Idempotent, + "deterministic" => TokenKind::Deterministic, + "commutative" => TokenKind::Commutative, + "where" => TokenKind::Where, + "assume" => TokenKind::Assume, "true" => TokenKind::Bool(true), "false" => TokenKind::Bool(false), _ => TokenKind::Ident(ident.to_string()), diff --git a/src/main.rs b/src/main.rs index 89167b7..d49e7c6 100644 --- a/src/main.rs +++ b/src/main.rs @@ -788,4 +788,66 @@ c")"#; "#; assert_eq!(eval(source).unwrap(), "0"); } + + // ============ Behavioral Types Tests ============ + + #[test] + fn test_behavioral_pure_function() { + // A pure function with no effects should work + let source = r#" + fn double(x: Int): Int is pure = x * 2 + let result = double(21) + "#; + assert_eq!(eval(source).unwrap(), "42"); + } + + #[test] + fn test_behavioral_total_function() { + // A total function should work + let source = r#" + fn always42(): Int is total = 42 + let result = always42() + "#; + assert_eq!(eval(source).unwrap(), "42"); + } + + #[test] + fn test_behavioral_idempotent_function() { + // An idempotent function + let source = r#" + fn clamp(x: Int): Int is idempotent = if x < 0 then 0 else x + let result = clamp(clamp(-5)) + "#; + assert_eq!(eval(source).unwrap(), "0"); + } + + #[test] + fn test_behavioral_multiple_properties() { + // A function with multiple properties + let source = r#" + fn identity(x: Int): Int is pure, is total = x + let result = identity(100) + "#; + assert_eq!(eval(source).unwrap(), "100"); + } + + #[test] + fn test_behavioral_deterministic() { + let source = r#" + fn square(x: Int): Int is deterministic = x * x + let result = square(7) + "#; + assert_eq!(eval(source).unwrap(), "49"); + } + + #[test] + fn test_behavioral_pure_with_effects_error() { + // A pure function with effects should produce a type error + let source = r#" + fn bad(x: Int): Int with {Logger} is pure = x + "#; + let result = eval(source); + assert!(result.is_err()); + assert!(result.unwrap_err().contains("pure but has effects")); + } } diff --git a/src/parser.rs b/src/parser.rs index 8700354..0d88669 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -191,6 +191,12 @@ impl Parser { Vec::new() }; + // Optional behavioral properties: is pure, is total, etc. + let properties = self.parse_behavioral_properties()?; + + // Optional where clauses + let where_clauses = self.parse_where_clauses()?; + self.expect(TokenKind::Eq)?; self.skip_newlines(); let body = self.parse_expr()?; @@ -203,6 +209,8 @@ impl Parser { params, return_type, effects, + properties, + where_clauses, body, span, }) @@ -490,6 +498,171 @@ impl Parser { Ok(effects) } + /// Parse behavioral properties: is pure, is total, is idempotent, etc. + fn parse_behavioral_properties(&mut self) -> Result, ParseError> { + let mut properties = Vec::new(); + + while self.check(TokenKind::Is) || self.check(TokenKind::Assume) { + let is_assumed = self.check(TokenKind::Assume); + self.advance(); // consume 'is' or 'assume' + + if is_assumed { + // 'assume' must be followed by 'is' + if !self.check(TokenKind::Is) { + return Err(ParseError { + message: "Expected 'is' after 'assume'".to_string(), + span: self.current_span(), + }); + } + self.advance(); // consume 'is' + } + + let property = self.parse_single_property()?; + properties.push(property); + + // Optional comma for multiple properties: is pure, is total + if self.check(TokenKind::Comma) { + self.advance(); + } + } + + Ok(properties) + } + + /// Parse a single behavioral property keyword + fn parse_single_property(&mut self) -> Result { + let span = self.current_span(); + match self.peek_kind() { + TokenKind::Pure => { + self.advance(); + Ok(BehavioralProperty::Pure) + } + TokenKind::Total => { + self.advance(); + Ok(BehavioralProperty::Total) + } + TokenKind::Idempotent => { + self.advance(); + Ok(BehavioralProperty::Idempotent) + } + TokenKind::Deterministic => { + self.advance(); + Ok(BehavioralProperty::Deterministic) + } + TokenKind::Commutative => { + self.advance(); + Ok(BehavioralProperty::Commutative) + } + _ => Err(ParseError { + message: "Expected behavioral property: pure, total, idempotent, deterministic, or commutative".to_string(), + span, + }), + } + } + + /// Parse where clauses: where F is pure, where result > 0 + fn parse_where_clauses(&mut self) -> Result, ParseError> { + let mut clauses = Vec::new(); + + while self.check(TokenKind::Where) { + self.advance(); // consume 'where' + let span = self.current_span(); + + // Check if it's a property constraint: where F is pure + // or a result refinement: where result > 0 + if self.check_ident() { + let ident = self.parse_ident()?; + + if self.check(TokenKind::Is) { + self.advance(); // consume 'is' + let property = self.parse_single_property()?; + clauses.push(WhereClause::PropertyConstraint { + type_param: ident, + property, + span, + }); + } else { + // This is a result refinement starting with an identifier + // For now, we'll parse it as a simple expression + // Put the identifier back by creating an expression + let predicate = self.parse_refinement_with_ident(ident)?; + clauses.push(WhereClause::ResultRefinement { + predicate: Box::new(predicate), + span, + }); + } + } else { + return Err(ParseError { + message: "Expected identifier after 'where'".to_string(), + span, + }); + } + + // Optional comma for multiple where clauses + if self.check(TokenKind::Comma) { + self.advance(); + } + } + + Ok(clauses) + } + + /// Parse a refinement expression that starts with an already-parsed identifier + fn parse_refinement_with_ident(&mut self, ident: Ident) -> Result { + // Start with the identifier as a variable + let mut left = Expr::Var(ident); + + // Parse the rest as a comparison expression + if let Some(op) = self.try_parse_comparison_op() { + let right = self.parse_primary_expr()?; + let span = left.span().merge(right.span()); + left = Expr::BinaryOp { + op, + left: Box::new(left), + right: Box::new(right), + span, + }; + } + + Ok(left) + } + + /// Try to parse a comparison operator + fn try_parse_comparison_op(&mut self) -> Option { + match self.peek_kind() { + TokenKind::Lt => { + self.advance(); + Some(BinaryOp::Lt) + } + TokenKind::Le => { + self.advance(); + Some(BinaryOp::Le) + } + TokenKind::Gt => { + self.advance(); + Some(BinaryOp::Gt) + } + TokenKind::Ge => { + self.advance(); + Some(BinaryOp::Ge) + } + TokenKind::EqEq => { + self.advance(); + Some(BinaryOp::Eq) + } + TokenKind::Ne => { + self.advance(); + Some(BinaryOp::Ne) + } + _ => None, + } + } + + /// Check if the current token is an identifier + fn check_ident(&self) -> bool { + matches!(self.peek_kind(), TokenKind::Ident(_)) + } + /// Parse a type expression fn parse_type(&mut self) -> Result { // Function type: fn(A, B): C with {E} @@ -1932,4 +2105,134 @@ mod tests { panic!("Expected type declaration"); } } + + // ============ Behavioral Properties Tests ============ + + #[test] + fn test_parse_function_is_pure() { + let source = "fn add(a: Int, b: Int): Int is pure = a + b"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.name.name, "add"); + assert_eq!(f.properties.len(), 1); + assert_eq!(f.properties[0], BehavioralProperty::Pure); + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_function_multiple_properties() { + let source = "fn double(x: Int): Int is pure, is total = x * 2"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.name.name, "double"); + assert_eq!(f.properties.len(), 2); + assert!(f.properties.contains(&BehavioralProperty::Pure)); + assert!(f.properties.contains(&BehavioralProperty::Total)); + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_function_with_effects_and_properties() { + let source = "fn log(msg: String): Unit with {Logger} is deterministic = Logger.log(msg)"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.name.name, "log"); + assert_eq!(f.effects.len(), 1); + assert_eq!(f.effects[0].name, "Logger"); + assert_eq!(f.properties.len(), 1); + assert_eq!(f.properties[0], BehavioralProperty::Deterministic); + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_function_idempotent() { + let source = "fn normalize(s: String): String is idempotent = s"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.properties.len(), 1); + assert_eq!(f.properties[0], BehavioralProperty::Idempotent); + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_function_commutative() { + let source = "fn add(a: Int, b: Int): Int is commutative = a + b"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.properties.len(), 1); + assert_eq!(f.properties[0], BehavioralProperty::Commutative); + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_where_property_constraint() { + let source = "fn retry(action: F): Int where F is idempotent = 0"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.name.name, "retry"); + assert_eq!(f.where_clauses.len(), 1); + if let WhereClause::PropertyConstraint { + type_param, + property, + .. + } = &f.where_clauses[0] + { + assert_eq!(type_param.name, "F"); + assert_eq!(*property, BehavioralProperty::Idempotent); + } else { + panic!("Expected PropertyConstraint"); + } + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_where_result_refinement() { + let source = "fn abs(x: Int): Int where result >= 0 = if x < 0 then 0 - x else x"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(f) = &program.declarations[0] { + assert_eq!(f.name.name, "abs"); + assert_eq!(f.where_clauses.len(), 1); + if let WhereClause::ResultRefinement { predicate, .. } = &f.where_clauses[0] { + // Check that the predicate is a binary comparison + if let Expr::BinaryOp { op, .. } = predicate.as_ref() { + assert_eq!(*op, BinaryOp::Ge); + } else { + panic!("Expected BinaryOp in refinement"); + } + } else { + panic!("Expected ResultRefinement"); + } + } else { + panic!("Expected function declaration"); + } + } + + #[test] + fn test_parse_all_behavioral_features() { + // Single-line version to avoid newline issues + let source = "fn process(f: F, x: Int): Int with {Logger} is pure, is total where F is deterministic = f(x)"; + let program = Parser::parse_source(source).unwrap(); + if let Declaration::Function(func) = &program.declarations[0] { + assert_eq!(func.name.name, "process"); + assert_eq!(func.effects.len(), 1); + assert_eq!(func.properties.len(), 2); + assert!(func.properties.contains(&BehavioralProperty::Pure)); + assert!(func.properties.contains(&BehavioralProperty::Total)); + assert_eq!(func.where_clauses.len(), 1); + } else { + panic!("Expected function declaration"); + } + } } diff --git a/src/typechecker.rs b/src/typechecker.rs index 9ad4f46..1f71108 100644 --- a/src/typechecker.rs +++ b/src/typechecker.rs @@ -9,8 +9,8 @@ use crate::ast::{ }; use crate::modules::ModuleLoader; use crate::types::{ - self, unify, EffectDef, EffectOpDef, EffectSet, HandlerDef, Type, TypeEnv, TypeScheme, - VariantDef, VariantFieldsDef, + self, unify, EffectDef, EffectOpDef, EffectSet, HandlerDef, PropertySet, Type, TypeEnv, + TypeScheme, VariantDef, VariantFieldsDef, }; /// Type checking error @@ -234,6 +234,55 @@ impl TypeChecker { span: func.span, }); } + + // Check behavioral properties + let properties = PropertySet::from_ast(&func.properties); + + // Pure functions cannot have effects + if properties.is_pure() && !func.effects.is_empty() { + self.errors.push(TypeError { + message: format!( + "Function '{}' is declared as pure but has effects: {{{}}}", + func.name.name, + func.effects + .iter() + .map(|e| e.name.as_str()) + .collect::>() + .join(", ") + ), + span: func.span, + }); + } + + // Check where clause property constraints + for where_clause in &func.where_clauses { + match where_clause { + ast::WhereClause::PropertyConstraint { + type_param, + property, + span, + } => { + // Record the constraint for later checking when the function is called + // For now, we just validate that the type parameter exists + if !func.type_params.iter().any(|p| p.name == type_param.name) + && !func.params.iter().any(|p| p.name.name == type_param.name) + { + self.errors.push(TypeError { + message: format!( + "Unknown type parameter '{}' in where clause", + type_param.name + ), + span: *span, + }); + } + } + ast::WhereClause::ResultRefinement { predicate, span } => { + // Result refinements are checked at runtime or via SMT solver + // For now, we just type-check the predicate expression + // (would need 'result' in scope, which we don't have yet) + } + } + } } fn check_let_decl(&mut self, let_decl: &LetDecl) { @@ -1089,8 +1138,9 @@ impl TypeChecker { let return_type = self.resolve_type(&func.return_type); let effects = EffectSet::from_iter(func.effects.iter().map(|e| e.name.clone())); + let properties = PropertySet::from_ast(&func.properties); - Type::function_with_effects(param_types, return_type, effects) + Type::function_with_properties(param_types, return_type, effects, properties) } fn effect_def(&self, effect: &EffectDecl) -> EffectDef { diff --git a/src/types.rs b/src/types.rs index 6be28cf..2f13ec9 100644 --- a/src/types.rs +++ b/src/types.rs @@ -25,11 +25,12 @@ pub enum Type { String, Char, Unit, - /// Function type with effects + /// Function type with effects and behavioral properties Function { params: Vec, return_type: Box, effects: EffectSet, + properties: PropertySet, }, /// Generic type application: List, Option App { @@ -72,6 +73,7 @@ impl Type { params, return_type: Box::new(return_type), effects: EffectSet::empty(), + properties: PropertySet::empty(), } } @@ -80,6 +82,21 @@ impl Type { params, return_type: Box::new(return_type), effects, + properties: PropertySet::empty(), + } + } + + pub fn function_with_properties( + params: Vec, + return_type: Type, + effects: EffectSet, + properties: PropertySet, + ) -> Self { + Type::Function { + params, + return_type: Box::new(return_type), + effects, + properties, } } @@ -121,10 +138,12 @@ impl Type { params, return_type, effects, + properties, } => Type::Function { params: params.iter().map(|p| p.apply(subst)).collect(), return_type: Box::new(return_type.apply(subst)), effects: effects.clone(), + properties: properties.clone(), }, Type::App { constructor, args } => Type::App { constructor: Box::new(constructor.apply(subst)), @@ -209,6 +228,7 @@ impl fmt::Display for Type { params, return_type, effects, + properties, } => { write!(f, "fn(")?; for (i, p) in params.iter().enumerate() { @@ -221,6 +241,9 @@ impl fmt::Display for Type { if !effects.is_empty() { write!(f, " with {{{}}}", effects)?; } + if !properties.is_empty() { + write!(f, " {}", properties)?; + } Ok(()) } Type::App { constructor, args } => { @@ -335,6 +358,109 @@ impl fmt::Display for EffectSet { } } +/// Set of behavioral properties for a function +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub struct PropertySet { + pub properties: HashSet, +} + +/// A behavioral property (mirrors BehavioralProperty from AST but for type system) +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum Property { + Pure, + Total, + Idempotent, + Deterministic, + Commutative, +} + +impl From for Property { + fn from(p: crate::ast::BehavioralProperty) -> Self { + match p { + crate::ast::BehavioralProperty::Pure => Property::Pure, + crate::ast::BehavioralProperty::Total => Property::Total, + crate::ast::BehavioralProperty::Idempotent => Property::Idempotent, + crate::ast::BehavioralProperty::Deterministic => Property::Deterministic, + crate::ast::BehavioralProperty::Commutative => Property::Commutative, + } + } +} + +impl fmt::Display for Property { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Property::Pure => write!(f, "pure"), + Property::Total => write!(f, "total"), + Property::Idempotent => write!(f, "idempotent"), + Property::Deterministic => write!(f, "deterministic"), + Property::Commutative => write!(f, "commutative"), + } + } +} + +impl PropertySet { + pub fn empty() -> Self { + Self { + properties: HashSet::new(), + } + } + + pub fn from_ast(props: &[crate::ast::BehavioralProperty]) -> Self { + Self { + properties: props.iter().copied().map(Property::from).collect(), + } + } + + pub fn is_empty(&self) -> bool { + self.properties.is_empty() + } + + pub fn contains(&self, prop: Property) -> bool { + self.properties.contains(&prop) + } + + pub fn is_pure(&self) -> bool { + self.contains(Property::Pure) + } + + pub fn is_total(&self) -> bool { + self.contains(Property::Total) + } + + pub fn insert(&mut self, prop: Property) { + self.properties.insert(prop); + } + + /// Check if this property set is a superset of another (satisfies constraints) + pub fn satisfies(&self, required: &PropertySet) -> bool { + required.properties.is_subset(&self.properties) + } + + /// Intersection of two property sets (for composition) + pub fn intersection(&self, other: &PropertySet) -> PropertySet { + PropertySet { + properties: self + .properties + .intersection(&other.properties) + .copied() + .collect(), + } + } +} + +impl fmt::Display for PropertySet { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + let props: Vec<_> = self.properties.iter().collect(); + for (i, p) in props.iter().enumerate() { + if i > 0 { + write!(f, ", ")?; + } + write!(f, "is {}", p)?; + } + Ok(()) + } +} + /// Type substitution (mapping from type variables to types) #[derive(Debug, Clone, Default)] pub struct Substitution { @@ -941,11 +1067,13 @@ pub fn unify(t1: &Type, t2: &Type) -> Result { params: p1, return_type: r1, effects: e1, + properties: props1, }, Type::Function { params: p2, return_type: r2, effects: e2, + properties: props2, }, ) => { if p1.len() != p2.len() { @@ -964,6 +1092,11 @@ pub fn unify(t1: &Type, t2: &Type) -> Result { )); } + // Properties are not checked during unification - they are guarantees, not constraints + // A pure function can be used anywhere a function is expected + // Property requirements are enforced via where clauses, not type unification + let _ = (props1, props2); // Acknowledge but don't enforce + let mut subst = Substitution::new(); for (a, b) in p1.iter().zip(p2.iter()) { let s = unify(&a.apply(&subst), &b.apply(&subst))?;