Note: there is example OCaml code for this chapter in fpc.ml and in rectypes.ml.
General idea: recursive types are solutions to arbitrary recursive equations such as those of the form "t = t -> t"
In Ch 20, we define these types by allowing types with recursive definitons:
D, t type |- tau type
---------------------
G |- rec (t.tau) type (note: more common to use "mu" instead of "rec")
The "rec (t. tau)" type is a finite notation for an infinite type, i.e. a type defined by recursion.
For example, natural numbers can be defined as
rec nat. 1 + nat
And a lists can be defined as (for any a)
rec list. 1 + a * list
We also add typing rules for "folding" and "unfolding" these recursively defined types:
G |- e : [ rec t.tau / t] tau
----------------------------------
G |- fold{t.tau}(e) : rec (t.tau) (note: more common to use "roll"
instead of "fold")
G |- e : rec (t.tau)
----------------------------------
G |- unfold(e) : [ rec t.tau / t] tau
- Several times Bob Harper has mentioned "... fixed point of type operators up to isomorphisms". I don't actually know what this means. As in "up to". How do we work up to isomorphisms?
We want to think of "rec" as a way to "construct" types, not as an actual type former. The fold/unfold terms (along with the {t.tau} annotation on fold) are there to make type checking syntax directed. Semantically, we want to think of types as "equal" to their unfoldings. i.e. there should be no difference between the types
rec nat. 1 + nat
and
1 + rec nat. 1 + nat
So the fold / unfold are witnesses to the isomorphism between these two types. The benefit of working with iso-recursive types is that type checking is simple: we know exactly what type
Note: it is possible to design a type system where fold/unfold is unnecessary and these types are equal according to the type system. i.e. language equates a type with its unrolling. In this case we say that
rec a . t === [ rec a .t / a ]
In fact, we can even do so and retain decidable type checking. See OCaml's "rectypes" flag.
- Could you discuss the connection between recursive types as presented in PFPL and types in object oriented languages such as Java and C++, where you typically don't see explicit (or implicit) fold and unfold?
Recursive types exists in many languages. For example, datatypes in ML / Haskell we have
nat = unit + nat
list = unit + nat * list
value = int + bool + (value -> value)
In imperative languages, we often see recursion in "struct" definitions
struct tree = { int v; tree next; }
In OO languages, they may show up in encodings of classes:
class ListNode {
int v;
ListNode next;
}
In both ML based languages and OO languages, we typically do know where we are introducing a value of a recursive type, typically using a data constructor or a class constructor. These constructors take the place of "fold" when it comes to type checking. (And also the type annotation on the introduction rule for sums in the case of datatypes.)
- What exactly is a fixed point of a type operator, especially since types aren't sets? We can't just say its the smallest set satisfying satisfying such and such relations can we?
Ch 20 gives an operational semantics, but what if we were concerned with a denotational semantics? If we think of types as sets of terms we have trouble when we interpret fcuntion types as sets of functions... with recursive types we may need to find a set such that (for example)
A ~= A -> 2
In classical set theory, we know that if A is countable there can be an uncountable number of functions on A, so it is troublesome to make these two sets isomorphic. Bob, however notes that we shouldn't be thinking of sets of arbitrary functions---we should only be thinking of sets of computable functions. And there are only a countable number of those (i.e. we can represent all computable functions as programs, and there are a countable number of programs).
- The introduction to the chapter says, "type equations involving functions have solutions only if the functions involved are partial." Why is it so? Also, can you take up some type equations and discuss their solutions?
- Why does Bob say that type equations involving functions have solutions only if the functions involved are partial?
Good question. We have type equation that we want to solve:
t ~= t -> t
And we know that we can solve it in a setting that can only express computable functions.
So why do we need partial functions? We know that PCF can express all computable functions, so that is a good setting. But what about a system that includes all computable total functions?
Perhaps the answer lies in the fact that if we can solve this equation, we can necessarily write an interpreter for the untyped lambda calculus, which gives us partiality.
- What is the advantage of/motivation behind thinking of types as fixed points of type operators? What sort of types can and cannot be "constructed" this way?
Much of this chapter is examples of code that you can write using recursive types.
- what is the restriction on the type operator?
Bob is talking about the positivity / negativity restriction from chapter 15. In this system, we can define inductive and coinductive types with recursive types. See fpc.ml.
- Could you make more explicit the connection between this chapter and inductive and coinductive types as presented in Chapter 15? Does the translation require you to add generic programming to your language?
Yes, I think that you still need map for the general construction. See fpc.ml.
- Why define FPC when we already have definitions for inductive and coinductive types in Chapter 15? Is it just to demonstrate applying the PCF definitions to the type level, or is there some advantages of FPC over the definitions we have seen in Chapter 15?
Part of this goes back to the discussion in Section 19.5. There is a significant difference between partial and total languages. However, once you have embraced partiality, you don't need to define inductive/coinductive types separately.
- I've been trying to puzzle out a more formal understanding of how strict
positivity prevents non-termination from being introduced. I understand how
you can't construct the data type
self(t) ≅ self(t) -> twithout dropping the positivity requirement, and how this construction leads to general recursion. What I don't formally grasp is how we can show that there is no other way general recursion might arise in a typed language with only strictly positive data types and no value-level self-reference. Is this even the case?
Yes, with strictly positive datatypes and no fix, you have a total language, for example, Coq. However, the argument is subtle.
Note that, as usual, there are two different semantics for recursive types, based on whether we want a strict or a nonstrict interpretation. Our choice of operational semantics determines the semantics of recursive types, which many of you picked up on.
-
My question is why do type equations have unique solutions in the setting of partial functions?
-
Could you clarify more about how the lazy and eager dynamics influence on the meaning of recursive types?
-
My main question is about the expressiveness of eager vs lazy dynamics. Is the point he's trying to make that lazy semantics can be encoded within the eager language itself by thunking while in a lazy language we need an external construct to enforce strictness (like ! in Haskell)? Or does he mean that bang (and similar constructs) can never really encode eagerness completely because of some more fundamental reason I'm missing?
-
In Ch20.2, we know that both nat and lnat satisfy the type equation r ~= [z ~> unit, s ~> r] What relation between the two types can we derive from such satisfaction?
In total languages, we distiguished between inductive and coinductive types because there were multiple solutions to the fixed point equations such as:
mu nat. 1 + nat
Should this type include an "infinite" number (like conats) or not? What is this number? (Note, we can define fix in this language, see below)
fix (\omega:nat. fold (Inr omega))
However, given the presence of ! in Haskell and the strange semantics of OCaml, I'm not sure that things are as clear cut as Bob claims.
- Bob Harper says, "... general recursion may, like other language features, be seen as a manifestations of types structure rather than as an ad hoc language feature." I would hoping you could elaborate and talk about this (if there is anything interesting to say about this statement).
I think Bob is saying that everything interesting in programming languages can be thought of in terms of types.
- Also, what (dis)advantages does PCF have over FPC? Are FPC and PCF as expressive as each other, and how can we tell whether they really are equivalent in this sense? It seems to me that they are equivalent but I don't really know how one would go about formulating that statement and then prove it.
This chapter shows one direction --- FPC is at least as powerful as PCF because we can define fix using recursive types. To show the other direction, we need to argue that recursive types do not make the language more expressive than PCF. I think we could do that by implementing a FPC evaluator inside PCF.
- Why does Bob say that we need full recursive types to implement the RS-latch at the end of the chapter? It seems to me that this is a strictly positive coinductive construction, and so shouldn't need arbitrary recursive types.
I'm also confused about the point of this example. I think a better example would be to define a Heap data structore for a state monad. If we want to store functions in the heap, then we need a negative occurrence to define the type structure.
Heap := label -> Val --- finite map from memory locations to values
Val := Int --- numbers
| (Val, Val, ...) --- tuples
| Val -> Heap -> (Val, Heap) --- store passing function
-
Bob gave an example of RS latch implemented with self-reference at the end of the chapter. Is the idea of state here similar to what imperative programming languages have? My understanding is that this is more like a stream-based state, where new states are unrolled at each step. Is this related to the other kind of "state"?
-
Could we go over the latch example together? I'm not sure I get all the details, especially with how recursive types are needed. I would also like to see the "bigger picture" of the link between statefulness and recursion. For instance, would there be a (somewhat) mechanical way of translating a stateful computation to a recursion-based one? Or is it only for feedback-y systems, like the circuit we're using here? It'd be really cool to encode an arbitrary stateful computation (that doesn't necessary exhibit (explicit) feedback) in a recursive one.