Chr*_*lor 277 ocaml haskell functional-programming algebraic-data-types miranda
代数数据类型的"代数"表达式对于具有数学背景的人来说非常具有启发性.让我试着解释一下我的意思.
定义了基本类型
•+X1并使用简写X²的X•X和2X对X+X等等,我们就可以定义如链表代数表达式
data List a = Nil | Cons a (List a) ↔ L = 1 + X • L
和二叉树:
data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²
现在,我作为数学家的第一直觉是坚持这些表达方式,并试图解决L和T.我可以通过重复替换来做到这一点,但似乎更容易滥用符号,并假装我可以随意重新排列.例如,对于链接列表:
L = 1 + X • L
(1 - X) • L = 1
L = 1 / (1 - X) = 1 + X + X² + X³ + ...
我用1 / (1 - X)完全不合理的方式使用幂级数展开来得到一个有趣的结果,即一个L类型是Nil,或者它包含1个元素,或者它包含2个元素,或3等.
如果我们为二叉树做它会变得更有趣:
T = 1 + X • T²
X • T² - T + 1 = 0
T = (1 - ?(1 - 4 • X)) / (2 • X)
T = 1 + X + 2 • X² + 5 • X³ + 14 • X? + ...
再次,使用幂级数扩展(使用Wolfram Alpha完成).这表达了非显而易见的(对我来说)事实,即只有一个二元树有1个元素,2个二叉树有两个元素(第二个元素可以在左边或右边的分支上),5个二叉树有三个元素等.
所以我的问题是 - 我在这做什么？这些操作似乎没有道理(无论如何,代数数据类型的平方根究竟是什么？)但它们会产生明显的结果.两种代数数据类型的商是否在计算机科学中有任何意义,还是仅仅是符号的诡计？
而且,或许更有趣的是,是否可以扩展这些想法？是否存在类型代数的理论,例如,允许类型上的任意函数,或类型是否需要幂级数表示？如果你可以定义一类函数,那么函数的组合是否有任何意义？
C. *_*ann 135
免责声明:当你考虑到⊥时,很多这种方法并没有真正起作用,所以为了简单起见,我会公然无视这一点.
一些初步要点:
请注意,"联合"可能不是这里A + B的最佳术语 - 这特别是两种类型的不相交联合,因为即使它们的类型相同,双方也是有区别的.对于它的价值,更常见的术语只是"和型".
单例类型实际上是所有单元类型.它们在代数操作下表现相同,更重要的是,仍然保留了存在的信息量.
您可能也想要零类型.没有标准的,但最常见的名称是Void.没有类型为零的值,就像有一个类型为1的值一样.
这里仍然缺少一个主要的操作,但我马上回过头来看看.
正如您可能已经注意到的那样,Haskell倾向于从类别理论中借用概念,并且所有上述内容都具有非常直接的解释:
给定Hask中的对象A和B ,它们的乘积A×B是唯一的(直到同构)类型,它允许两个投影fst:A×B→A和snd:A×B→B,其中给出任何类型C和函数f:C→A,g:C→B你可以定义配对f &&& g:C→A×B,使得fst∘(f &&&g) = f,同样g.参数化自动保证了通用属性,而我不太精确的名称选择应该会给你一个想法.在(&&&)操作中定义Control.Arrow,顺便说一句.
以上的对偶是产品A + B注入inl:A→A + B和inr:B→A + B,其中给出任何类型C和函数f:A→C,g:B→C,你可以定义copairing f ||| g:A + B→C使得明显的等价性成立.同样,参数化自动保证了大部分棘手的部分.在这种情况下,标准注射是简单的Left,Right并且共处是功能either.
产品和总和类型的许多属性可以从上面得出.请注意,任何单例类型都是Hask的终端对象,任何空类型都是初始对象.
返回上述缺失操作,在笛卡尔闭合类别中,您具有与该类别的箭头对应的指数对象.我们的箭头是函数,我们的对象是具有类型的类型*,并且类型A -> B确实在类型的代数操作的上下文中表现为B A. 如果不明白为什么这应该成立,请考虑类型Bool -> A.只有两个可能的输入,该类型的函数与两个类型的值同构A,即(A, A).因为Maybe Bool -> A我们有三种可能的输入,依此类推.此外,观察到,如果我们改写上述copairing定义中使用代数符号,我们得到了身份Ç 甲 ×C 乙 = C A + B.
至于为什么这一切都有意义 - 特别是为什么你使用幂级数扩展是合理的 - 注意上面的大部分内容是指某种类型的"居民"(即具有该类型的不同值)证明代数行为.要明确这个观点:
产品类型(A, B)表示各自的值,A并且B独立地取得.因此,对于任何固定值a :: A,(A, B)每个居民的类型都有一个值B.这当然是笛卡儿产品,产品类型的居民数量是因素的居民数量的乘积.
总和类型Either A B从任一表示的值A或B,与左,右分支区分.如前所述,这是一个不相交的联盟,总和类型的居民数量是总数的居民数量的总和.
指数类型B -> A表示从类型B值到类型值的映射A.对于任何固定参数b :: B,A可以为其分配任何值; 类型的值B -> A选取为每个输入,这相当于作为许多拷贝的乘积一个这样的映射A为B具有居民,因此求幂.
虽然最初将类型视为集合很诱人,但在这种情况下实际上并不能很好地工作 - 我们有不相交的联合而不是集合的标准联合,对交集或许多其他集合操作没有明显的解释,我们通常不关心集合成员资格(将其留给类型检查器).
另一方面,上面的结构花了很多时间讨论计算居民,并且枚举类型的可能值是一个有用的概念.这很快就会引导我们进行枚举组合,如果你查阅链接的维基百科文章,你会发现它所做的第一件事就是定义"对"和"联合",其含义与产品和总和类型完全相同.生成函数,然后使用完全相同的技术对与Haskell列表相同的"序列"执行相同的操作.
编辑:噢,这是一个快速的奖金,我认为这一点非常引人注目.您在评论中提到,对于树类型,T = 1 + T^2您可以派生标识T^6 = 1,这显然是错误的.但是,T^7 = T 确实存在,并且可以直接构建树和七元组树之间的双射,参见 安德烈亚斯布拉斯的"七棵树合一".
编辑×2:关于其他答案中提到的"类型衍生"结构的主题,你可能也会从同一作者中获得这篇论文,这篇论文进一步建立了这个理念,包括分裂的概念和其他有趣的东西.
sig*_*fpe 44
二元树由T=1+XT^2类型的半环中的等式定义.通过构造,T=(1-sqrt(1-4X))/(2X)在复数的半环中由相同的等式定义.因此,考虑到我们在同一类代数结构中求解相同的方程式,我们看到一些相似之处实际上并不令人惊讶.
问题在于,当我们在复杂数字的半环中推理多项式时,我们通常使用复数形成环或甚至是场的事实,因此我们发现自己使用不适用于半环的减法等操作.但是,如果我们有一条允许我们从方程的两边取消的规则,我们通常可以从我们的论证中消除减法.这是菲奥雷和伦斯特证明的那种事情,表明关于戒指的许多争论可以转移到半环.
这意味着您对戒指的大量数学知识可以可靠地转移到类型上.因此,一些涉及复数或幂级数的论证(在正式权力系列的环中)可以以完全严格的方式延续到类型.
然而,这个故事还有更多.通过显示两个幂级数相等来证明两种类型相等(比如说)是一回事.但您也可以通过检查电源系列中的术语来推断有关类型的信息.我不确定这里的正式声明应该是什么.(我建议布伦特Yorgey的纸张上组合品种的一些工作内容紧密相关,但种不一样的类型.)
我发现完全令人兴奋的是你发现的东西可以扩展到微积分.关于微积分的定理可以转移到类型的半环节.实际上,甚至关于有限差分的论证也可以转移,你会发现数值分析中的经典定理在类型理论中有解释.
玩得开心!
new*_*cct 21
似乎你所做的只是扩展递归关系.
L = 1 + X • L
L = 1 + X • (1 + X • (1 + X • (1 + X • ...)))
= 1 + X + X^2 + X^3 + X^4 ...
T = 1 + X • T^2
L = 1 + X • (1 + X • (1 + X • (1 + X • ...^2)^2)^2)^2
= 1 + X + 2 • X^2 + 5 • X^3 + 14 • X^4 + ...
由于类型操作的规则就像算术运算规则一样,你可以使用代数方法来帮助你弄清楚如何扩展递归关系(因为它并不明显).
yat*_*975 18
我没有完整的答案,但这些操作倾向于"正常工作".一篇相关的论文可能是菲奥雷和伦斯特的"类别为对象的类别" - 我在阅读sigfpe关于相关主题的博客时遇到过那篇文章 ; 该博客的其余部分是类似想法的金矿,值得一试!
顺便说一下,您还可以区分数据类型 - 这将为您提供适合数据类型的Zipper!
And*_*lft 10
通信过程代数(ACP)处理类似的过程表达式.它提供了加法和乘法作为选择和序列的运算符,以及相关的中性元素.基于这些,有其他构造的运算符,例如并行和中断.请参见http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes.还有一篇名为"过程代数简史"的在线论文.
我正致力于使用ACP扩展编程语言.去年四月,我在2012年Scala Days上发表了一篇研究论文,可在http://code.google.com/p/subscript/上找到.
在会议上,我演示了一个运行并行递归规范的调试器:
Bag = A; (袋及一)
其中A和a代表输入和输出动作; 分号和&符号代表顺序和并行.查看SkillsMatter上的视频,可从上一个链接访问.
一个袋子规格更可比
L = 1 + X•L
将会
B = 1 + X&B
ACP使用公理在选择和顺序方面定义并行性; 请参阅维基百科文章.我想知道包包的类比是什么
L = 1 /(1-X)
ACP样式编程对于文本解析器和GUI控制器非常方便.规格如
searchCommand = clicked(searchButton)+ key(回车)
cancelCommand = clicked(cancelButton)+ key(Escape)
可以通过使两个细化"clicked"和"key"隐式(比如Scala允许的函数)更简洁地写下来.因此我们可以写:
searchCommand = searchButton + Enter
cancelCommand = cancelButton + Escape
右侧现在包含作为数据的操作数,而不是进程.在这个级别,没有必要知道隐式改进将把这些操作数转换为进程; 他们不一定会改进投入行动; 输出动作也适用,例如在测试机器人的规范中.
进程以数据的形式获得数据; 因此,我称之为"项代数".
这是另一个小的补充 - 组合扩展系列扩展中的系数应该"起作用"的组合洞察,特别是关注可以使用来自微积分的泰勒 - 麦克劳林方法得出的系列.注意:您给出的操纵列表类型的示例系列扩展是Maclaurin系列.
由于其他答案和评论涉及代数类型表达式(总和,产品和指数)的行为,因此这个答案将忽略该细节并关注类型"微积分".
在这个答案中你可能会注意到引号中的引号很重要.有两个原因:
的麦克劳林级数的函数f : ? ? ?被定义为
f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f???(0)X? + ...
在哪里f???意味着.的n衍生物f.
为了能够理解用类型解释的Maclaurin系列,我们需要理解我们如何在类型上下文中解释三件事:
0(1/n!)事实证明,这些来自分析的概念在类型世界中具有合适的对应物.
"合适的对手"是什么意思？它应该具有同构的味道 - 如果我们能够在两个方向上保存真理,那么在一个上下文中可导出的事实可以转移到另一个上下文中.
那么类型表达式的导数是什么意思呢？事实证明,对于一个大型且表现良好("可区分")类型的表达式和仿函数,有一种自然操作,其行为类似于足以成为合适的解释!
为了破坏妙语,类似于差异化的操作就是制造"单洞背景".这是进一步拓展这一特定点的绝佳场所,但单孔上下文(da/dx)的基本概念是它表示x从一个术语(类型a)中提取特定类型()的单个子项的结果,保留所有其他信息,包括确定子项目原始位置所必需的信息.例如,表示列表的单孔上下文的一种方法是使用两个列表:一个用于在提取的一个之前的项目,一个用于之后的项目.
通过区分识别该操作的动机来自以下观察.我们写的da/dx是指具有类型孔的类型的单孔上下文a的类型x.
d1/dx = 0
dx/dx = 1
d(a + b)/dx = da/dx + db/dx
d(a × b)/dx = a × db/dx + b × da/dx
d(g(f(x))/dx = d(g(y))/dy[f(x)/a] × df(x)/dx
在这里,1和0表示类型正好与一个和正好为零居民,分别与+和×代表总和和产品类型如常.f并且g用于表示类型函数或类型表达式,并且[f(x)/a]表示替换前面表达式中的f(x)每个的操作a.
这可以用无点样式编写,写成f'类型函数的派生函数f,因此:
(x ? 1)' = x ? 0
(x ? x)' = x ? 1
(f + g)' = f' + g'
(f × g)' = f × g' + g × f'
(g ? f)' = (g' ? f) × f'
这可能是优选的.
如果我们使用类型和仿函数的同构类来定义导数,那么可以使等式变得严格和精确.
现在,我们特别注意到微积分中有关加法,乘法和组合的代数运算的规则(通常称为求和,产品和链条规则)完全由"打洞"的操作反映出来.此外,在一个恒定表达式或术语x本身中"制作孔"的基本情况也表现为分化,因此通过归纳,我们得到所有代数类型表达式的类似分化的行为.
现在我们可以解释分化,n类型表达式的'衍生' d?e/dx?是什么意思？它是表示类型n-place上下文:术语,当"填充"与n类型方面x产生一种e.还有一个关键的观察与' (1/n!)'后来出现有关.
我们已经0在类型世界中得到了解释:没有成员的空类型.从组合的角度来看,将类型函数应用于它是什么意思？更具体地说,假设f是一个类型函数,f(0)看起来是什么样的？好吧,我们当然无法访问任何类型的内容0,因此任何f(x)需要的构造x都不可用.剩下的是那些在他们缺席时可以访问的术语,我们可以将其称为该类型的"不变"或"常量"部分.
对于一个明确的例子,使用Maybe函数,它可以代数表示为x ? 1 + x.当我们应用它时0,我们得到1 + 0- 它就像1:唯一可能的值是None值.对于列表,类似地,我们只获得与空列表对应的术语.
当我们将它带回来并将类型解释f(0)为数字时,可以将其视为可以获得多少个类型(任何)的计数而无需访问:即"空类"条款的数量.f(x)xx
我担心我不能想到一种适当的直接解释(1/n!).
如果我们考虑到,虽然类型f???(0)在上面的光,我们看到,它可以被解释为类型n-place上下文的类型的术语f(x),其并不包含一个 x -那就是,当我们"整合"他们n倍,由此产生的术语恰好是 n x s,不多也不少.然后将类型解释f???(0)为数字(如在Maclaurin系列的系数中f)仅仅是对有多少这样的空位置n上下文的计数.我们快到了!
但(1/n!)到底哪里结束了？检查"区分"类型的过程向我们表明,当多次应用时,它会保留提取子项的"顺序".例如,考虑(x?, x?)类型的术语x × x和两次"打洞"的操作.我们得到两个序列
(x?, x?) ? (_?, x?) ? (_?, _?)
(x?, x?) ? (x?, _?) ? (_?, _?)
(where _ represents a 'hole')
即使两者都来自同一个词,因为有两种2! = 2方法可以从两个元素中取出两个元素,保留顺序.一般来说,有一些n!方法可以从中获取n元素n.因此,为了计算具有n元素的仿函数类型的配置数量,我们必须计算类型f???(0)并除以n!,与Maclaurin系列的系数完全相同.
因此,除以n!结果本身就是可解释的.
首先,一些观察:
由于我们有链规则,如果我们将类型导数形式化为同构类,我们可以使用隐式区分.但隐式分化不需要任何外来机动,如减法或除法!所以我们可以用它来分析递归类型定义.以列表为例,我们有
L(X) ? 1 + X × L(X)
L'(X) = X × L'(X) + L(X)
然后我们可以评估
L'(0) = L(0) = 1
获得X¹Maclaurin系列的系数.
但由于我们确信这些表达式确实是严格"可区分的",如果只是隐含的,并且由于我们与函数ℝ→ℝ具有对应关系,其中衍生物当然是唯一的,我们可以放心,即使我们使用'获得值'非法'操作,结果有效.
现在,类似地,使用第二个观察,由于函数ℝ→correspondence的对应关系(它是同态吗？),我们知道,如果我们对函数有 Maclaurin系列感到满意,如果我们能找到任何系列总而言之,上述原则可以应用于使其严谨.
至于你关于函数组合的问题,我认为链规则提供了部分答案.
我不确定这适用于多少Haskell风格的ADT,但我怀疑它有很多,如果不是全部的话.我发现了这个事实的一个真正奇妙的证据,但这个边际太小而无法包含它......
现在,当然这只是解决这里发生的事情的一种方法,可能还有很多其他方法.
0我们提供该仿函数的"空洞"术语.我对这个问题的第一个答案是概念高而细节低，并反映在子问题“发生了什么？”；这个答案将是相同的，但侧重于子问题“我们能否获得任意类型的函数？”。
sum和product的代数运算的一个扩展是所谓的“大算子”，它表示通常分别写入?并?分别表示的序列的sum和积（或更一般地，一个域上的函数的sum和积）。请参阅Sigma符号。
所以总和
a? + a?X + a?X² + ...
可能会写
?[i ? ?]a?X?
例如，哪里a是实数序列。该产品将类似地以?代替?。
当从远处看时，这种表达看起来很像;中的“任意”函数X。当然，我们仅限于可表达的级数及其关联的分析功能。这是类型理论表述的候选人吗？绝对！
具有这些表达式的直接表示形式的类型理论的类别是“从属”类型理论的类别：具有从属类型的理论。自然地，我们有术语依赖于术语，并且在Haskell之类的语言中具有类型函数和类型量化，术语和类型取决于类型。在从属设置中，我们还根据术语具有类型。Haskell不是依赖类型的语言，尽管可以通过稍微折磨该语言来模拟依赖类型的许多功能。
“柯里-霍华德同构”的诞生是因为观察到简单类型的λ演算的术语和类型判断规则与应用于直觉命题逻辑的自然推论（由Gentzen提出）完全相对应，其中类型代替了命题，而术语代替了证明，尽管两者是独立发明/发现的。从那时起，它一直是类型理论家的巨大灵感来源。要考虑的最明显的事情之一是，命题逻辑的这种对应关系是否以及如何扩展到谓词逻辑或高阶逻辑。从属类型理论最初是从这种探索途径产生的。
有关简单类型的lambda演算的Curry-Howard同构的介绍，请参见此处。例如，如果我们想证明，A ? B就必须证明A和证明B；组合证明只是一对证明：每个合取项一个。
自然推论：
? ? A ? ? B
? ? A ? B
在简单类型的lambda演算中：
? ? a : A ? ? b : B
? ? (a, b) : A × B
对于?和和类型，?函数类型以及各种消除规则也存在类似的对应关系。
不可证明的（直觉上是错误的）命题对应于一个无人居住的类型。
考虑到类型的比喻是逻辑命题，我们可以开始考虑如何在类型世界中对谓词建模。有许多方法在此已正式（见本介绍马丁- LOF的直觉类型论为一种广泛使用的标准），但抽象的方法通常观察到的谓词就像是一个命题，免费长期变量，或者，一种对命题使用术语的功能。如果我们允许类型表达式包含项，那么使用lambda演算样式进行处理就立即成为一种可能！
仅考虑构造性证明，什么构成证明?x ? X.P(x)？我们可以将其视为证明函数，将术语（x）用作其相应命题（P(x)）的证明。因此，类型（命题）的成员（样张）?x : X.P(x)是“相关的功能”，其每个x在X给类型的术语P(x)。
那?x ? X.P(x)呢 我们需要的任何成员X，x与的证明一起P(x)。因此，类型（命题）的成员（样张）?x : X.P(x)是“依赖对”：一个杰出的术语x中X，与类型的术语一起P(x)。
表示法：我将使用
?x ? X...
有关该类成员的实际陈述X，以及
?x : X...
用于类型表达式，对应于类型的通用量化X。同样适用于?。
除了类型与命题的库里-霍华德对应之外，我们还有代数类型与数字和函数的组合对应，这是这个问题的重点。幸运的是，这可以扩展到上面概述的依赖类型！
我将使用模数表示法
|A|
表示类型的“大小” A，以明确指出问题中概述的类型和数字之间的对应关系。注意，这是理论之外的概念。我不认为该语言中需要任何此类运算符。
让我们计算类型的可能（完全减少的，规范的）成员
?x : X.P(x)
这是考虑方面相关的功能的类型x类型的X到类型方面P(x)。每个此类函数必须具有的每个项的X输出，并且此输出必须具有特定的类型。那么，对于xin中的每个X，这都会提供|P(x)|“选择”输出。
重点是
|?x : X.P(x)| = ?[x : X]|P(x)|
如果Xis IO ()，那当然没有什么意义，但适用于代数类型。
类似地，类型术语
?x : X.P(x)
是对类型(x, p)与p : P(x)，所以给出的任何x中X我们可以构造适当的一对带中的任何成员P(x)，给人|P(x)|“选择”。
因此，
|?x : X.P(x)| = ?[x : X]|P(x)|
同样的警告。
这证明了使用符号?和表示理论中从属类型的通用符号是正确的?，并且由于上述对应关系，实际上许多理论模糊了“所有人”和“产品”之间以及“有”和“和”之间的区别。
我们越来越近了！
我们现在可以编码数字表达式吗
?[n ? ?]X?
作为类型表达式？
不完全的。尽管我们可以像X?Haskell 那样非正式地考虑表达式的含义，在哪里X是类型和n自然数，但这是对符号的滥用。这是一个包含数字的类型表达式：显然不是有效的表达式。
另一方面，对于图片中的从属类型，包含数字的类型恰好是关键。实际上，从属元组或“向量”是一个非常常见的例子，说明了从属类型如何为诸如列表访问之类的操作提供实用的类型级安全性。向量只是一个列表，以及有关其长度的类型级别信息：正是我们对诸如此类的类型表达式所追求的X?。
在此答案的持续时间内，让
Vec X n
是-type值的长度n向量的X类型。
从技术上讲，n此处是自然数在系统中的表示，而不是实际的自然数。我们可以代表自然数（Nat在皮亚诺风格）的要么是零（0）或者继承人（S另一个自然数），并为n ? ?我写?n?的意思在长期Nat代表n。例如，?3?是S (S (S 0))。
那我们有
|Vec X ?n?| = |X|?
对于任何n ? ?。
现在我们可以编码像
?[n ? ?]X?
作为类型。这个特定的表达式将产生一个类型，该类型X与问题中所标识的列表类型同构。（不仅如此，而且从类别理论的角度来看，类型函数（它是一个函子），采用X上述类型对于List函子来说自然是同构的。）
“任意”函数的最后一个难题是如何编码，
f : ? ? ?
像这样的表达
?[n ? ?]f(n)X?
这样我们就可以将任意系数应用于幂级数。
我们已经了解了代数类型与数字的对应关系，从而使我们能够将类型映射为数字，并将类型函数映射为数值函数。我们也可以走另一条路！-取一个自然数，显然存在一个可定义的代数类型，其中有许多项成员，无论我们是否具有从属类型。通过归纳，我们可以轻松地在类型理论之外证明这一点。我们需要的是一种在系统内部将自然数映射为类型的方法。
一个令人愉悦的认识是，一旦有了依赖类型，归纳证明和递归构造就变得极为相似-实际上，它们在许多理论中都是同一回事。既然我们可以通过归纳证明存在满足我们需求的类型，那么我们是否应该不能构造它们呢？
有几种方法可以在术语级别表示类型。在这里，我将使用虚构的Haskellish表示法来表示*类型的宇宙，通常将其本身视为从属环境中的类型。1个
同样，?注释“- 消除”的方法至少也与依赖类型理论一样多。我将使用Haskellish模式匹配表示法。
我们需要与属性映射，?从Nat到*
?n ? ?.|? ?n?| = n.
以下伪定义就足够了。
data Zero -- empty type
data Successor a = Z | Suc a -- Successor ? Maybe
? : Nat -> *
? 0 = Zero
? (S n) = Successor (? n)
因此，我们看到?镜像的作用反映了后继者的行为S，使其成为同态。Successor是一个类型函数，将一个类型的成员数量“加一”；也就是说，|Successor a| = 1 + |a|对于任何a具有定义大小的对象。
例如? ?4?（是? (S (S (S (S 0))))），是
Successor (Successor (Successor (Successor Zero)))
和这种类型的条款是
Z
Suc Z
Suc (Suc Z)
Suc (Suc (Suc Z))
给了我们四个要素：|? ?4?| = 4。
同样，对于任何n ? ?，我们有
|? ?n?| = n
按要求。
*仅仅是类型的代表，并且提供操作作为从类型术语*到其关联类型的显式映射。其他理论允许文字类型本身是术语级实体。现在，我们有一种设备可以将一种完全通用的幂级数表达为一种类型！
该系列
?[n ? ?]f(n)X?
成为类型
?n : Nat.? (?f? n) × (Vec X n)
?f? : Nat ? Nat函数语言中合适的表示在哪里f。我们可以看到如下。
|?n : Nat.? (?f? n) × (Vec X n)|
= ?[n : Nat]|? (?f? n) × (Vec X n)| (property of ? types)
= ?[n ? ?]|? (?f? ?n?) × (Vec X ?n?)| (switching Nat for ?)
= ?[n ? ?]|? ?f(n)? × (Vec X ?n?)| (applying ?f? to ?n?)
= ?[n ? ?]|? ?f(n)?||Vec X ?n?| (splitting product)
= ?[n ? ?]f(n)|X|? (properties of ? and Vec)
这到底有多“随意”？通过这种方法，我们不仅限于整数系数，而且还限于自然数。除此之外，f在具有依赖类型的图灵完成语言的情况下，可以是任何东西，我们可以用自然数系数表示任何解析函数。
我还没有研究这种情况与例如问题中提供的情况的相互作用，List X ? 1/(1 - X)或者在这种情况下这种否定和非整数“类型”可能具有什么意义。
希望这个答案对探索任意类型的函数可以走多远有所帮助。