Typology.Modality

@cite{aikhenvald-2004} @cite{de-haan-2013} @cite{vanbogaert-2013} @cite{deandradedehaanValenzuela-2013} @cite{wals-2013}

Per-language typological substrate for modality and evidentiality. Covers five WALS chapters by @cite{de-haan-2013} and others:

• Ch 74: situational possibility (root, dynamic) — verbal, affixal, other.
• Ch 75: epistemic possibility — verbal, affixal, other.
• Ch 76: overlap between situational and epistemic modal marking.
• Ch 77: semantic distinctions of evidentiality (no grammatical / indirect-only / direct + indirect / three+).
• Ch 78: coding of evidentiality (verbal affix, particle, TAM-fused, ...).

Mirrors the Linglib/Typology/{Possession,Negation,Comparison,Coordination} substrate-extension pattern. Fragment-importable.

What lives here

• EvidentialSystem (Ch 77 4-way), EvidentialCoding (Ch 78 5-way) enums.
• EvidentialityProfile per-language struct.
• WALS converters: fromWALS77A, fromWALS78A.
• Aggregate distribution theorems for Ch 74-78 (corpus-only, theory-neutral).
• Helper predicates (hasEvidentials, hasDirect, numChoices, isBound, countBySystem, countByCoding).

Theory-laden caveats

• EvidentialSystem extends WALS Ch 77's 3-way to a 4-way by adding threeOrMore. WALS collapses Quechua / Tuyuca / Aymara / Tariana into the same directAndIndirect bucket as Turkish / Bulgarian.
• EvidentialCoding extends WALS Ch 78 with a separate clitic value (WALS lumps "verbal affix or clitic"). Used by analyses that distinguish affix from clitic.
• @cite{aikhenvald-2004}'s richer evidential typology (4-term, 5-term, etc. with finer category labels — visual / nonvisual / inferential / etc.) is beyond what WALS encodes; per-language profiles can record additional detail in markers and notes.

Out of scope

Cross-linguistic generalisations consuming Fragment per-language data live in Phenomena/Modality/Studies/Aikhenvald2004.lean (evidentiality typology + the 18-language sample) and other paper-anchored studies (Narrog2010/2012 for deontic necessity; Rubinstein2014 for weak necessity; ImelGuoST2026 for modal-meaning typology).

inductive Typology.Modality.EvidentialSystem : Type

WALS Ch 77: how many evidential distinctions a language grammaticalises. Extends the WALS 3-way classification with a threeOrMore value to distinguish Quechua/Tuyuca-style rich systems from canonical 2-way systems (Turkish/Bulgarian).

• noGrammatical : EvidentialSystem

  No grammatical evidentials (e.g. English, French, Mandarin).

• indirectOnly : EvidentialSystem

  Indirect evidential only (e.g. Georgian, West Greenlandic).

• directAndIndirect : EvidentialSystem

  Two-choice direct vs indirect (e.g. Turkish, Bulgarian, Tibetan, Abkhaz).

• threeOrMore : EvidentialSystem

  Three or more evidential choices (e.g. Quechua, Tuyuca, Aymara, Tariana).

@[implicit_reducible]

instance Typology.Modality.instDecidableEqEvidentialSystem : DecidableEq EvidentialSystem

Equations

• Typology.Modality.instDecidableEqEvidentialSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Modality.instBEqEvidentialSystem : BEq EvidentialSystem

Equations

• Typology.Modality.instBEqEvidentialSystem = { beq := Typology.Modality.instBEqEvidentialSystem.beq }

def Typology.Modality.instBEqEvidentialSystem.beq : EvidentialSystem → EvidentialSystem → Bool

Equations

• Typology.Modality.instBEqEvidentialSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Modality.instReprEvidentialSystem : Repr EvidentialSystem

Equations

• Typology.Modality.instReprEvidentialSystem = { reprPrec := Typology.Modality.instReprEvidentialSystem.repr }

