请求明确类型函数式编程中promotion与lifting的精确定义

一、Promotion（提升） #

核心定义 #

Promotion的本质是将某一层级的实体（值、类型）向上迁移到更高层级的同构/关联实体，迁移后实体的核心语义保持一致，但所处的上下文层级更高。

适用场景 #

基础值级场景

• 数值类型的隐式/显式转换：比如C中char转int（窄值域值提升到宽值域类型，语义仍为数值）；Haskell中Integer转为Expr（具体数值提升为抽象语法树节点，语义从“具体值”变为“表达式节点”）。
• 核心特征：实体本身的语义被保留，仅所处的类型/上下文层级提升。

类型级场景（GHC -XDataKinds 扩展）

• 开启-XDataKinds后，promotion指将值级的数据构造器提升为类型级构造器，将值级类型提升为种类（Kind）。例如：

  -- 值级类型定义
  data Nat = Zero | Succ Nat
  

  提升后，Nat成为种类Nat :: *，Zero、Succ成为类型级构造器Zero :: Nat、Succ :: Nat -> Nat，让类型系统可直接复用值级结构进行类型计算。

二、Lifting（升阶） #

核心定义 #

Lifting的本质是将作用于低层级实体的操作（函数、运算），扩展为可作用于高层级容器/上下文的操作，操作的核心逻辑不变，但能处理包裹在容器/上下文中的实体。

适用场景 #

基础容器场景

• Functor的fmap是典型案例：fmap (+1) [1,2,3]中，原本作用于Int的(+1)函数，被升阶为可作用于[Int]列表容器的函数，核心逻辑仍是给数值加1，但适配了列表上下文。
• 同类场景包括Monad的liftM、Applicative的liftA，均为普通函数向Monad/Applicative上下文的升阶。

类型级场景（GADTs、类型类）

• 在GADTs中，可将作用于普通类型的函数升阶为适配GADT类型索引约束的函数。例如：

  data Vec n a where
    VNil :: Vec Zero a
    VCons :: a -> Vec n a -> Vec (Succ n) a
  

  普通的a -> b函数可通过GADT版本的fmap升阶为Vec n a -> Vec n b，既保留原函数逻辑，又维持了向量长度的类型约束。
• Haskell的Data.Type.Lift模块提供的liftTyped，可将类型级字面量升阶为值级表达式（如liftTyped 5将类型级5转为值级Exp Int），实现类型级实体到值级操作的适配。

三、术语区别与严谨性 #

核心区别 #

• Promotion：实体本身的层级迁移（值→类型、类型→种类），迁移后是独立的更高层级实体；
• Lifting：操作的上下文扩展（普通函数→容器函数、值级操作→类型级操作），扩展后是原操作在更高层级的适配版本。

术语严谨性 #

• 这两个术语无完全统一的“正式标准定义”，但社区已形成约定俗成的用法边界：
  • 涉及“层级向上迁移实体”时用promotion；
  • 涉及“扩展操作适配更高层级上下文”时用lifting；
• Haskell官方文档与学术文献中，-XDataKinds的类型迁移明确称为promotion，Functor/Monad的函数扩展明确称为lifting，这是最严谨的用法；
• 需避免混淆：不要将fmap的操作称为promotion，也不要将DataKinds的类型迁移称为lifting，遵循社区共识可减少歧义。

内容的提问来源于stack exchange，提问作者Theo H