时间戳

首页 > 解决方案 > 将函数表示为类型

function - 将函数表示为类型

问题描述

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

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] 类型。但我想知道一个函数是否可以被认为是一种类型，如果可以，如何将它建模为面向类型理论的语言中的一种类型，在该语言中它对函数的实际实现进行建模。

标签： functionhaskellcoqtype-theory

解决方案

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

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

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

只是实现本身的一种冗长的替代语法。也就是说，我们可以将这个 i-type（以类似 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-type 和实现是完全一样的。

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

特别是，在 Haskell 的类型级别“建模”这些 i-types 似乎并不高效。Haskell 已经可以在术语级别对它们进行建模。只需将您的 i-types 编写为 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-types！您甚至可以使用 GHCi 查询派生参数和返回类型：

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

现在，您可能正在想象在某些情况下实现和 i-type 会发生分歧，也许当您开始引入文字值时。例如，也许你觉得像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
}

不过，同样，您最好定义一个任意的 term-level Char，例如：

someChar :: Char
someChar = undefined

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

f n = if even n then someChar else someChar

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

推荐阅读