Skip to content

Latest commit

 

History

History
111 lines (82 loc) · 5.02 KB

101316.md

File metadata and controls

111 lines (82 loc) · 5.02 KB

Oct 13, 2016

Speaker: Leo

Notes

At a high level, generic programming is writing code that works with many different types of data. For example, Haskell's parametric polymorphism is an instance of generic programming.

But in this chapter, we are looking a non-parametric polymorphism.

Questions

  • I am confused about the restriction Bob Harper places on positive type operators having to do with negative occurrences. I know he talks about what goes wrong but I can't really follow his example. I was hoping you could go over this and how his proposed solution works?

  • We have generic extensions for positive type operators as given in 14.3. On similar lines, we can have generic extensions for non-negative type operators, statics given by inference rule (14.6a). The next inference rule reverses the roles of ρ and ρ' and gives the statics of generic extension for negative type operators. I think we can't have generic extensions for any type operator (positive or negative) in general. Am I right? If so, does this point to something interesting regarding function types?

    [SCW: if you have an operator that is both positive and negative, then there is a generic extension, but you need to have two functions to extend, one for the positive occurrences and one for the negative occurrences. (That is called a 'dimap' in Haskell.)]

    1. Could you give some examples on the application of generic programming, especially the generic extension?

    [SCW: Generic programming can be used to derive operations based on type structure in Haskell. These ideas are behind the "deriving" of type classes like Eq, Show, Functor (which is generic extension) etc. I've personally used generic programming to implement alpha-equivalence and substitution operations in the 'unbound' library.]

    1. Could we define the normal form of generic extension like the expression derived from the generic extension which is not polynomial type. In this case, could we define the progress property for it?

    [SCW: ??? Generic extension shouldn't have a normal form. It should always be able to make progress.]

    1. Could you give some examples on how positive type operators can be used in programming languages?

    [SCW: most data structures in Haskell are formed from positive type operators, such as tuples, lists, trees...

  • It seems to me that the polynomial type defined here does not allow multiple type operators (for example, t1.t2.t1+t2 or t1.t1+t2.t2). Why is there such a restriction?

    [SCW: the generic extension is only defined for one type operator. You can define it for multiple arguments in your type operator, but then the extension looks different. For example, we have map for lists, but bimap for tuples:

    map :: (a -> b) -> [a] -> [b] bimap :: (a -> b) -> (c -> d) -> (a,c) -> (b,d)

    There is a way to generalize these definitions, but Bob doesn't go into that in this Chapter (you need to know about kinds first).]

  • Why is polynomial type defined at t.unit and t.void, but not at t.nat? (the example on pg. 121 does use the nat data type) This also means that types like t.<nat*t> are not polynomial types, which makes the polynomial types defined here look quite restricted to me.

    [SCW: I think polynomial types should include nat.]

  • I’m not sure how to understand the generic extension intuitively. What is this feature called in programming language terms? [SCW: it is fmap in Haskell, and usually specialized to specific types, like list.]

  • Why is generic extension called map? [SCW: it generalizes list map --- (a -> b) -> list a -> list b

  • At the end of the chapter, the book made a note saying that generic extension is the same as functorial programming, and the connection was very clear from the way generic extension's dynamics and statics is presented. In haskell we also have a contravariant functor typeclass, whose map operator has type (b -> a) -> f a -> f b. Is there some connection between contravariant operators and potential features of a programming language?

    For example, if f is (-> n) (the arrow type whose second parameter is fixed, which allows us to put type parameters in the first type instead of the second as restricted by positive type operators), then contramap would have type (b -> a) -> (a -> n) -> (b -> n), which would have the definition

    contramap f g = g . f -- flip (.)?

    But I am not sure if this would be useful in anyway. Would you mind providing some insight?

    [SCW: Good question! I haven't needed this operator so much...]

  • The big question looming in my mind is: what about inductive types? It's easy to see how to use one of these type operators to apply operations at specified points in some polynomial non-recursive data type, but what does it look like to talk about mu? [SCW: See Tuesday's class]

    If we consider a language with such generic operations as the proof-term language of some logic, what corresponding logic do we (might we) get? [SCW: They are important part of current definitions of Cubical Type theory]