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

Question

是否有一种类型化的编程语言，我可以像以下两个示例一样约束类型？

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

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

离散概率分布是一个映射，其中：键都应该是相同的类型，值都是概率，并且值的总和 = 1.0。
```
type DPD<K> subtype of map<K, Probability>
where
    sum(values) = 1.0
```

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

score 31 · Accepted Answer

您想要的称为细化类型。

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

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

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

score 26 · Accepted Answer

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

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

{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 的一个小子集，具有“每个构造函数只有一个案例”之类的规则。）这意味着这种风格的细化类型没有那么强大，但比完整的更容易使用-on 依赖类型，使它们更实用。

score 10 · Accepted Answer

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

具体针对您的问题：

subset Probability of Real where 0 .. 1;

和

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

（注意：在当前的实现中，“where”部分是在运行时检查的，但由于“真实类型”是在编译时检查的（包括你的类），并且由于is purestd (主要是 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 什么，真的 - 多方法或其他），我们可以基于它进行调度：

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

score 7 · Accepted Answer

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

type
  TSubrange = range[0..5]

score 2 · Accepted Answer

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

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 求解器静态验证这些不变量和前置/后置条件。这可以很好地处理上述示例，但目前在处理涉及数组和循环不变量的更复杂示例时遇到了困难。

score 2 · Accepted Answer

2

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

于 2014-08-30T00:29:15.303 回答

score 1 · Accepted Answer

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

问题的第一部分是直截了当的，因为自从提出这个问题以来，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 表的尝试。

score 0 · Accepted Answer

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

TYPE PROBABILITY = [0..100]

根据需要添加有效数字。

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

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

8 回答 8

Related

Reference