是否存在具有可约束类型的语言？

Question

有没有一种类型化的编程语言可以像下面两个例子那样约束类型？

1. 概率是一个浮点数，最小值为 0.0，最大值为 1.0。

   type Probability subtype of float
   where
       max_value = 0.0
       min_value = 1.0
   

2. 离散概率分布是一个映射，其中：键应该都是同一类型，值都是概率，值的总和 = 1.0。

   type DPD<K> subtype of map<K, Probability>
   where
       sum(values) = 1.0
   

据我了解，这对于 Haskell 或 Agda 是不可能的。

Answer 1

你想要的是refinement types。

可以在 Agda 中定义Probability：Prob.agda

概率质量函数类型，求和条件在第 264 行定义。

与 Agda 相比，有些语言具有更直接的细化类型，例如 ATS

Answer 2

您可以在 Haskell 中使用 Liquid Haskell 执行此操作，它使用 refinement types 扩展 Haskell。谓词在编译时由 SMT 求解器管理，这意味着证明是全自动的，但您可以使用的逻辑受到 SMT 求解器处理的限制。 （令人高兴的是，现代 SMT 求解器相当通用！）

一个问题是我认为 Liquid Haskell 目前不支持浮点数。如果不是这样，应该可以纠正，因为有 用于 SMT 求解器的浮点数理论。您也可以假装浮点数实际上是有理数（甚至在 Haskell 中使用 Rational！）。考虑到这一点，您的第一个类型可能如下所示：

{p : Float | p >= 0 && p <= 1}

您的第二种类型会更难编码，特别是因为地图是一种难以推理的抽象类型。如果您使用配对列表而不是地图，则可以这样编写“度量”：

measure total :: [(a, Float)] -> Float
total []          = 0 
total ((_, p):ps) = p + probDist ps

（您可能也想将[] 包装在newtype 中。）

现在您可以在细化中使用total 来约束列表：

{dist: [(a, Float)] | total dist == 1}

Liquid Haskell 的巧妙之处在于，所有推理都是在编译时为您自动执行的，以换取使用某种受限的逻辑。 （total 之类的度量在编写方式上也受到很大限制——它是 Haskell 的一个小子集，具有“每个构造函数只有一个案例”之类的规则。）这意味着这种风格的细化类型不太强大，但更容易使用比完全依赖的类型更实用。

Answer 3

Perl6 有一个“类型子集”的概念，它可以添加任意条件来创建“子类型”。

专门针对您的问题：

subset Probability of Real where 0 .. 1;

和

role DPD[::T] {
  has Map[T, Probability] $.map
    where [+](.values) == 1; # calls `.values` on Map
}

（注意：在当前的实现中，“where”部分是在运行时检查的，但是因为“真实类型”是在编译时检查的（包括你的类），并且因为有纯注释（@987654325 @) 在 std 中（主要是 perl6）（那些也在 * 等运算符上），这只是一个努力的问题（而且不应该更多）。

更一般地说：

# (%% is the "divisible by", which we can negate, becoming "!%%")
subset Even of Int where * %% 2; # * creates a closure around its expression
subset Odd of Int where -> $n { $n !%% 2 } # using a real "closure" ("pointy block")

然后你可以用智能匹配运算符~~检查一个数字是否匹配：

say 4 ~~ Even; # True
say 4 ~~ Odd; # False
say 5 ~~ Odd; # True

而且，多亏了multi subs（或多种，实际上是多种方法或其他方法），我们可以基于此进行调度：

multi say-parity(Odd $n) { say "Number $n is odd" }
multi say-parity(Even) { say "This number is even" } # we don't name the argument, we just put its type
#Also, the last semicolon in a block is optional

Answer 4

Nimrod 是一种支持这一概念的新语言。它们被称为子范围。这是一个例子。您可以在此处了解有关该语言的更多信息link

type
  TSubrange = range[0..5]

Answer 5

对于第一部分，是的，那就是 Pascal，它具有整数子范围。

Answer 6

Whiley language 支持的内容与您所说的非常相似。例如：

type natural is (int x) where x >= 0
type probability is (real x) where 0.0 <= x && x <= 1.0

这些类型也可以像这样实现为前置/后置条件：

function abs(int x) => (int r)
ensures r >= 0:
    //
    if x >= 0:
        return x
    else:
        return -x

语言非常有表现力。使用 SMT 求解器静态验证这些不变量和前置/后置条件。这可以很好地处理上述示例，但目前在处理涉及数组和循环不变量的更复杂示例时遇到了困难。

Answer 7

对于任何感兴趣的人，我想我会在 Nim 中添加一个示例，说明截至 2019 年如何解决此问题。

问题的第一部分是直截了当的，因为自从提出这个问题以来，Nim 已经获得了在浮点数（以及序数和枚举类型）上生成子范围类型的能力。下面的代码定义了两个新的浮点子范围类型，Probability 和 ProbOne。

问题的第二部分更棘手 - 定义一个对其字段的函数有约束的类型。我提出的解决方案没有直接定义这种类型，而是使用宏 (makePmf) 将常量 Table[T,Probability] 对象的创建与创建有效 ProbOne 对象的能力联系起来（从而确保 PMF 是有效的）。 makePmf 宏在编译时进行评估，确保您无法创建无效的 PMF 表。

请注意，我是 Nim 的新手，所以这可能不是编写此宏的最惯用方式：

import macros, tables

type
  Probability = range[0.0 .. 1.0]
  ProbOne = range[1.0..1.0]

macro makePmf(name: untyped, tbl: untyped): untyped =
  ## Construct a Table[T, Probability] ensuring
  ## Sum(Probabilities) == 1.0

  # helper templates
  template asTable(tc: untyped): untyped =
    tc.toTable

  template asProb(f: float): untyped =
    Probability(f)

  # ensure that passed value is already is already
  # a table constructor
  tbl.expectKind nnkTableConstr
  var
    totprob: Probability = 0.0
    fval: float
    newtbl = newTree(nnkTableConstr)

  # create Table[T, Probability]
  for child in tbl:
    child.expectKind nnkExprColonExpr
    child[1].expectKind nnkFloatLit
    fval = floatVal(child[1])
    totprob += Probability(fval)
    newtbl.add(newColonExpr(child[0], getAst(asProb(fval))))

  # this serves as the check that probs sum to 1.0
  discard ProbOne(totprob)
  result = newStmtList(newConstStmt(name, getAst(asTable(newtbl))))


makePmf(uniformpmf, {"A": 0.25, "B": 0.25, "C": 0.25, "D": 0.25})

# this static block will show that the macro was evaluated at compile time
static:
  echo uniformpmf

# the following invalid PMF won't compile
# makePmf(invalidpmf, {"A": 0.25, "B": 0.25, "C": 0.25, "D": 0.15})

注意：使用宏的一个很酷的好处是nimsuggest（集成到 VS Code 中）甚至会突出显示创建无效 Pmf 表的尝试。

Answer 8

Modula 3 具有子范围类型。 （序数的子范围。）因此，对于您的示例 1，如果您愿意将概率映射到某个精度的整数范围，您可以使用：

TYPE PROBABILITY = [0..100]

根据需要添加有效数字。

参考：有关子范围序数的更多信息here。