Speaker: Nicholas Topic: Inductive and Coinductive types
-
Given an inductive type, there would be an induction principle with which we can use to prove properties about values of this type. For coinductive types, the values are represented by the value's current state and "destructors" that pushes the state further and extracts some useful information. Do we have coinduction principles that let us prove properties of coinductive values? What would they look like? Is it about showing the property holds for all possible ways to destruct a coinductive value?
[SCW: yes, there is a principle of coinduction. However, in stead of using it to prove properties about natural numbers, you use it to generate relations between numbers. See: http://adam.chlipala.net/cpdt/html/Coinductive.html]
-
Since the evaluation of coinductive expressions never terminate, and different constructors might yield the same results, how do we define the equality between coinductive expressions?
[SCW: You can't write a function to determine whether two conats are equal. However, you can define a (coinductive) equivalence relation that captures what it means for two conats to be equal, and then prove that certain conats are in this relation.]
-
My question for tomorrow’s CIS 670 lecture is: What does coinduction mean in the logic side?
[SCW: coinduction is a principle of logical reasoning, just like induction.]
-
What would a termination proof look like for the language M? Bob says it's "beyond our current reach," but what's out of reach about it (other than, I don't know how I would start, off-hand)?
[SCW: take a look at the exercises for Ch9, which walk through a termination proof for System T. This will get you started...]
-
This is the first time I am seeing coinductive types, so the question is very basic. Inductive types are defined by specifying how one can form elements of that type. By looking at the example of 'stream', I think that coinductive types can be defined as entities whose parts satisfy certain properties. As such, one can't enumerate a stream in the way we enumerate a list like [1;2;3]. This agrees with the fact that coinductive data types are infinite data types. Another way I think about this is, inductive data types are nothing more than what we get from the ways in which they can be formed, and coinductive data types are nothing less than everything that can be destroyed such that the properties specified of the parts are satisfied. Have I got the right intuitions?
[SCW: Yes! You are on the right track. Inductive sets start with nothing and then build up the set through addition. Coinductive sets start at everything and define the set by elimination. ]
-
In such discussions of least and greatest solutions to type equations, it's frequently mentioned that there might be other solutions, neither least nor greatest. However, these non-extreme solutions are never specified. Are they ever interesting, and if so, how?
[SCw: see below]
-
Is there any way to characterize the possible solutions to type equations (as in section 15.4)? Are there solutions other than the purely inductive or purely coinductive ones?
[SCW: yes, sometimes there are fixed points besides the least and greatest ones. For example, consider the tree functor: t. 1 + t * t
The least fixed point (mu t. 1 + t * t) includes all finite trees. The greatest fixed point adds all infinite trees as well. Note that there are many ways that a tree can be infinite --- all we need is a single infinite path in the tree. So a fixed point in between would add some infinite trees but not all of them. ]
-
I am confused about the termination property of M. What does it mean that streams are represented as in a continuing state of creation, and not as a completed whole?
[SCW: All M expressions terminate. Even though M can model "infinite" data structures, it still limits how exactly those data structures can be used.]
-
What is the definition of conat? I am not clear of what Bob says about the relation between nat and conat.
[SCW: If you think of types as sets of values, then nat is the set of values that is isomorphic to the natural numbers. conat adds a limit (omega) to this set: a number that is larger than all natural numbers.]
-
Essentially what is the decisive feature of a language having the termination property?
[SCW: As far as I know, there isn't a general property, just a lot of ways that termination can fail. There are a lot of subtle paradoxes that prevent languages from having termination property. ]
-
In what sense are coinductive types dual to inductive types? (category theory?)
[SCW: Notice the symmetry between the intro and elimination forms between the two types. The general forms for inductive type is (where F is the polynomial type operator)
fold :: F (Mu F) -> Mu F rec :: (F a -> a) -> Mu F -> aand then general forms for coinductive types swaps the arrows around:
gen :: (a -> F a) -> a -> Nu F unfold :: Nu F -> F (Nu F)]
-
Why do the type operators in the premises of the typing rules for inductive and coinductive types have to be positive?
[SCW: because of the reliance on map, which is defined for positive type operators.]
-
Could you run a concrete example in class maybe? Maybe nat and say trees? I get the impression that this chapter is about pattern matching but I'm probably wrong since we've already covered that chapter
[SCW: please ask for more examples in class!]