Crate bhc_types 

BHC Type System

This crate implements the type system for the Basel Haskell Compiler (BHC), including type representations, type inference, unification, and typeclass resolution.

Overview

The BHC type system is based on Hindley-Milner type inference with extensions for:

• Higher-kinded types
• Type classes with functional dependencies
• Type families
• GADTs (Generalized Algebraic Data Types)
• Rank-N polymorphism (limited)
• M9 Dependent Types Preview: Shape-indexed tensors with compile-time dimension checking

Core Types

The type system is built around several key types:

• Ty: The main type representation
• TyVar: Type variables for polymorphism
• TyId: Unique type identifiers
• Kind: Kinds for higher-kinded types
• Scheme: Polymorphic type schemes
• TyNat: Type-level natural numbers (M9)
• TyList: Type-level lists for shapes (M9)

Type Inference

Type inference proceeds in several phases:

1. Constraint generation: Walk the AST and generate type constraints
2. Unification: Solve constraints to find substitutions
3. Generalization: Generalize types at let-bindings
4. Defaulting: Apply defaulting rules for ambiguous types

Shape-Indexed Tensors (M9)

BHC supports shape-indexed tensor types for compile-time dimension checking:

matmul :: Tensor '[m, k] Float -> Tensor '[k, n] Float -> Tensor '[m, n] Float

See nat and ty_list modules for type-level constructs.

See Also

• bhc-hir: High-level IR that uses these types
• bhc-core: Core IR with explicit type annotations
• H26-SPEC Section 4: Type System Specification
• H26-SPEC Section 7: Tensor Model

Re-exports

pub use dyn_tensor::dyn_tensor_of;

pub use dyn_tensor::dyn_tensor_tycon;

pub use dyn_tensor::shape_witness_of;

pub use dyn_tensor::shape_witness_tycon;

pub use nat::TyNat;

pub use ty_list::TyList;

Modules

dyn_tensor

Dynamic tensor types for gradual shape adoption.

nat

Type-level natural numbers.

ty_list

Type-level lists for tensor shapes.

Structs

Constraint

A type class constraint (e.g., Eq a, Num a).

Scheme

A polymorphic type scheme (forall-quantified type).

Subst

A substitution mapping type variables to types.

TyCon

A type constructor with its name and kind.

TyId

A unique identifier for types within the type system.

TyVar

A type variable, used for polymorphic types.

Enums

Kind

Kinds classify types, just as types classify values.

PrimTy

Unboxed primitive types for the Numeric Profile.

Ty

The main type representation in BHC.

TypeError

Errors that can occur during type operations.

Functions

types_equal

Check if two types are structurally equal.

types_match

Match a pattern type against a target type, returning a substitution.

types_match_multi

Match multiple pattern types against target types, returning combined substitution.

types_match_with_subst

Helper function that accumulates substitutions during type matching.