为何构造器字段均映射到Void的ExpUD类型能存在有效值？

我正在学习Shayan Najd和Simon Peyton Jones所著的Trees that grow论文以深入理解类型族。论文首先定义了用于建模带整数字面量和显式类型注解的简单类型λ项的不可扩展Exp类型：

type Var = String

data Typ = Int | Fun Typ Typ

data Exp = Lit Int
         | Var Var
         | Ann Exp Typ
         | Abs Var Exp
         | App Exp Exp

该Exp类型无法扩展，既不能新增构造器，也不能为现有构造器添加参数。论文提出的解决方案是将其修改为带xi参数的Exp类型：

data Exp xi = Lit (Xlit xi) Int
            | Var (Xvar xi) Var
            | Ann (Xann xi) (Exp xi) Typ
            | Abs (Xabs xi) Var (Exp xi)
            | App (Xapp xi) (Exp xi) (Exp xi)
            | Exp (Exp xi)

同时定义了对应的类型族及实例：

data UD -- stands for UnDecorated, referring to the AST

type family Xlit xi; type instance Xlit UD = Void
type family Xvar xi; type instance Xvar UD = Void
type family Xann xi; type instance Xann UD = Void
type family Xabs xi; type instance Xabs UD = Void
type family Xapp xi; type instance Xapp UD = Void
type family Xexp xi; type instance Xexp UD = Void

并定义ExpUD = Exp UD，称原Exp与ExpUD的值存在一一对应关系。但我无法理解：由于每个构造器的首个字段都通过类型实例映射为空类型Void，ExpUD为何能存在有效值？

解答 #

核心原因在于Haskell中Void类型的特性，以及我们可以借助Data.Void中的absurd函数来构造ExpUD的有效值：

• Void的本质：Void是一个没有任何构造器的类型，意味着它不存在有效值。但Haskell允许我们使用absurd :: Void -> a这个函数——它是一个总函数（永远不会被实际调用，因为没有Void值需要处理），可以将“不存在的Void值”转换为任意类型。

• 构造ExpUD的智能构造器：对于原Exp的每个构造器，我们可以为ExpUD定义对应的智能构造器，用absurd填充Void类型的参数位置：

  import Data.Void (absurd)
  
  litUD :: Int -> ExpUD
  litUD n = Lit absurd n
  
  varUD :: Var -> ExpUD
  varUD v = Var absurd v
  
  annUD :: ExpUD -> Typ -> ExpUD
  annUD e t = Ann absurd e t
  
  absUD :: Var -> ExpUD -> ExpUD
  absUD v e = Abs absurd v e
  
  appUD :: ExpUD -> ExpUD -> ExpUD
  appUD e1 e2 = App absurd e1 e2
  

• 一一对应的逻辑：

  • 每个原Exp值都可以通过上述智能构造器转换成唯一的ExpUD值；
  • 反过来，对ExpUD的值进行模式匹配时，由于Void参数没有有效值，我们可以用emptyCase（GHC扩展）或者直接忽略该参数（因为它永远不会被匹配到），从而还原出对应的原Exp值。

这种设计的巧妙之处在于，通过类型族的参数化，既保留了原AST的结构（UD场景下），又为后续扩展留下了空间——当需要给构造器添加额外信息时，只需要定义新的xi类型，并为对应的Xlit、Xvar等类型族实例指定非Void的类型即可。

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