def Typology.Modality.instReprEvidentialSystem.repr : EvidentialSystem → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.EvidentialSystem.HasEvidentials : EvidentialSystem → Prop

Whether a language has any grammatical evidential marking.

Equations

• Typology.Modality.EvidentialSystem.noGrammatical.HasEvidentials = False
• Typology.Modality.EvidentialSystem.indirectOnly.HasEvidentials = True
• Typology.Modality.EvidentialSystem.directAndIndirect.HasEvidentials = True
• Typology.Modality.EvidentialSystem.threeOrMore.HasEvidentials = True

@[simp]

theorem Typology.Modality.EvidentialSystem.hasEvidentials_iff (s : EvidentialSystem) : s.HasEvidentials ↔ s ≠ noGrammatical

@[implicit_reducible]

instance Typology.Modality.EvidentialSystem.instDecidablePredHasEvidentials : DecidablePred HasEvidentials

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.EvidentialSystem.HasDirect : EvidentialSystem → Prop

Whether a language grammaticalizes a direct evidence category.

Equations

• Typology.Modality.EvidentialSystem.directAndIndirect.HasDirect = True
• Typology.Modality.EvidentialSystem.threeOrMore.HasDirect = True
• Typology.Modality.EvidentialSystem.noGrammatical.HasDirect = False
• Typology.Modality.EvidentialSystem.indirectOnly.HasDirect = False

@[simp]

theorem Typology.Modality.EvidentialSystem.hasDirect_iff (s : EvidentialSystem) : s.HasDirect ↔ s = directAndIndirect ∨ s = threeOrMore

@[implicit_reducible]

instance Typology.Modality.EvidentialSystem.instDecidablePredHasDirect : DecidablePred HasDirect

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.EvidentialSystem.numChoices : EvidentialSystem → Nat

Number of evidential choices in the system (0, 1, 2, or 3+).

Equations

• Typology.Modality.EvidentialSystem.noGrammatical.numChoices = 0
• Typology.Modality.EvidentialSystem.indirectOnly.numChoices = 1
• Typology.Modality.EvidentialSystem.directAndIndirect.numChoices = 2
• Typology.Modality.EvidentialSystem.threeOrMore.numChoices = 3

inductive Typology.Modality.EvidentialCoding : Type

WALS Ch 78: how evidentiality is morphologically expressed.

• verbalAffix : EvidentialCoding

  Evidential is a verbal affix or clitic (bound morpheme). Dominant strategy worldwide (131/418 in WALS Ch 78).

• clitic : EvidentialCoding

  Evidential is a clitic (phrasal-level, not strictly verbal).

• particle : EvidentialCoding

  Evidential is a free separate particle (65/418).

• partOfTAM : EvidentialCoding

  Evidential distinctions fused into the TAM paradigm.

• notApplicable : EvidentialCoding

  Not applicable: language has no grammatical evidentials.

@[implicit_reducible]

instance Typology.Modality.instDecidableEqEvidentialCoding : DecidableEq EvidentialCoding

Equations

• Typology.Modality.instDecidableEqEvidentialCoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Modality.instBEqEvidentialCoding.beq : EvidentialCoding → EvidentialCoding → Bool

Equations

• Typology.Modality.instBEqEvidentialCoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Modality.instBEqEvidentialCoding : BEq EvidentialCoding

Equations

• Typology.Modality.instBEqEvidentialCoding = { beq := Typology.Modality.instBEqEvidentialCoding.beq }

@[implicit_reducible]

instance Typology.Modality.instReprEvidentialCoding : Repr EvidentialCoding

Equations

• Typology.Modality.instReprEvidentialCoding = { reprPrec := Typology.Modality.instReprEvidentialCoding.repr }

def Typology.Modality.instReprEvidentialCoding.repr : EvidentialCoding → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.EvidentialCoding.IsBound : EvidentialCoding → Prop

Whether the coding strategy involves a bound morpheme (affix or clitic).

Equations

