CTFP Ch06 - WinChua/blog GitHub Wiki

概要

第五章讲的product以及coproduct是组合基础类型的两种最基本的方式. 而事实上许多在编程中常常被使用的数据结构都可以用这种组合的方式产生. 不仅数据结构能够通过组合产生, 复合数据结构的属性也能够通过组合基本数据结构的属性产生.

摘录

  • pairs are not strictly commutative, a pair (Int, Bool) cannot be substituted for a pair (Bool, Int), but they are isomorphic up to swap: $$ swap :: (a, b) \to (b, a) \\ swap (x, y) = ( y, x ) $$

  • the creation of a product type is a binary operation on types.

  • associative up to isomorphism: (a, (b, c) == ((a, b), c)

  • Set(the category of set) is a monoidial category.

    • It's a category but also a monoid where the set is the set in category
    • binary operator is product
    • neutral element: ()

  • product in the category of sets gives rise to product types, the coproduct gives rise to sum types.

  • **Set is also a monoidial cateogyr with respect to coproduct ** :

    • the set is the set of category
    • binary operatory is |
    • neutral element: initial object Void

  • Algebra of Types

    • product and sum types can be used to define a variety of usefule data structures, but the real strngth comes from combining the two.

    • So far, we have two commutative monoidal structures:

      • sum type with Void as the neutral element ==> addition with 0
      • product type with () as the neutral element ==> multiplication with 1

    • some question:

      • does multiply zero with zero? ==> is a product type with one component being Void isomorphic to Void?
      To create a pair you need two values. Say you would
like to create a pair of (Int, Void). You can get a
value of Int easily, but as for Void is uninhabitable.
You cann't pick a value from Void, so you can't construct
a pair of (Int, Void). so
                       a * 0 = 0

    • the distributive property: $$ a \times ( b + c ) = a \times b + a \times c $$ Does it hold for product and sum types? ==> Does $(a, Either\ b\ c)$ isomorphic to $(a\ Either\ b, a\ Either\ c)$

    • rig or semiring is the name for such interwined monoids. It's not a full ring, because we can't define subtraction of types. And the name "rig" is for "ring without an n(negative)"

    • data List a = Nil | Cons a List a $$ x = 1 + a * x \\ x = 1 + a * (1 + a * x) = 1 + a + a * a * x $$ which is a infinite sum of the product of a

    • logic and and or also form a rig. the mapping between logic and type is showed below.

随笔

第六章的内容也不多, 主要在讲的内容是, Set这个category可以有两种方式被认为是monoid:

  • Set中的每一个set作为操作数, product作为二元操作符, ()作为单位元
  • Set中的每一个set作为操作数, sum作为二元操作符, Void 作为单位元 上面的每一个二元操作符都是以类型(set)作为操作数, 产生一个新的类型, 也就是说新的类型可以通过product以及sum操作的组合产生. 可以使用类型变量来演算这种操作的过程, 因此称为抽象代数类型;

product以及sum这两种交互在一起的monoid的结构被称为半环, 没有negative的环