将函数表示为类型

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

我不太清楚你的目标是什么，所以我会尝试指出一些你可能想要阅读的相关术语。

函数不仅有 return 类型，还有描述其参数的类型。所以 f 的 (Haskell) 类型读取 "f takes an Int and a Float, and returns a List of Floats."

f :: Int -> Float -> [Float]
f i x = replicate i x

类型还可以描述更多的函数规范。在这里，我们可能希望类型说明列表的长度与第一个参数相同，或者列表的每个元素都与第二个参数相同。长度索引列表（通常称为向量）是依赖类型的第一个常见示例。

您可能还对将类型作为参数的函数和 return 类型感兴趣。这些有时称为 "type-level functions"。在 Coq 或 Idris 中，它们的定义方式与更熟悉的函数相同。在Haskell中，我们通常使用Type Families, or using Type Classes with Functional Dependencies.

来实现它们

回到问题的第一部分，Beta Reduction 是为函数的每个参数填充具体值的过程。我听说有人将表达式描述为 "after reduction" 或 "fully reduced" 以强调此过程中的某个阶段。这类似于函数 Call Site，但强调表达式和参数，而不是周围的上下文。

Answer 2

我认为问题是直接基于实现的类型（我们称之为 "i-types"）似乎不是很有用，我们已经有了很好的建模方法（称为 "programs" -- 哈哈).

在您的具体示例中，您函数的完整 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))

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

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

i-type 和实现完全一样。

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

特别是，"modelling" Haskell 中类型级别的这些 i 类型似乎效率不高。 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 类型建模！您甚至可以使用 GHCi 查询派生参数和 return 类型：

> :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
}

同样，您最好定义一个任意的术语级别 Char，例如：

someChar :: Char
someChar = undefined

并在术语级别对此 i 类型建模：

f n = if even n then someChar else someChar

再说一次，只要你没有运行这个程序，你已经成功建模了f的i类型，可以查询它的参数和return类型，将其作为更大程序的一部分进行类型检查等。

将函数表示为类型

Representing Functions as Types

function

haskell

coq

type-theory