Imperative-system typology — substrate types and WALS data

@cite{wals-2013} (Chs 70, 71, 72, 73) @cite{van-der-auwera-lejeune-2013}

Type-level enums + per-language profile struct for the imperative-prohibitive- hortative-jussive-optative complex across @cite{wals-2013} chapters 70–73, plus WALS distribution data and the principal cross-linguistic generalizations from van der Auwera & Lejeune (2013).

Schema

• MorphImpType (Ch 70): morphological imperative status
• ProhibitiveType (Ch 71): prohibitive construction (verb form × negation type)
• ImpHortSystem (Ch 72): hortative/jussive paradigm richness
• OptativePresence (Ch 73): dedicated optative present/absent
• ImperativeProfile: per-language bundle

Per-language data lives in Fragments/{Lang}/Directives.lean.

inductive Typology.MorphImpType : Type

WALS Ch 70: whether a language has a dedicated morphological imperative, and if so whether the paradigm extends beyond 2nd person. @cite{van-der-auwera-lejeune-2013}: 426/548 (77.7%) of sampled languages have some morphological imperative; only 122 lack one entirely.

• secondOnly : MorphImpType

  Dedicated morphological imperative for second person only (e.g., English Go!, Turkish Gel!).

• secondAndOther : MorphImpType

  Morphological imperative for second person and other persons (1st-inclusive, 3rd jussive; e.g., Latin i/eamus, Quechua).

• noMorphological : MorphImpType

  No dedicated morphological imperative; commands use bare stems, indicative forms, particles, or intonation (e.g., Mandarin Chinese, many isolating languages).

@[implicit_reducible]

instance Typology.instDecidableEqMorphImpType : DecidableEq MorphImpType

Equations

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

@[implicit_reducible]

instance Typology.instReprMorphImpType : Repr MorphImpType

Equations

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

def Typology.instReprMorphImpType.repr : MorphImpType → Nat → Std.Format

Equations

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

inductive Typology.ProhibitiveType : Type

WALS Ch 71: how prohibitives ("Don't!") are formed. Cross-tabulation of two binary features: is the imperative construction the SAME as the affirmative or SPECIAL, and is the negation strategy SAME as in declaratives or SPECIAL? Yields four structural types.

The key typological finding (@cite{van-der-auwera-lejeune-2013}): Type 1 (normal+normal) is surprisingly uncommon — languages tend to treat prohibitives differently from simple negation of an imperative.

• normalImpNormalNeg : ProhibitiveType

  Type 1: normal imperative + normal negation (e.g., Korean kala → kaci malla; Hungarian menj! → ne menj!).

• normalImpSpecialNeg : ProhibitiveType

  Type 2: normal imperative + special negation (e.g., Ancient Greek declarative ou vs imperative mē).

• specialImpNormalNeg : ProhibitiveType

  Type 3: special imperative + normal negation (e.g., Italian va! → non andare!, infinitive replaces imperative).

• specialImpSpecialNeg : ProhibitiveType

  Type 4: special imperative + special negation (e.g., Latin ne eas!; many Austronesian and African languages).

@[implicit_reducible]

instance Typology.instDecidableEqProhibitiveType : DecidableEq ProhibitiveType

Equations

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

def Typology.instReprProhibitiveType.repr : ProhibitiveType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprProhibitiveType : Repr ProhibitiveType

Equations

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

inductive Typology.ImpHortSystem : Type

