We introduce Ideograph, a language for expressing and manipulating structured data. Its types describe kinds of structures, such as natural numbers, lists, multisets, binary trees, syntax trees with variable binding, directed multigraphs, and relational databases. Fully normalized terms of a type correspond exactly to members of the structure, analogous to a Church-encoding. Moreover, definable operations over these structures are guaranteed to respect the structures' equivalences. In this paper, we give the syntax and semantics of the non-polymorphic subset of Ideograph, and we demonstrate how it can represent and manipulate several interesting structures.
翻译:我们介绍了 Ideograph,一种用于表达和操作结构化数据的语言。它的类型描述了种类的结构,例如自然数、列表、多重集合、二叉树、具有变量绑定的语法树、有向多重图和关系数据库。一种类型的完全规范术语恰好对应于结构的成员,类似于 Church 编码。此外,针对这些结构的定义操作被保证遵守结构的等价性。在本文中,我们给出 Ideograph 的非多态子集的语法和语义,并展示它如何表示和操作若干有趣的结构。