- TypeScript 96.8%
- HTML 2.7%
- JavaScript 0.5%
Type Classes in math-engine-js
- Type Classes in math-engine-js
Type Classes in math-engine-js
This document demonstrates how type classes are implemented and used in math-engine-js, a computer algebra system based on lambda calculus with Hindley-Milner type inference.
Overview
Type classes provide a way to define abstract interfaces that types can implement. They are similar to Haskell typeclasses or Rust traits, allowing polymorphic behavior without sacrificing type safety.
Running the Example
To run the examples in this document:
# Build the project
npm run build
# Start the REPL
node dist/repl-cli.js
# Debug with type class script
node debug-typeclass.jsContinuous Fields Example
Let's walk through a complete example using continuity in mathematical fields:
1. Define the Continuous Type Class
First, we define a type class named Continuous with a method to check continuity at a point:
// Define the Continuous type class
defineClass("Continuous", "a", [
("isContinuousAt", "a -> Number -> Bool")
])
The type class takes a type parameter a and defines a method isContinuousAt that checks if a value of type a is continuous at a given point.
2. Implement for Scalar Types
Now we can implement this type class for basic types like Number:
// Implement for Number type
implementClass("Continuous", "Number", [
("isContinuousAt", (x, p) => true)
])
// Implement for Function type
implementClass("Continuous", "Function(Number, Number)", [
("isContinuousAt", (f, p) =>
// Check if limit exists at point p
// This is a simplified implementation
abs(f(p + 0.001) - f(p)) < 0.01
)
])3. Implement for Tensor Types
We can extend continuity to tensors:
// Implement for component tensors
implementClass("Continuous", "ComponentTensor(1,0)", [
("isContinuousAt", (tensor, p) =>
// A tensor is continuous if all its components are
allComponents(tensor, component =>
isContinuousAt(component, p)
)
)
])4. Define Functions with Type Class Constraints
Now we can define functions that require continuity:
// Define a function that works on any continuous type
// The :: operator imposes the Continuous constraint
differentiate = (f :: Continuous) =>
(x) => limit(h => (f(x + h) - f(x)) / h, 0)
// Use a type class method directly - dictionary passing happens internally
continuousAt = (f :: Continuous, p) =>
isContinuousAt(f, p) // The system handles dispatching to the correct implementation
// Define function composition that preserves continuity
compose = (f :: Continuous, g :: Continuous) =>
(x) => f(g(x))Type Inference with Constraints
The compose function example above is sufficient without any explicit type annotations. This definition works because:
- The
::operator adds constraints to the type variables, not explicit types - The Hindley-Milner type inference system infers the most general type for the function
- The constraint ensures that whatever types
fandghave, they must implement theContinuoustype class - The implementation works for any type that satisfies the constraint
This is one of the key benefits of type classes - they provide ad-hoc polymorphism without requiring explicit type annotations. The compose function is "universal" in the sense that it works for any types f and g that implement the Continuous type class, regardless of their specific types.
5. Use with Einstein Notation
Type classes integrate with Einstein notation for tensor operations:
// Define a continuous vector field
v_μ = (x^ρ :: Continuous) => x^ρ * x^ρ
// Differentiate the vector field
dv_μν = differentiate(v_μ)6. Verification and Type Checking
The type system verifies that constraints are satisfied:
// This works - Number implements Continuous
derivative = differentiate(x => x^2)
// This also works - we implemented Continuous for ComponentTensor(1,0)
metricDerivative = differentiate(g_μν)
// This would fail at compile-time - String does not implement Continuous
// Type checking prevents the following:
// invalidDerivative = differentiate("not a function")
// Type class constraints are checked at compile-time
// The implementation uses dictionary passing at runtimeTechnical Implementation
The type class system is implemented through:
- Type class definitions in GenericTypeSystem (type-system.ts)
- Constrained types in the type system (type-system.ts)
- Type inference with constraint checking (inference.ts)
- Dictionary passing transformation (lambda.ts)
The implementation works as follows:
- The
- operator creates constrained types during type inference
- ?
- Type checking verifies that appropriate instances exist for constrained types
- ?
- Dictionary passing happens during expression evaluation via transformTypeClassMethods
- ?
- Method calls are dispatched to the correct implementation based on the type
Advanced Examples
Differentiable Type Class
// Define the Differentiable type class
defineClass("Differentiable", "a", [
("derivative", "a -> a")
])
// Implement for functions
// This registers the implementation in the type system
implementClass("Differentiable", "Function(Number, Number)", [
("derivative", (f) =>
(x) => limit(h => (f(x + h) - f(x)) / h, 0)
)
])
// Call the type class method directly
// The dictionary passing transformation happens internally
derivative = (f :: Differentiable) => derivative(f)
// Define chain rule with constraints
// Methods are called directly - the system handles the correct dispatch
chainRule = (f :: Differentiable, g :: Differentiable) =>
(x) => derivative(f)(g(x)) * derivative(g)(x)Field Type Class
// Define the Field type class
defineClass("Field", "a", [
("zero", "a"),
("one", "a"),
("add", "a -> a -> a"),
("mul", "a -> a -> a"),
("neg", "a -> a"),
("inv", "a -> a")
])
// Implement for real numbers
implementClass("Field", "Number", [
("zero", 0),
("one", 1),
("add", (x, y) => x + y),
("mul", (x, y) => x * y),
("neg", (x) => -x),
("inv", (x) => 1/x)
])Reference Documentation
- The
::operator: Applies a type class constraint to an expression defineClass: Creates a new type classimplementClass: Implements a type class for a specific type- Dictionary passing: The implementation uses dictionary passing internally
- Method access: Type class methods are called directly, and the system handles dispatching to the correct implementation