Documentation

Linglib.Typology.Adposition

Adposition typology: shared substrate type #

@cite{dryer-2013-wals} @cite{greenberg-1963} @cite{dryer-1992}

Framework-agnostic enum for storing per-language adposition order (WALS Ch 85). Lives in Typology/ so both Fragments/ (per-language profiles) and Phenomena/ (cross-linguistic generalisations) can import without violating the layered dependency hierarchy.

Sister substrate to Typology.WordOrder — same shape (enum with WALS-attested cases plus epistemic-distinction cases, namespaced AdpositionOrder.ofWALS{85A,} converters, classification predicates, head-direction projection).

Epistemic distinction: noDominant vs notInWALS #

AdpositionOrder.noDominant is the WALS-attested mixed-system code (language has both pre- and postpositions, neither dominates — itself a finding). AdpositionOrder.notInWALS is absence from Ch 85 — the language was not coded. A consumer that filtered on ≠ .noDominant would otherwise silently include unencoded languages as "genuinely nondominant". The two cases are kept distinct, mirroring Typology.WordOrder's post-refactor design.

noAdpositions as a category #

WALS codes ~30 languages as .noAdpositions (case-marking alone, no adposition morphology). This is distinct from noDominant (language has both) and from notInWALS (uncoded). All three are framework- neutral.

Greenbergian vs Dryerian primacy #

The substrate is neutral on which classification is theoretically primary. @cite{greenberg-1963}'s Universals 3 and 4 treat adposition as the correlate of basic constituent order (VSO → Prep, SOV → Postp). @cite{dryer-1992} explicitly demoted SOV/SVO/VSO in favour of OV/VO + correlation pairs (Branching Direction Theory), making adposition a co-primary head-direction phenomenon. Consumers downstream choose which projection to read; the substrate provides both IsPrepositional/IsPostpositional (Greenberg-style predicates) and headDirection (Dryer-style projection).

source
inductive Typology.Adposition.AdpositionOrder :
Type

WALS Ch 85 plus the absence-from-WALS case.

  • prepositional : AdpositionOrder

    Adposition precedes complement NP (head-initial PP).

  • postpositional : AdpositionOrder

    Adposition follows complement NP (head-final PP).

  • inpositional : AdpositionOrder

    Adposition appears medially in a complex NP (rare; WALS lists ~8 Australian Aboriginal + Cariban + PNG languages).

  • noAdpositions : AdpositionOrder

    Language has no adpositions (case-marking alone; ~30 WALS languages). Distinct from notInWALS.

  • noDominant : AdpositionOrder

    WALS-attested mixed system (both pre- and postpositions, neither dominates).

  • notInWALS : AdpositionOrder

    Language not coded in WALS Ch 85 (no information). Distinct from noAdpositions (which is a substantive WALS finding).

Instances For
    source
    @[implicit_reducible]
    instance Typology.Adposition.instDecidableEqAdpositionOrder :
    DecidableEq AdpositionOrder
    Equations
    source
    def Typology.Adposition.instReprAdpositionOrder.repr :
    AdpositionOrder → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Typology.Adposition.instReprAdpositionOrder :
      Repr AdpositionOrder
      Equations
      source
      def Typology.Adposition.AdpositionOrder.ofWALS85A :
      Data.WALS.F85A.AdpositionNPOrder → AdpositionOrder

      Convert WALS F85A's AdpositionNPOrder to a local AdpositionOrder.

      Equations
      Instances For
        source
        def Typology.Adposition.AdpositionOrder.ofWALS (iso : String) :
        AdpositionOrder

        Look up Ch 85 adposition order for an ISO 639-3 code. Returns .notInWALS when the language is absent from the chapter.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[reducible, inline]
          abbrev Typology.Adposition.AdpositionOrder.IsPrepositional (a : AdpositionOrder) :
          Prop

          a is prepositional.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Typology.Adposition.AdpositionOrder.IsPostpositional (a : AdpositionOrder) :
            Prop

            a is postpositional.

            Equations
            Instances For
              source
              def Typology.Adposition.AdpositionOrder.headDirection :
              AdpositionOrder → Option HeadDirection

              Project an AdpositionOrder to a HeadDirection. Theory-neutral: prepositional ⇒ head-initial PP, postpositional ⇒ head-final PP. Returns none for the categories that do not commit to a single direction (.inpositional, .noAdpositions, .noDominant, .notInWALS). Sister of OVOrder.verbPosition; consumers needing BDT-style head-direction unification can iterate over both projections.

              Equations
              Instances For