内存敏感的语言，如C++和Rust，使用编译时信息来计算数据类型的大小。这些大小用于以提高运行时性能的方式通知对齐、分配和调用约定。此设置中的现代语言支持泛型类型，但到目前为止，这些语言只允许对类型进行参数化，而不允许对类型构造函数进行参数化。在本文中，我将描述如何在任意类型构造上启用参数化，同时仍然保留数据类型大小的编译时计算。
许多类型化语言支持某种形式的泛型(参数化)数据类型。这种抽象类型的能力称为“参数多态性”(简称多态性)。例如，在Rust中，可以将多态对类型定义为结构对<；A，B&>(fst：A，snd：B)。在此定义中，A和B是类型变量(或类型参数)，可以替代其他类型：Pair<；bool、bool&>、Pair<；bool、char&>和Pair<；string、int32&>；都是有效的对。
不带任何参数的类型名称称为类型构造函数。Pair不是单独的类型；Pair<；A，B>；(对于某些类型A和B)是。“完成”一个类型构造函数所需的类型数量是已知的(因此Pair的数量为2)。必须始终考虑类型构造函数的多样性；提供比预期更多或更少的类型参数都是错误的。例如，对<；bool>；和对<；char，int32，string>；无效。
当使用C++或Rust时，编译器将计算每种数据类型需要多少字节内存。像int32和bool这样的简单类型具有恒定的大小；分别为4字节和1字节。使用其他简单类型构建的数据类型的大小很容易计算。计算结构大小的最简单方法是将字段的大小相加，而计算枚举(或标记的联合)大小的最简单方法是找到最大的变量，然后加1(表示标记字节)。这很少是生产编译器使用的确切公式，因为它们考虑了对齐。本文将假定使用简单的大小调整公式，因为结果可以很容易地适应更细微的公式。
像struct TwoInts(x：int32，y：int32)这样的数据类型的大小在其定义时是立即知道的。TwoInts需要8字节的内存。另一方面，泛型数据类型的大小在其定义上并不总是已知的。结构对<；A，B>；(fst：A，snd：B)的大小是多少？它是A的大小加上B的大小，对于一些未知的A和B。
这一困难通常是通过仅在所有泛型类型都已被具体类型替换时才为数据类型和函数生成代码来解决的。这个过程被称为单形化。如果程序包含一对(true，true)，那么编译器将生成一个新类型的struct PairBoolBool(fst：bool，snd：bool)，其大小是静态已知的。如果将Pair(true，true)传递给函数FN SWAP<；A，B>；(p：Pair<；A，B>；)->；Pair<；B，A>；，则编译器会生成新函数FN swapBoolBool(p：PairBoolBool)->；PairBoolBool。因为这个新函数只使用已知大小的类型，所以可以正确生成内存分配和调用约定的代码。
还有一些泛型类型不依赖于其参数的大小。这方面的一个例子是指针，在Rust中通常称为Box<；A>；。无论指针指向什么，它都具有相同的大小(通常为4或8字节，取决于您的CPU)。但是为了分配新指针，必须知道项的大小。
对于每个泛型数据类型或函数，编译器跟踪哪些类型变量对于大小计算很重要。这方面的细节将在类型类一节中讨论。
所有这一切的结果是，在这些语言中，类型变量只能代表类型。但是，也有充分的理由使用代表类型构造函数的类型变量：
struct one<；A>；(A)Implt<；A>；one<；A>；{map<；B，F：fn(A)->；B>；(Self，f：F)->；one<；B>；{.}struct Two<；A>；(A，A)Impl<；A>；Two<；{map<；B，F：fn(A)->；B>；(self，f：F)->；Two<；B>；{.}}结构3<；A>；(A，A，A)实施3<；A>；3<；A>；{map<；B，F：fn(A)->；B>；(SELF，f：F)->；Three<；B>；{.}}。
以下是一些1-arity容器类型。这些数据类型之间唯一的区别是它们包含的元素数量不同。它们都支持映射操作，该操作将函数应用于所有数据类型的元素。使用MAP的函数需要为每种类型实现一次，即使它们的实现是相同的：
fn incrOne(x：one<；int32>；)->；one<；int32>；{x.map(|n|n+1)}fn incrTwo(x：Two<；int32>；)->；Two<；int32>；{x.map(|n|n+1)}fn incrThree(x：3<；int32>；{x.map(|n|n+1)}。
要解决这个问题，首先必须有一种在类型构造函数上进行抽象的方法，以便可以一劳永逸地编写代码：
fn增量；F&>；(x：F<；int32>；)->；F<；int32>；{x.map(|n|n+1)}//当F<；A&>；有MAP时，适用于所有类型A。
那么，一定有某种方法可以排除无效类型。例如，在F<；int32>；中用bool替换F是无效的，因为bool<；int32>；不是类型。这是第一类的工作。
类型描述类型(和类型构造函数)的“形状”的方式与类型描述值的“形状”的方式相同。类型的种类决定它是否接受任何参数。以下是种类的语法：
不带参数的类型(如bool、char和string)具有KIND类型。接受一个参数的类型(如一个参数)具有种类类型->；类型。在上面的incr代码中，F隐式具有KIND Type->；Type。接受多个参数的类型以咖喱形式表示。这意味着两个人有种类类型-&>类型-&>类型，而不是(类型，类型)-&>类型。三种有KIND类型-->；类型，以此类推。
咖喱类型的构造函数在此设置中是标准的，但不是必需的。本文中的结果也可以应用于具有不确定类型构造函数的设置，但代价是表达式或实现复杂性。
种类将类型和类型构造函数放在同等的位置。对于本文的其余部分，这两个概念都将被称为类型。种类就成了与众不同的特征。例如，“类型构造函数2”将替换为“类型类型->；类型->；类型”。
最后还有一些行话：类型不同于类型的类型称为“高级类型”，参数依赖于高级类型称为“高级多态”。
铁锈使用性状来协调大小计算。每个数据类型隐式接收一个大小特征的实现，并且每个与大小计算相关的类型变量都被赋予一个大小界限。这意味着性状分辨率这一已经很有用的特性可以被重用来执行尺寸计算。
与特征密切相关的是类型Class 1的函数编程概念。两者之间存在差异，但这些差异不会影响本文的结果。类型类将被证明是讨论这些想法的更方便的语言。
类型类(或特征)可以被视为类型的谓词。类型类约束(或特征界限)是谓词必须为真的断言。对于满足的每个约束，都有相应的“证据”证明谓词为真。
当类型T具有大小约束时，将断言“T具有已知大小”语句为真。为简明起见，这将写为大小为T。当满足此语句时(例如，当T为int32时)，生成的证据是T的实际大小(当大小为int32时，证据是数字4-int32的大小)。
像Two<；A>；这样的泛型类型的大小取决于它们的类型参数。就约束条件而言，可以说A号意味着2号A>；。如果A是int32，那么它的大小是4，这意味着两个int32>；的大小是4+4=8。类似地，可以说大小A意味着[大小B意味着大小对A，B>；]。可以在咖喱版本和非咖喱版本之间进行选择；也可以说[SIZED A和SIZE B]意味着<；A，B&>；，但为了方便起见，将使用咖喱版本。
请注意，类型构造函数没有大小。换句话说，只有Kind Type的类型才有大小。一个类型构造函数，如Two(种类类型->；Type)，具有SIZE函数。给定类型构造函数参数的大小，Size函数计算结果数据类型的大小。二的大小函数是\a->；a+a。对的大小函数是\a->；b->；a+b(在不加标记的情况下也可以是\(a，b)->；a+b)。
当Kind Type的类型与尺寸计算相关时，将为其提供尺寸约束，该约束将以具体尺寸作为证据来满足。对于对大小计算有贡献的高级类型，约束和证据的等价概念是什么？
引入量化类约束可以很好地解决这个问题2.量化约束是对类型类的扩展，它为约束语言和相应的证据概念增加了隐含和量化。
约束：：=大小类型(大小约束)约束=>；所有A的约束(隐含约束)约束(量化约束)。
约束c1=>；c2的证据是用于获取c1的证据并产生用于c2的证据的函数，而用于所有Ac的证据仅是用于c的证据。量化约束的证据通常稍有细微差别，但是当仅考虑大小约束时，这种描述是准确的。
具体地说，这意味着现在可以使用约束来表示更高类型的大小规则，并且可以使用类型类解析来执行涉及更高类型的大小计算。现在的情况是，对于所有A，大小A=大小为2；A&>A；，且该约束的证据是函数\a->a+A。对于所有A，对于所有B，大小A=；大小B=大小的对，具有证据函数\a，b->a+b，对A，B&>；是相关的约束条件，对于所有的A，大小为A=；大小为2的对，且此约束的证据是函数\a->a+a。对于所有的B，大小A=大小的对，A，B&>；具有证据函数\a，b->a+b。
这可以扩展到任何类型。对于所有类型，都有一种仅基于类型的种类导出适当大小约束的机械方法；种类类型的T导致大小T，种类类型的U-gt；类型导致所有A大小的A=>；大小的T<；A>；，依此类推。在数据类型和函数中，任何与大小相关的类型变量都可以通过这种方式分配一个大小约束，编译器在单形化定义时将使用此额外信息。
Size-HKTS是实现这些思想的最小编译器。它支持更高级的多态性、函数和代数数据类型，并编译成C语言。可以推断出种类和大小约束，不需要用户进行注释。
下面是一些示例代码，它说明了更高级的数据模式(源代码，生成的C代码)：
枚举ListF f a{Nil()，Cons(f a，Ptr(ListF F A))}枚举可能是{Nothing()，Just(A)}struct Identity a=Identity(A)FN Validation<；a>；(xs：ListF可能a)->；可能(ListF Identity A){Match Xs{Nil()=>；Just(Nil())，Cons(MX，REST)=&。匹配验证(*rest){Nothing()=>；Nothing()，Just(NextRest)=>；Just(CONS(Identity(X)，new[nextRest]))}fn main()->；int32{let a=Nil()；b=CONS(Nothing()，new[a])；c=CONS(Just(1)，new[b])在匹配验证(C){Nothing()=>；22，CONS(x，rest)=>；x.0}。
这段代码定义了一个链表，该链表的元素包装在一个泛型“容器”类型中。它定义了两种可能的容器类型：可能是可能为空的容器，以及标识是单元素容器。VALIDATE接受一个列表，该列表的元素可能包含在其中，并尝试用Identity替换所有的JUST，如果列表中的任何元素为Nothing，则整个函数不返回任何内容。
生成5种类型，对应于：ListF可能为int32、ListF标识为int32、可能为int32、标识为int32、可能(ListF标识为int32)。
只生成1个版本的验证，因为它只在的一个实例化中使用。
生成的代码没有使用sizeof；数据类型大小是在类型检查之后知道的，并且在代码生成期间内联。编译器知道ListF可能int32只有14字节宽(1+max(1，1+4)+8)，而ListF标识int32有13字节宽(max(1，1+4)+8)。
数据类型大小不一定与sizeof一致，因为为了简单起见，它们忽略了对齐。此时，在大小计算中考虑对齐很简单。
量化的类约束为静态大小更高类型的类型提供了一个优雅的框架。这本身可以提高高性能语言的抽象上限，但也可以作为函数式、应用式和可遍历等函数式编程抽象的“零成本”版本的基础。
这项工作表明，Rust以合理的方式支持更高级的类型是完全可能的，但是在实践中这可能不是一个好主意，有一些理论上较少的原因。添加“量化的特征界限”将需要新的语法，这代表了用户需要学习的另一个概念。将一种类型的系统添加到Rust中也将是一个有争议的改变；选择保持类型不混乱将对该系统的潜在用户不利，而更改为不受限制的类型将需要重新考虑语法和教育材料，以保持Rust的用户体验的高标准。
琼斯，M.P.(1995)。构造函数类系统：重载和隐式高阶多态性。函数式编程学报，5(1)，1-35。↩和↩2。
Bottu，G.J.，Karachalias，G.，Schrijvers，T.，Oliveira，B.C.D.S.，&；Wadler，P.(2017)。量化类约束。ACMSIGPLAN通知，52(10)，148-161.(↩)