Functor modules

A module declaration may take type or value parameters, producing a functor module — a module-valued function:

functor-mod  ::= 'mod' Ident generic-params '{' mod-item* '}'
                                                              // generic functor
              |  'mod' Ident '(' param-list ')' '{' mod-item* '}'
                                                              // value-parameter functor
mod-alias    ::= 'mod' Ident '=' path '(' expr-list ')' ';'  // instantiation

Functor modules are instantiated via the mod Name = path(args); alias form introduced in Structure; the body is re-elaborated per instantiation site with the parameters bound. The substrate guarantees monomorphization at elaboration — there is no runtime module dispatch.

mod TaxJurisdiction<J: Jurisdiction> {
    pub type TaxableIncome <: Money;
    pub derive owes_tax(p: Person) :- p.income: TaxableIncome, p.income > 0;
}

mod us_federal = TaxJurisdiction<USFederal>;
mod california = TaxJurisdiction<California>;

Parametric modules, not parametric concepts. Argon admits parameterization only at the module level. There is no parametric pub type Container<T> { … } form — a metatype-classified concept is always a closed, monomorphic classifier. When a modeler wants Container<Apple> vs Container<Orange>, the answer is either (a) a specialization hierarchy (pub type AppleBox <: Container) when the variation is ontological, or (b) a functor module whose body declares the per-instantiation concepts when the variation is parametric. This restriction keeps the metatype calculus first-order and the inference tier classifier decidable; lifting it would require admitting kind-polymorphism into refinement and standpoint federation, both of which are unsound at present without further machinery.

A functor body admits any module-level item: concepts, relations, rules, traits, macros, sub-mods, and other functor modules. Each instantiation produces a fully elaborated namespace; symbols from one instantiation do not unify with symbols from another (us_federal::TaxableIncome and california::TaxableIncome are distinct types, both <: Money).

Functor modules are the canonical mechanism for vocabulary-parameterized libraries (per D-007).