function - 将函数表示为类型

Question

函数可以是高度嵌套的结构:

function a(x) {
  return b(c(x), d(e(f(x), g())))
}

首先，想知道函数是否有实例。实例。也就是说，函数的评估是函数的实例。从这个意义上来说，类型就是函数，实例就是函数的求值。如果可以，那么如何将函数建模为类型(使用某种面向类型理论的语言，如 Haskell 或 Coq)。

几乎就像:

type a {
  field: x
  constructor b {
    constructor c {
      parameter: x
    },
    ...
  }
}

但我不确定我是否走在正确的道路上。我知道你可以说函数有 [return] 类型。但我想知道一个函数是否可以被视为一种类型，如果可以，如何将其建模为面向类型理论的语言中的类型，其中它对函数的实际实现进行建模。

Answer 1

我认为问题在于直接基于实现的类型(让我们称之为“i-types”)似乎不太有用，而且我们已经有了很好的建模方法(称为“程序”——哈哈) )。

在您的具体示例中，函数的完整 i 类型，即:

type a {
  field: x
  constructor b {
    constructor c {
      parameter: x
    },
    constructor d {
      constructor e { 
        constructor f { 
          parameter: x 
        } 
        constructor g {
        }
    }
  }
}

只是实现本身的一种冗长的替代语法。也就是说，我们可以将这个 i 类型(用类似 Haskell 的语法)写成:

itype a :: a x = b (c x) (d (e (f x) g))

另一方面，我们可以将您的函数实现直接转换为 Haskell 术语级语法，将其编写为:

a x = b (c x) (d (e (f x) g))

并且 i 类型和实现是完全相同的。

您将如何使用这些 i 类型？编译器可能通过派生参数和返回类型来使用它们来对程序进行类型检查。 (幸运的是，有一些众所周知的算法，例如 Algorithm W ，用于同时从此类 i 类型中派生和类型检查参数和返回类型。)程序员可能不会直接使用 i 类型 - 它们是太复杂，无法用于重构或推理程序行为。他们可能想查看编译器为参数和返回类型派生的类型。

特别是，在 Haskell 中的类型级别“建模”这些 i 类型似乎并不高效。 Haskell 已经可以在术语级别对它们进行建模。只需将您的 i 类型编写为 Haskell 程序即可:

a x = b (c x) (d (e (f x) g))
b s t = sqrt $ fromIntegral $ length (s ++ t)
c = show
d = reverse
e c ds = show (sum ds + fromIntegral (ord c))
f n = if even n then 'E' else 'O'
g = [1.5..5.5]

并且不要运行它。恭喜，您已成功建模这些 i 类型!您甚至可以使用 GHCi 查询派生参数和返回类型:

> :t a
a :: Floating a => Integer -> a   -- "a" takes an Integer and returns a float
>

现在，您可能会想象在某些情况下实现和 i 类型会出现分歧，也许是在您开始引入文字值时。例如，也许你感觉像上面的函数f:

f n = if even n then 'E' else 'O'

应分配如下所示的类型，该类型不依赖于特定的文字值:

type f {
  field: n
  if_then_else {
    constructor even {    -- predicate
      parameter: n
    }
    literal Char          -- then-branch
    literal Char          -- else-branch
}

不过，您最好定义任意术语级 Char，例如:

someChar :: Char
someChar = undefined

并在术语级别对此 i-type 进行建模:

f n = if even n then someChar else someChar

同样，只要您不运行该程序，您就已经成功建模了 f 的 i 类型，可以查询其参数和返回类型，将其作为更大的程序等。