如何在类型系统中将类型字段限制为 2 的幂？

问题描述

在一些 JavaScript 代码中有这个：

    $('.likin').click(function(){
$.ajax({
         type: "POST",url: "{% url 'video:like' video.pk %}",data: {'content_id': $(this).attr('name'),'operation':'like_submit','csrfmiddlewaretoken': '{{ csrf_token }}'},dataType: "json",success: function(response) {
          selector = document.getElementsByName(response.next);
                if(response.liked==true){
                  $(selector).css("color","blue");
                }
                else if(response.liked==false){
                  $(selector).css("color","black");
                }


          }

    });

})

本质上，输入 function allocate(bits) { if ((bits & (bits - 1)) != 0) { throw "Parameter is not a power of 2"; } ... } 有一个约束，即它是 2 的幂。或者，与其称其为“约束”，不如说它对输入进行了验证，表明它是 2 的幂。

旁注，我在 SQL 中看到您可以执行以下类型的约束：

bits

但在 SQL 和 JavaScript 示例中，此代码在运行时执行以检查它是否有效。我确定 JS，不完全确定 SQL，但我想这是一个运行时的事情。

我想知道如何在诸如 TypeScript 或其他 programming language with types 之类的健壮类型系统中表达这种“二的幂”约束。理想情况下，它是一个编译时约束。这可能吗？如果是这样，它是如何用某种语言完成的？任何语言都可以，主要是寻找有关如何在具有自己的类型系统的自定义语言中实现这一点的灵感。不完全确定这将如何作为编译时约束工作。它是一个“类型”，“两个整数的幂类型”，但不知道如何表达。

解决方法

解决这个问题的最佳方法并不完全是单一的，因为有多种方法可以进行不同的权衡。以下是 Haskell 中使用的一些主要样式。

“通过构造纠正”

与其接受更通用的类型，如 Int 并在事后尝试约束它，不如引入一种可以只表示有效 2 的幂的类型，或者通过封装验证：

allocate :: PowerOfTwo -> …

module PowerOfTwo
  ( PowerOfTwo  -- Abstract type,powerOfTwo  -- Smart constructor,toInt
  ) where

newtype PowerOfTwo = PowerOfTwo Int

powerOfTwo :: Int -> Maybe PowerOfTwo
powerOfTwo n
  | isPowerOfTwo n = Just (PowerOfTwo n)
  | otherwise = Nothing

toInt :: PowerOfTwo -> Int
toInt (PowerOfTwo n) = n

或者根据使无效状态不可表示的原则，有时可以通过约定来实现：

-- | @'allocate' n@ allocates @2^n@ bits…
allocate :: Word -> …

或者在结构上：

allocate :: PowerOfTwo -> …

-- | This type can /only/ represent 2^n.
-- (Ignore for the moment that it’s quite inefficient!)
data PowerOfTwo
  = One
  | Twice PowerOfTwo

toInt :: PowerOfTwo -> Int
toInt One = 1
toInt (Twice n) = 2 * n

证明和单例

连同输入一起，需要证明输入已经已经被调用者验证；证明只是一个值，只有执行验证才能构造。

在最简单的情况下，这与上面的 newtype 解决方案相同：PowerOfTwo 是一对 Int 和它已被验证的隐式证明。

但是您也可以使这些证明显式，这通常在依赖类型语言中完成，但可以在任何具有表示存在类型的方式的语言中完成，如在 singletons 库或 {{3} } 风格：

-- A type-level proposition that n is a power of 2.
data IsPo2 n

-- A classification of whether a value is a power of 2.
data WhetherPo2 n
  = Po2 (Proof (IsPo2 n))
  | NotPo2 (Proof (Not (IsPo2 n)))

-- Assertion that proposition ‘p’ is true.
data Proof p = TrustMe

-- Encapsulated validation,like above,-- but now it gives back a “proof” value.
validate :: Named n Int -> WhetherPo2 n
validate (Named n)
  | isPowerOfTwo n = Po2 TrustMe
  | otherwise = NotPo2 TrustMe

为了调用‘allocate’，你必须提供一个你验证过输入的证明：

allocate
  :: Named n Int
  -> Proof (IsPo2 n)
  -> …

获得一个的唯一方法是从validate：

-- ‘name’ from the paper gives a type-level name to a value.
name 64 $ \ n -> case validate n of

  -- If we got a proof,we can proceed.
  Po2 p -> allocate n p

  -- Calling ‘allocate’ would be a type error here.
  NotPo2 np -> …

像 Idris 和 ATS 这样的依赖类型语言经常使用这种风格，使用隐式参数等语法糖来帮助减少传递这些证明值的噪音。

改进

某些语言和工具（如 Ghosts of Departed Proofs）包含用于细化类型的求解器，这些类型如 Int 用命题对其进行了改进。在这里，allocate 的输入可以被赋予一个类似 { n:Int | isPowerOfTwo n } 的类型，这是对上述证明进行编码的一种更紧凑的方式。

细化类型检查器通常结合使用显式证明、隐式流敏感分析和数值求解 (SMT) 来验证您是否已测试确保命题成立的条件。这种风格的优点是易于阅读，但遗憾的是，对于复杂命题，使用基于启发式求解器的方法很难预测验证何时会失败。

---

我喜欢所有这些样式的一点是它们不需要重复执行验证；一旦你有一个证明证明某些不变量成立，无论是作为结构不变量还是文字证明对象，那么你就可以假设它成立，并使用更有效的代码，否则不安全。