WALS Ch 72: paradigm richness for non-2nd-person commands. Whether the language has morphological hortative (1st-person let's) and/or jussive (3rd-person let him) in addition to the basic 2nd-person imperative.

• imperativeOnly : ImpHortSystem

  Imperative only: morphological 2nd-person commands but no dedicated hortative or jussive (e.g., English uses periphrastic let's).

• imperativeAndHortative : ImpHortSystem

  Imperative + hortative: morphological 2SG + 1PL forms (e.g., Turkish gel! / gelelim).

• imperativeAndJussive : ImpHortSystem

  Imperative + jussive: morphological 2nd + 3rd person forms (e.g., Hindi-Urdu jao / jaae).

• allThree : ImpHortSystem

  All three: dedicated 2nd, 1st, and 3rd-person command forms (e.g., Latin i/eamus/eat; Georgian; Quechua).

@[implicit_reducible]

instance Typology.instDecidableEqImpHortSystem : DecidableEq ImpHortSystem

Equations

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

@[implicit_reducible]

instance Typology.instReprImpHortSystem : Repr ImpHortSystem

Equations

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

def Typology.instReprImpHortSystem.repr : ImpHortSystem → Nat → Std.Format

Equations

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

inductive Typology.OptativePresence : Type

WALS Ch 73: whether the language has a morphologically dedicated optative (mood expressing wishes: may it rain, if only she were here). Languages that express wishes only via particles, intonation, or subjunctive forms shared with other functions are classified as lacking a dedicated optative.

• present : OptativePresence

  Morphologically dedicated optative present (e.g., Ancient Greek -oimi, Turkish -sA, Georgian).

• absent : OptativePresence

  No dedicated morphological optative; wishes via subjunctive, particles, conditional, or periphrasis (e.g., English, Mandarin, Japanese).

@[implicit_reducible]

instance Typology.instDecidableEqOptativePresence : DecidableEq OptativePresence

Equations

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

def Typology.instReprOptativePresence.repr : OptativePresence → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprOptativePresence : Repr OptativePresence

Equations

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

structure Typology.ImperativeProfile : Type

A language's imperative-system profile across @cite{wals-2013} Chs 70–73.

• language : String
• iso : String
• morphImp : MorphImpType

  Ch 70: morphological imperative type.

• prohibitive : ProhibitiveType

  Ch 71: prohibitive construction type.

• impHortSystem : ImpHortSystem

  Ch 72: imperative-hortative system.

• optative : Option OptativePresence

  Ch 73: optative presence (none if language not in Ch 73 sample).

• impForms : List String

  Illustrative imperative form(s) for documentation.

• notes : String

  Notes on the imperative system.

def Typology.instReprImperativeProfile.repr : ImperativeProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprImperativeProfile : Repr ImperativeProfile

Equations

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

def Typology.ImperativeProfile.hasMorphImp (p : ImperativeProfile) : Bool

Does a language have a morphological imperative (of any type)?

Equations

• p.hasMorphImp = (p.morphImp != Typology.MorphImpType.noMorphological)

def Typology.ImperativeProfile.hasExtendedParadigm (p : ImperativeProfile) : Bool

Does a language have an extended imperative paradigm (beyond 2nd person)?

Equations

• p.hasExtendedParadigm = (p.morphImp == Typology.MorphImpType.secondAndOther)

def Typology.ImperativeProfile.hasHortative (p : ImperativeProfile) : Bool

Does a language have a hortative?

Equations

• p.hasHortative = (p.impHortSystem == Typology.ImpHortSystem.imperativeAndHortative || p.impHortSystem == Typology.ImpHortSystem.allThree)

def Typology.ImperativeProfile.hasJussive (p : ImperativeProfile) : Bool

Does a language have a jussive?

Equations

• p.hasJussive = (p.impHortSystem == Typology.ImpHortSystem.imperativeAndJussive || p.impHortSystem == Typology.ImpHortSystem.allThree)

def Typology.ImperativeProfile.hasOptative (p : ImperativeProfile) : Bool

Does a language have a dedicated optative?

Equations

• p.hasOptative = (p.optative == some Typology.OptativePresence.present)

def Typology.ImperativeProfile.hasSpecialProhibitive (p : ImperativeProfile) : Bool

Does a language use a special prohibitive construction (Type 2/3/4) — i.e., does the prohibitive differ from simply negating the imperative?

Equations

• p.hasSpecialProhibitive = (p.prohibitive != Typology.ProhibitiveType.normalImpNormalNeg)

def Typology.fromWALS70A : Data.WALS.F70A.MorphologicalImperative → Option MorphImpType

Convert WALS 70A (number distinctions in 2nd-person imperative) into the substrate enum. F70A tracks number distinctions, not whether the paradigm extends to other persons, so only noSecondPersonImperatives produces a determinate noMorphological value; other values return none.

Equations

• Typology.fromWALS70A Data.WALS.F70A.MorphologicalImperative.noSecondPersonImperatives = some Typology.MorphImpType.noMorphological
• Typology.fromWALS70A x✝ = none

def Typology.fromWALS71A : Data.WALS.F71A.Prohibitive → ProhibitiveType

Convert WALS 71A prohibitive values into the substrate enum (one-to-one).

Equations

• Typology.fromWALS71A Data.WALS.F71A.Prohibitive.normalImperativeNormalNegative = Typology.ProhibitiveType.normalImpNormalNeg
• Typology.fromWALS71A Data.WALS.F71A.Prohibitive.normalImperativeSpecialNegative = Typology.ProhibitiveType.normalImpSpecialNeg
• Typology.fromWALS71A Data.WALS.F71A.Prohibitive.specialImperativeNormalNegative = Typology.ProhibitiveType.specialImpNormalNeg
• Typology.fromWALS71A Data.WALS.F71A.Prohibitive.specialImperativeSpecialNegative = Typology.ProhibitiveType.specialImpSpecialNeg

def Typology.fromWALS72A : Data.WALS.F72A.ImperativeHortativeSystems → Option ImpHortSystem

Convert WALS 72A imperative-hortative system values into the substrate enum. WALS uses maximalSystem / minimalSystem / bothTypesOfSystem / neitherTypeOfSystem; only the two extreme values map cleanly to the substrate's four-way split.

Equations

• Typology.fromWALS72A Data.WALS.F72A.ImperativeHortativeSystems.neitherTypeOfSystem = some Typology.ImpHortSystem.imperativeOnly
• Typology.fromWALS72A Data.WALS.F72A.ImperativeHortativeSystems.maximalSystem = some Typology.ImpHortSystem.allThree
• Typology.fromWALS72A x✝ = none

def Typology.fromWALS73A : Data.WALS.F73A.Optative → OptativePresence

Convert WALS 73A optative values into the substrate enum (one-to-one).

Equations

• Typology.fromWALS73A Data.WALS.F73A.Optative.present = Typology.OptativePresence.present
• Typology.fromWALS73A Data.WALS.F73A.Optative.absent = Typology.OptativePresence.absent

structure Typology.MorphImpCounts : Type

WALS Ch 70 distribution: morphological imperative number distinctions (n = 548).

• secondSingularAndSecondPlural : Nat
• secondSingular : Nat
• secondPlural : Nat
• secondPersonNumberNeutral : Nat
• noSecondPersonImperatives : Nat

@[implicit_reducible]

instance Typology.instReprMorphImpCounts : Repr MorphImpCounts

Equations

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

def Typology.instReprMorphImpCounts.repr : MorphImpCounts → Nat → Std.Format

Equations

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

def Typology.MorphImpCounts.total (c : MorphImpCounts) : Nat

Equations

• c.total = c.secondSingularAndSecondPlural + c.secondSingular + c.secondPlural + c.secondPersonNumberNeutral + c.noSecondPersonImperatives

def Typology.MorphImpCounts.withMorphImp (c : MorphImpCounts) : Nat

Total languages in the Ch 70 sample with some morphological imperative.

Equations

• c.withMorphImp = c.secondSingularAndSecondPlural + c.secondSingular + c.secondPlural + c.secondPersonNumberNeutral

def Typology.ch70Distribution : MorphImpCounts

WALS Ch 70 counts (548 languages, @cite{van-der-auwera-lejeune-2013}).

Equations

• Typology.ch70Distribution = { secondSingularAndSecondPlural := 292, secondSingular := 78, secondPlural := 38, secondPersonNumberNeutral := 18, noSecondPersonImperatives := 122 }

structure Typology.ProhibitiveCounts : Type

WALS Ch 71 distribution: prohibitive types (n = 496).

• normalImpNormalNeg : Nat
• normalImpSpecialNeg : Nat
• specialImpNormalNeg : Nat
• specialImpSpecialNeg : Nat

@[implicit_reducible]

instance Typology.instReprProhibitiveCounts : Repr ProhibitiveCounts

Equations

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

def Typology.instReprProhibitiveCounts.repr : ProhibitiveCounts → Nat → Std.Format

Equations

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

def Typology.ProhibitiveCounts.total (c : ProhibitiveCounts) : Nat

Equations

• c.total = c.normalImpNormalNeg + c.normalImpSpecialNeg + c.specialImpNormalNeg + c.specialImpSpecialNeg

def Typology.ProhibitiveCounts.special (c : ProhibitiveCounts) : Nat

Languages with any "special" prohibitive (Types 2, 3, 4).

Equations

• c.special = c.normalImpSpecialNeg + c.specialImpNormalNeg + c.specialImpSpecialNeg

def Typology.ch71Distribution : ProhibitiveCounts

WALS Ch 71 counts (496 languages).

Equations

• Typology.ch71Distribution = { normalImpNormalNeg := 113, normalImpSpecialNeg := 182, specialImpNormalNeg := 55, specialImpSpecialNeg := 146 }

structure Typology.ImpHortCounts : Type

WALS Ch 72 distribution: imperative-hortative systems (n = 375). The WALS coding splits languages by paradigm shape: maximal (full hortative+ jussive), minimal (only the basic split), both, or neither.

• neitherTypeOfSystem : Nat
• minimalSystem : Nat
• maximalSystem : Nat
• bothTypesOfSystem : Nat

@[implicit_reducible]

instance Typology.instReprImpHortCounts : Repr ImpHortCounts

Equations

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

def Typology.instReprImpHortCounts.repr : ImpHortCounts → Nat → Std.Format

Equations

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

def Typology.ImpHortCounts.total (c : ImpHortCounts) : Nat

Equations

• c.total = c.neitherTypeOfSystem + c.minimalSystem + c.maximalSystem + c.bothTypesOfSystem

def Typology.ch72Distribution : ImpHortCounts

WALS Ch 72 counts (375 languages).

Equations

• Typology.ch72Distribution = { neitherTypeOfSystem := 201, minimalSystem := 20, maximalSystem := 133, bothTypesOfSystem := 21 }

structure Typology.OptativeCounts : Type

WALS Ch 73 distribution: optative presence (n = 319).

• present : Nat
• absent : Nat

@[implicit_reducible]

instance Typology.instReprOptativeCounts : Repr OptativeCounts

Equations

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

def Typology.instReprOptativeCounts.repr : OptativeCounts → Nat → Std.Format

Equations

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

def Typology.OptativeCounts.total (c : OptativeCounts) : Nat

Equations

• c.total = c.present + c.absent

def Typology.ch73Distribution : OptativeCounts

WALS Ch 73 counts (319 languages).

Equations

• Typology.ch73Distribution = { present := 48, absent := 271 }

theorem Typology.morph_imp_dominant : ch70Distribution.withMorphImp > ch70Distribution.noSecondPersonImperatives * 3

Languages with some morphological imperative (426/548 = 77.7%) vastly outnumber those without (122/548 = 22.3%): the former exceed the latter by more than 3:1.

theorem Typology.sg_pl_most_common : ch70Distribution.secondSingularAndSecondPlural > ch70Distribution.secondPersonNumberNeutral ∧ ch70Distribution.secondSingularAndSecondPlural > ch70Distribution.noSecondPersonImperatives ∧ ch70Distribution.secondSingularAndSecondPlural > ch70Distribution.secondSingular ∧ ch70Distribution.secondSingularAndSecondPlural > ch70Distribution.secondPlural

Two-number imperatives (singular and plural distinguished) are the single most common Ch 70 type: 292 of 548 languages.

theorem Typology.prohibitive_mostly_special : ch71Distribution.special > ch71Distribution.normalImpNormalNeg * 3

van der Auwera's key finding: the majority of languages (383/496 = 77.2%) use a special prohibitive construction (Types 2, 3, or 4). Only 113/496 (22.8%) use Type 1 (normal imperative + normal negation). Prohibitives are typologically marked relative to affirmative imperatives.

theorem Typology.type2_most_common_prohibitive : ch71Distribution.normalImpSpecialNeg > ch71Distribution.specialImpSpecialNeg ∧ ch71Distribution.specialImpSpecialNeg > ch71Distribution.normalImpNormalNeg ∧ ch71Distribution.normalImpNormalNeg > ch71Distribution.specialImpNormalNeg

Type 2 (normal imperative + special negation) is the single most common prohibitive type, followed by Type 4, then Type 1, then Type 3.

theorem Typology.neither_system_majority : ch72Distribution.neitherTypeOfSystem * 2 > ch72Distribution.total

More than half of languages (201/375 = 53.6%) have neither type of imperative-hortative system — i.e., the imperative paradigm does not extend morphologically to 1st-person hortative or 3rd-person jussive.

theorem Typology.minimal_system_rarest : ch72Distribution.minimalSystem < ch72Distribution.bothTypesOfSystem ∧ ch72Distribution.minimalSystem < ch72Distribution.maximalSystem ∧ ch72Distribution.minimalSystem < ch72Distribution.neitherTypeOfSystem

Minimal systems (only one of hortative/jussive) are the rarest type.

theorem Typology.maximal_more_common_than_minimal : ch72Distribution.maximalSystem > ch72Distribution.minimalSystem + ch72Distribution.bothTypesOfSystem

Maximal systems (full hortative + jussive paradigm) are much more common than minimal or both-types systems.

theorem Typology.optative_minority : ch73Distribution.absent > ch73Distribution.present * 5

Dedicated optatives are a minority feature: 271 of 319 languages lack one, outnumbering those with optatives by more than 5:1.