2

在 Ada 中定义自然数可以这样写：

subtype Natural  is Integer range 0 .. Integer'Last;

这是类型安全的，并在编译时进行检查。它简单（一行代码）且高效（它不像许多函数式语言那样使用递归来定义自然数）。有没有可以提供类似功能的功能语言？

谢谢

4

2 回答 2

3

这是类型安全的，并在编译时进行检查。

正如您在对问题的评论中已经指出的那样，在编译时不会对其进行检查。Modula-2 或任何其他可用于生产的通用编程语言中都没有等效功能。

在编译时检查这样的约束的能力需要依赖类型、细化类型或类似的结构。您可以在Coq或Agda等定理证明器或ATS或Liquid Haskell等实验/学术语言中找到这些特性。

现在我提到的那些语言中，Coq 和 AgdaNat递归地定义了它们的类型，所以这不是你想要的，而且 ATS 是一种命令式语言。这样就剩下 Liquid Haskell（当然还有我没有提到的语言）。Liquid Haskell 是带有额外类型注释的 Haskell，因此它绝对是一种函数式语言。在 Liquid Haskell 中，您可以定义一个MyNat（Nat已在标准库中定义的类型）类型，如下所示：

{-@ type MyNat = {n:Integer | n >= 0} @-}

然后像这样使用它：

{-@ fac :: MyNat -> MyNat @-}
fac :: Integer -> Integer
fac 0 = 1
fac n = n * fac (n-1)

如果您随后尝试fac使用负数作为参数进行调用，则会出现编译错误。如果您使用用户输入作为参数调用它，您也会收到编译错误，除非您专门检查输入是否为非负数。如果您删除了该行，您也会收到编译错误，fac 0 = 1因为现在n下一行可能为 0，n-1当您调用 时为负数fac (n-1)，因此编译器会拒绝它。

应该注意的是，即使使用最先进的类型推断技术，像这样的语言中的非平凡程序最终也会具有相当复杂的类型签名，并且您将花费大量时间和精力来追踪类型错误。复杂的类型签名丛林，只有难以理解的类型错误来指导您。因此，这些功能为您提供的安全性是有代价的。还应该指出的是，在图灵完备的语言中，您有时必须为您知道不可能发生的情况编写运行时检查，因为即使您认为应该证明编译器也无法证明一切。

于 2013-09-15T13:55:57.593 回答
1

Typed Racket 是 Racket 的一种类型化方言，具有丰富的数字子类型集，并且它知道相当数量的闭包属性（例如，两个非负数之和是非负数，两个精确整数之和是一个精确整数等）。这是一个简单的例子：

#lang typed/racket
(: f : (Nonnegative-Integer Nonnegative-Integer -> Positive-Integer))
(define (f x y)
  (+ x y 1))

类型检查是静态完成的，但是类型检查器当然不能证明关于数字子类型的每一个真实事实。例如，下面的函数实际上只返回 type 的值Nonnegative-Integer，但是减法的类型规则只允许 TR 得出 的结果类型Integer。

> (lambda: ([x : Nonnegative-Integer] [y : Nonnegative-Integer])
    (- x (- x y)))
- : (Nonnegative-Integer Nonnegative-Integer -> Integer)
#<procedure>

St-Amour 等人在Typing the Numeric Tower中描述了 Typed Racket 的数字方法（出现在 PADL 2012）。这里通常有一个指向该论文的链接，但该链接目前似乎已断开。如果您搜索标题，Google 会将 PDF 缓存呈现为 HTML。

于 2013-09-16T00:21:25.113 回答