Plural-marking typology — substrate types

@cite{wals-2013} (Chs 33-36)

Type-level enums + per-language profile struct for nominal and pronominal plurality across @cite{wals-2013} chapters 33–36.

Schema

• PluralCoding (Ch 33): how plurality is morphologically realized
• PluralOccurrence (Ch 34): when plural marking occurs (animacy + obligatoriness)
• PronounPlurality (Ch 35): how independent pronouns encode number
• AssociativePlural (Ch 36): "X and associates" construction
• PluralityProfile: per-language bundle of the four

Per-language data lives in Fragments/{Lang}/Plurals.lean. Raw WALS distributions live in Data/WALS/Features/F3{3..6}A.lean — count any strategy directly via F3XA.allData.countP (·.value == ...) rather than re-tabulating here. Corbett 2000 Number refines several of these (general number, dual/trial/paucal inventory, facultative number, Smith-Stark animacy hierarchy, clusivity); those distinctions are formalized in Features/Number.lean, Features/Person.lean, and Phenomena/Agreement/Studies/Corbett2000.lean rather than here.

Layer discipline

This file is substrate: enums, profile struct, predicates, WALS converters. No Fragment imports.

inductive Typology.PluralCoding : Type

WALS Ch 33: how plurality is morphologically coded on full nouns. Nine values cross morphological strategy with absence-of-marking.

• prefix : PluralCoding

  Plural prefix (e.g., Swahili wa-toto 'children').

• suffix : PluralCoding

  Plural suffix (e.g., English dog-s).

• stemChange : PluralCoding

  Stem-internal vowel change (e.g., Maricopa humar/humaar).

• tone : PluralCoding

  Tonal change (e.g., Ngiti kamà/kámá 'chief/chiefs').

• reduplication : PluralCoding

  Complete reduplication (e.g., Indonesian rumah-rumah).

• mixedMorphological : PluralCoding

  Two or more methods, none primary (e.g., Arabic).

• pluralWord : PluralCoding

  Separate word in NP (e.g., Hawaiian mau, Mandarin 些).

• pluralClitic : PluralCoding

  NP-level clitic (e.g., Cayuvava me=).

• noPlural : PluralCoding

  No indication of plurality.

@[implicit_reducible]

instance Typology.instDecidableEqPluralCoding : DecidableEq PluralCoding

Equations

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

@[implicit_reducible]

instance Typology.instReprPluralCoding : Repr PluralCoding

Equations

• Typology.instReprPluralCoding = { reprPrec := Typology.instReprPluralCoding.repr }

def Typology.instReprPluralCoding.repr : PluralCoding → Nat → Std.Format

Equations

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

inductive Typology.PluralOccurrence : Type

WALS Ch 34: when plural marking occurs on full nouns. Cross of animacy scope (none / human-only / all) and obligatoriness (optional / obligatory).

• noNominalPlural : PluralOccurrence

  No nominal plural at all.

• humanOnlyOptional : PluralOccurrence

  Plural only on human nouns, optional.

• humanOnlyObligatory : PluralOccurrence

  Plural only on human nouns, obligatory.

• allNounsAlwaysOptional : PluralOccurrence

  Plural on all nouns, always optional.

• allNounsOptionalInanimates : PluralOccurrence

  Plural on all nouns, obligatory for human, optional for inanimate.

• allNounsAlwaysObligatory : PluralOccurrence

  Plural on all nouns, always obligatory.

@[implicit_reducible]

instance Typology.instDecidableEqPluralOccurrence : DecidableEq PluralOccurrence

Equations

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

def Typology.instReprPluralOccurrence.repr : PluralOccurrence → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPluralOccurrence : Repr PluralOccurrence

Equations

• Typology.instReprPluralOccurrence = { reprPrec := Typology.instReprPluralOccurrence.repr }

inductive Typology.PronounPlurality : Type

WALS Ch 35: how independent personal pronouns encode number.

• noIndependentPronouns : PronounPlurality

  No independent subject pronouns (e.g., Acoma).

• numberIndifferent : PronounPlurality

  Same form for sg and pl (e.g., Pirahã ti 'I/we').

• personNumberAffixes : PronounPlurality

  Both person and number are affixal.

• personNumberStem : PronounPlurality

  Person+number fused in stem (e.g., Dogon mi/emme).

• pnStemPronominalAffix : PronounPlurality

  Person-number stem + pronominal plural affix.

• pnStemNominalAffix : PronounPlurality

  Person-number stem + nominal plural affix (e.g., Russian).

• personStemPronominalAffix : PronounPlurality

  Person stem + pronominal plural affix (e.g., Chuvash).

• personStemNominalAffix : PronounPlurality

  Person stem + nominal plural affix (e.g., Mandarin -men).

@[implicit_reducible]

instance Typology.instDecidableEqPronounPlurality : DecidableEq PronounPlurality

Equations

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

@[implicit_reducible]

instance Typology.instReprPronounPlurality : Repr PronounPlurality

Equations

• Typology.instReprPronounPlurality = { reprPrec := Typology.instReprPronounPlurality.repr }

def Typology.instReprPronounPlurality.repr : PronounPlurality → Nat → Std.Format

Equations

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

inductive Typology.AssociativePlural : Type

WALS Ch 36: associative plural marking ("X and associates"). The typological split is between marker-overlap with additive plural vs dedicated associative form.

• sameAsAdditive : AssociativePlural

  Marker also used for additive plural (e.g., Zulu, Turkish).

• uniqueAffixal : AssociativePlural

  Dedicated affix (e.g., Hungarian -ek).

• uniquePeriphrastic : AssociativePlural

  Dedicated free/clitic marker (e.g., Tagalog, Japanese -tachi).

• absent : AssociativePlural

  No productive associative plural (e.g., Russian, English).

@[implicit_reducible]

instance Typology.instDecidableEqAssociativePlural : DecidableEq AssociativePlural

Equations

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

@[implicit_reducible]

instance Typology.instReprAssociativePlural : Repr AssociativePlural

Equations

• Typology.instReprAssociativePlural = { reprPrec := Typology.instReprAssociativePlural.repr }

def Typology.instReprAssociativePlural.repr : AssociativePlural → Nat → Std.Format

Equations

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

structure Typology.PluralityProfile : Type

A language's plurality profile across @cite{wals-2013} Chs 33-36.

• language : String

  Language name (matches LanguageProfile.name when bundled).

• iso : String

  ISO 639-3 code (matches LanguageProfile.iso when bundled).

• coding : PluralCoding

  Ch 33: how plurality is coded on nouns.

• occurrence : PluralOccurrence

  Ch 34: when plural marking occurs.

• pronounPlurality : PronounPlurality

  Ch 35: pronoun plurality type.

• associativePlural : AssociativePlural

  Ch 36: associative plural strategy.

def Typology.instReprPluralityProfile.repr : PluralityProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPluralityProfile : Repr PluralityProfile

Equations

• Typology.instReprPluralityProfile = { reprPrec := Typology.instReprPluralityProfile.repr }

@[implicit_reducible]

instance Typology.instDecidableEqPluralityProfile : DecidableEq PluralityProfile

Equations

• Typology.instDecidableEqPluralityProfile = Typology.instDecidableEqPluralityProfile.decEq

def Typology.instDecidableEqPluralityProfile.decEq (x✝ x✝¹ : PluralityProfile) : Decidable (x✝ = x✝¹)

Equations

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