CTFP Ch06

概要

第五章讲的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)"

随笔