• Typology.Modality.EvidentialCoding.verbalAffix.IsBound = True
• Typology.Modality.EvidentialCoding.clitic.IsBound = True
• Typology.Modality.EvidentialCoding.particle.IsBound = False
• Typology.Modality.EvidentialCoding.partOfTAM.IsBound = False
• Typology.Modality.EvidentialCoding.notApplicable.IsBound = False

@[simp]

theorem Typology.Modality.EvidentialCoding.isBound_iff (c : EvidentialCoding) : c.IsBound ↔ c = verbalAffix ∨ c = clitic

@[implicit_reducible]

instance Typology.Modality.EvidentialCoding.instDecidablePredIsBound : DecidablePred IsBound

Equations

• One or more equations did not get rendered due to their size.

structure Typology.Modality.EvidentialityProfile : Type

A language's evidentiality profile across WALS Chs 77-78.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• family : String

  Language family.

• system : EvidentialSystem

  WALS Ch 77: evidential system type.

• coding : EvidentialCoding

  WALS Ch 78: coding strategy.

• markers : List String

  Evidential marker forms (if applicable).

• notes : String

  Notes on the evidential system.

• attestedEvidentials : List Features.Evidentiality.EvidentialSource

  Bridge to the lexical-layer Features.Evidentiality.EvidentialSource taxonomy: the canonical Aikhenvald-style source categories (direct / hearsay / inference) attested in this language. Defaults to [] for no-grammatical-evidentials languages. For 5-term systems (Tuyuca, Tariana, Kashaya) the visual/nonvisual distinction collapses onto .direct; the finer Aikhenvald categories live in markers.

def Typology.Modality.instReprEvidentialityProfile.repr : EvidentialityProfile → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Modality.instReprEvidentialityProfile : Repr EvidentialityProfile

Equations

• Typology.Modality.instReprEvidentialityProfile = { reprPrec := Typology.Modality.instReprEvidentialityProfile.repr }

@[implicit_reducible]

instance Typology.Modality.instDecidableEqEvidentialityProfile : DecidableEq EvidentialityProfile

Equations

• Typology.Modality.instDecidableEqEvidentialityProfile = Typology.Modality.instDecidableEqEvidentialityProfile.decEq

