Liquid Haskell精化类型中能否用let绑定简化重复表达式？

Liquid Haskell支持通过逻辑变量实现你想要的“内部定义名称、避免重复书写表达式”的效果，无需自定义虚构语法，具体实现方式如下：

直接使用逻辑变量的写法 #

{-@
  addDigit ::
    c : Bool -> x : Digit -> y : Digit ->
    { v : (Bool, Digit)
    |  exists z:Int. 
         z = x + y + if c then 1 else 0 
         && fst v = (z > 9)
         && (snd v + (if (fst v) then 10 else 0)) == z
    }
@-}

关键说明 #

• 用exists z:Int.引入逻辑变量z，作用完全等价于你虚构的let z = ...，用来复用重复表达式。
• 必须明确标注逻辑变量的类型（比如这里的Int，因为x和y是Digit，相加后可能超出Digit范围）。
• 所有依赖z的约束都写在exists块内，Liquid Haskell会自动推导z与原表达式的等价性。

多场景复用的进阶方式：定义辅助measure #

如果该表达式需要在多个精化类型中复用，可以定义一个带精化的辅助measure：

{-@ measure total :: Bool -> Digit -> Digit -> Int @-}
{-@ total :: c:Bool -> x:Digit -> y:Digit -> {v:Int | v = x + y + if c then 1 else 0} @-}
total c x y = x + y + if c then 1 else 0

{-@
  addDigit ::
    c : Bool -> x : Digit -> y : Digit ->
    { v : (Bool, Digit)
    |  fst v = (total c x y > 9)
         && (snd v + (if (fst v) then 10 else 0)) == total c x y
    }
@-}

这种方式将重复表达式封装成可调用的精化函数，让类型签名更简洁易读。

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