将函数表示为类型

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
    },
    ...
  }
}

但我不确定我是不是在正确的轨道上。我知道你可以说函数有一个返回类型。但我想知道一个函数是否可以被认为是一种类型，如果是的话，如何在面向类型的语言中将它建模为一种类型，在这种语言中，它对函数的实际实现进行建模。

Answer 1

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

在您的具体示例中，您的函数的完整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类型和实现是完全相同的。

你会怎么使用这些I-类型？编译器可以通过派生参数和返回类型来使用它们来检查程序.(幸运的是，有一些众所周知的算法，比如算法W，用于从这类类型的I-类型同时派生和类型检查参数和返回类型。)程序员可能不会直接使用i-types -它们太复杂了，无法用于重构或对程序行为进行推理。他们可能希望查看编译器为参数和返回类型派生的类型。

特别是，在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-类型进行建模：

f n = if even n then someChar else someChar

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

Answer 2

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

函数不仅具有返回类型，而且还具有描述其参数的类型。因此，(Haskell)类型的f会读到"f接受Int和Float，并返回浮点数列表。“

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

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

您还可能对将类型作为参数和返回类型的函数感兴趣。这些有时被称为“类型级函数”。在Coq或Idris中，可以像定义更熟悉的函数一样定义它们。在Haskell中，我们通常使用类型家族或使用功能依赖的Type类来实现它们。

回到问题的第一部分，β还原是为每个函数的参数填充具体值的过程。我听说过人们用“后还原”或“完全缩减”来形容表达，以强调这个过程中的某个阶段。这类似于函数调用站点，但强调表达式&参数，而不是周围的上下文。