Proving Algebraic Datatypes are “Algebraic”

栏目: IT技术 · 发布时间: 4年前

Several programming languages allow programmers to define (potentially recursive) custom types, by composing together existing ones. For instance, in OCaml, one can define lists as follows:
type 'a list =
| Cons of 'a * 'a list
| Nil
This translates in Haskell as
data List a =
  Cons a (List a)
| Nil
In Rust:
enum List<A> {
  Cons(A, Box< List<a> >),
  Nil,
}
In Coq:
Inductive list a :=
| cons : a -> list a -> list a
| nil
And so forth.Each language will have its own specific constructions, and the type systems of OCaml, Haskell, Rust and Coq —to only cite them— are far from being equivalent. That being said, they often share a common “base formalism,” usually (and sometimes abusively) referred to as algebraic datatypes . This expression is used because under the hood any datatype can be encoded as a composition of types using two operators: sum ( + ) and product ( * ) for types.
  • a + b is the disjoint union of types a and b . Any term of a can be injected into a + b , and the same goes for b . Conversely, a term of a + b can be projected into either a or b .
  • a * b is the Cartesian product of types a and b . Any term of a * b is made of one term of a and one term of b (remember tuples?).
For an algebraic datatype, one constructor allows for defining “named tuples”, that is ad-hoc product types. Besides, constructors are mutually exclusive: you cannot define the same term using two different constructors. Therefore, a datatype with several constructors is reminescent of a disjoint union. Coming back to the list type, under the syntactic sugar of algebraic datatypes, the list α type is equivalent to unit + α * list α , where unit models the nil case, and α * list α models the cons case.The set of types which can be defined in a language together with + and * form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of + and * have to satisfy properties such as commutativity or the existence of neutral elements. In this article, we will prove some of them in Coq. More precisely,
  • + is commutative, that is ( x , y ) ,   x + y = y + x \forall (x, y),\ x + y = y + x
  • + is associative, that is ( x , y , z ) ,   ( x + y ) + z = x + ( y + z ) \forall (x, y, z),\ (x + y) + z = x + (y + z)
  • + has a neutral element, that is e s ,   x ,   x + e s = x \exists e_s, \ \forall x,\ x + e_s = x
  • * is commutative, that is ( x , y ) ,   x y = y x \forall (x, y),\ x * y = y * x
  • * is associative, that is ( x , y , z ) ,   ( x y ) z = x ( y z ) \forall (x, y, z),\ (x * y) * z = x * (y * z)
  • * has a neutral element, that is e p ,   x ,   x e p = x \exists e_p, \ \forall x,\ x * e_p = x
  • The distributivity of + and * , that is ( x , y , z ) ,   x ( y + z ) = x y + x z \forall (x, y, z),\ x * (y + z) = x * y + x * z
  • * has an absorbing element, that is e a ,   x ,   x e a = e a \exists e_a, \ \forall x, \ x * e_a = e_a
For the record, the sum and prod types are defined in Coq as follows:
Inductive sum (A B : Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B

Inductive prod (A B : Type) : Type :=
| pair : A -> B -> prod A B
  1. An Equivalence for Type
    1. Introducing type_equiv
    2. type_equiv is an Equivalence
      1. list ’s Canonical Form
      2. nat is a Special-Purpose list
  2. prod has an Absorbing Element
  3. prod and sum Distributivity
  4. Bonus: Algebraic Datatypes and Metaprogramming
Revisions

This revisions table has been automatically generated from the git history of this website repository , and the change descriptions may not always be as useful as they should.

You can consult the source of this file in its current version here .

2020-07-12 More spellchecking and typos 48a9b49
2020-07-12 Invert the table of contents and the revision tables 0a750a2
2020-07-12 Spellchecking cec5638
2020-07-12 New article on Algebraic Datatypes 41007fc

以上就是本文的全部内容,希望对大家的学习有所帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

构建高性能Web站点

构建高性能Web站点

郭欣 / 电子工业出版社 / 2012-6 / 75.00元

《构建高性能Web站点(修订版)》是畅销修订版,围绕如何构建高性能Web站点,从多个方面、多个角度进行了全面的阐述,几乎涵盖了Web站点性能优化的所有内容,包括数据的网络传输、服务器并发处理能力、动态网页缓存、动态网页静态化、应用层数据缓存、分布式缓存、Web服务器缓存、反向代理缓存、脚本解释速度、页面组件分离、浏览器本地缓存、浏览器并发请求、文件的分发、数据库I/O优化、数据库访问、数据库分布式......一起来看看 《构建高性能Web站点》 这本书的介绍吧!

CSS 压缩/解压工具
CSS 压缩/解压工具

在线压缩/解压 CSS 代码

RGB转16进制工具
RGB转16进制工具

RGB HEX 互转工具

XML 在线格式化
XML 在线格式化

在线 XML 格式化压缩工具