def Typology.Modality.instDecidableEqEvidentialityProfile.decEq (x✝ x✝¹ : EvidentialityProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.fromWALS77A : Data.WALS.F77A.EvidentialityDistinctions → EvidentialSystem

WALS Ch 77 → EvidentialSystem. WALS Ch 77's 3-way classification maps onto our 4-way; threeOrMore cannot be reached from WALS alone (WALS lumps three-or-more systems with directAndIndirect).

Equations

• Typology.Modality.fromWALS77A Data.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials = Typology.Modality.EvidentialSystem.noGrammatical
• Typology.Modality.fromWALS77A Data.WALS.F77A.EvidentialityDistinctions.indirectOnly = Typology.Modality.EvidentialSystem.indirectOnly
• Typology.Modality.fromWALS77A Data.WALS.F77A.EvidentialityDistinctions.directAndIndirect = Typology.Modality.EvidentialSystem.directAndIndirect

def Typology.Modality.fromWALS78A : Data.WALS.F78A.EvidentialityCoding → EvidentialCoding

WALS Ch 78 → EvidentialCoding. WALS lumps "verbal affix or clitic"; the mixed and modalMorpheme categories are mapped to closest local cells (best-effort).

Equations

• Typology.Modality.fromWALS78A Data.WALS.F78A.EvidentialityCoding.noGrammaticalEvidentials = Typology.Modality.EvidentialCoding.notApplicable
• Typology.Modality.fromWALS78A Data.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic = Typology.Modality.EvidentialCoding.verbalAffix
• Typology.Modality.fromWALS78A Data.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem = Typology.Modality.EvidentialCoding.partOfTAM
• Typology.Modality.fromWALS78A Data.WALS.F78A.EvidentialityCoding.separateParticle = Typology.Modality.EvidentialCoding.particle
• Typology.Modality.fromWALS78A Data.WALS.F78A.EvidentialityCoding.modalMorpheme = Typology.Modality.EvidentialCoding.particle
• Typology.Modality.fromWALS78A Data.WALS.F78A.EvidentialityCoding.mixed = Typology.Modality.EvidentialCoding.partOfTAM

def Typology.Modality.EvidentialityProfile.HasEvidentials (p : EvidentialityProfile) : Prop

Does a language have grammatical evidentials?

Equations

• p.HasEvidentials = p.system.HasEvidentials

@[simp]

theorem Typology.Modality.EvidentialityProfile.hasEvidentials_iff (p : EvidentialityProfile) : p.HasEvidentials ↔ p.system.HasEvidentials

@[implicit_reducible]

instance Typology.Modality.EvidentialityProfile.instDecidablePredHasEvidentials : DecidablePred HasEvidentials

Equations

• p.instDecidablePredHasEvidentials = decidable_of_iff p.system.HasEvidentials ⋯

def Typology.Modality.EvidentialityProfile.HasDirect (p : EvidentialityProfile) : Prop

Does a language have a direct evidence category?

Equations

• p.HasDirect = p.system.HasDirect

@[simp]

theorem Typology.Modality.EvidentialityProfile.hasDirect_iff (p : EvidentialityProfile) : p.HasDirect ↔ p.system.HasDirect

@[implicit_reducible]

instance Typology.Modality.EvidentialityProfile.instDecidablePredHasDirect : DecidablePred HasDirect

Equations

• p.instDecidablePredHasDirect = decidable_of_iff p.system.HasDirect ⋯

def Typology.Modality.countBySystem (langs : List EvidentialityProfile) (s : EvidentialSystem) : Nat

Count of languages in a sample with a given system type.

Equations

• Typology.Modality.countBySystem langs s = (List.filter (fun (x : Typology.Modality.EvidentialityProfile) => x.system == s) langs).length

def Typology.Modality.countByCoding (langs : List EvidentialityProfile) (c : EvidentialCoding) : Nat

Count of languages in a sample with a given coding type.

Equations

• Typology.Modality.countByCoding langs c = (List.filter (fun (x : Typology.Modality.EvidentialityProfile) => x.coding == c) langs).length

def Typology.Modality.walsEvidentialSystem (iso : String) : Option EvidentialSystem

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.walsEvidentialCoding (iso : String) : Option EvidentialCoding

Equations

• One or more equations did not get rendered due to their size.

def Typology.Modality.EvidentialityProfile.fromWALS (language iso family : String) (markers : List String := []) (notes : String := "") (attestedEvidentials : List Features.Evidentiality.EvidentialSource := []) (systemFb : EvidentialSystem := EvidentialSystem.noGrammatical) (codingFb : EvidentialCoding := EvidentialCoding.notApplicable) : EvidentialityProfile

Build an EvidentialityProfile from an ISO 639-3 code via WALS lookups for Chs 77/78. Required-field fallbacks (systemFb, codingFb) fire only when WALS is silent for that ISO. The markers, notes, attestedEvidentials, and family fields are paper-stipulated.

Note: WALS Ch 77 only encodes a 3-way classification (no threeOrMore); languages with rich evidential systems (Quechua, Tuyuca, Tariana, etc.) will get .directAndIndirect from fromWALS77A rather than .threeOrMore. Per @cite{aikhenvald-2004}'s richer typology, those languages need a Studies-side override (mirrors the Corbett 1991 vs 2013 record-update pattern in Phenomena/Gender/Studies/Corbett1991).

Equations

• One or more equations did not get rendered due to their size.

Earlier revisions of this file carried 11 aggregate-count corpus theorems on the full WALS Ch 74-78 datasets (ch74_verbal_dominant, ch77_no_evidentials_most_common, etc.). These were the "aggregate-count theorems go stale" anti-pattern AND required native_decide for ~250-418-element list reductions; deleted as part of the EvidentialityProfile mathlib polish. The corpus distributions remain documentary in @cite{de-haan-2013}'s WALS chapters.