Skip to content

Latest commit

 

History

History
137 lines (98 loc) · 5.29 KB

092916.md

File metadata and controls

137 lines (98 loc) · 5.29 KB
Raw

September 29, 2016

Speaker: Yao Li

See accompanying Coq development: systemt_finite.ott Ch11.v

Notes about sum types

First, note that sums are not as common as they should be. In particular, Java, C#, etc. don't have them, to their detriment.

Why sums?

  • Booleans: Can use sums to implement booleans. Boolean is a type with two values, true and false. Plus, we have if expressions to have a condition on booleans.

  • Option types: A type with two sort of values, null (none) and just (some). Can use options for partial operations that may not return a value. Searching a list may return nothing. We can test option types with a conditional that checks whether there is a value or not. In the case of just, the condition binds a variable to refer to the value carried by the option.

  • Sum types are the most general form of these types.

Plan for today

  1. Definitions of sums
  2. Proofs of type safety with sums
  3. Applications of sums

Definitions

 type t ::= ... | void         contains no values
                 | t1 + t2      sum types

 exp  e ::= ... | abort{t} e   elimination form for void
                 | inl{t} e     introduction form for sum types
					  | inr{t} e     introduction form for sum types
					  | case e of { inl x -> e1 ; inr x -> e2 }

Note: abort must be annotated with the type t so that type checking is syntax-directed.

ALso, inl & inr needs to be annotated with the other side of the sum type that is being introduced.

For example, what is the type of inl z ? It is nat + ?? but the ?? could be anything.

Discussions:

  • What is the point of void in a programming language? Where would you run across it?
  • Do the two branches of a case have to have the same type?
  • Can we get rid of the evaluation rule for abort? Can we just get rid of the premise of the abort evaluation rule?

Note: you can try modifying the rules and reproving the theorems in Ch11.v.

Questions

  • In Exercise 11.2, the author says, 'The essence of Hoare's mistake is the misidentification of the type τ opt with the type bool × τ. ... The idea is that the flag indicates whether the associated value is 'present'.' I understand that this presents a problem. But if the value is always 'present' irrespective of what the flag indicates and is used only when the the flag is true, would there still be some problem? More generally, can τ₁ + τ₂ be replaced by 𝔹 × τ₁ × τ₂ and the corresponding definitions appropriately modified and can this be done for any finite sum with a suitable replacement for 𝔹?

    [SCW: If the value is always present then there is no problem, and the bool is unnecessary. You are also right that any sum "t1 + t2" can be replaced by "bool * t1 * t2", or if you have dependent types and want to save space "Sigma b:Bool, if b then t1 else t2"]

  • For the nullify sum, the typing rule says that when e is void type, then abort(e) will be of type tau. Does it mean that we could define any type to abort(e) expression?

    [SCW: Yes, abort can have any type, because it is guaranteed to never finish. We will never get to a value as the argument of the abort expression --- that argument will always diverge or be otherwise inaccessible.]

    Also for the case rule, the book says that two branches should return expressions with the same type. It is only for the language which is type safe? And it would be great if the proof of safety can be proved during the class.

    [SCW: Yes, having both branches return the same type is an approximation that statically typed languages make to ensure that code can be type checked. There are non-crashy programs that have differently-typed case expressions, but the general problem of showing crash-freedom is difficult when the case branches aren't required to line up.]

    [LY: You can find the type safety proof in Ch11.v.]

  • I see the resemblance with how we implemented Bool, and Maybe, and finite enumerations. Say we wanted to make a list type. Would adding product types be enough to get our ADTs? Or do we need some sort of recursive type?

    Does this work?

          Exp e := node
               Cons (e1,e2)

      t list = t + (t, t list)
              node = l . e
              cons(e1, e2) = r (e1, e2)

    [SCW: you do need a recursive type to have recursive ADTs]

    [LY: you can find more details in the last section of Ch11.v. If we model list in the above form, we will get a type with recursive structure.]

  • I can see the coherence between product types and structs in C. Is there such coherence between sum types and C unions? If yes, since we can simulate unions with structs in C, can we also simulate sum types with product types?

    [SCW: almost. C's unions are not type safe because they don't force "tags" i.e. runtime evidence that tells you what case of the union they represent. We can simulate sums with products: see above.]

  • From chapter 10, we saw that product types allowed us to express mutual recursion, are there such computational benefits that we can gain from adding sum types to our language? One benefit I can think of is being able to turn some partial functions into total functions. Is there something else?

    [SCW: Good question. I don't know a good answer to this.]