OK. We have a candidate. Let's see if the types say what Glen thinks they say.
Glen: I don't intend to poke fun by this, so I apologize. I'm trying to make the point that even when the types we have to work with aren't all that complicated, it's very hard to understand what we wrote down. Also, sorry, my intent was to ask that these types be written in BitC rather than in C/C++, but I think we can work with what you wrote. On Thu, Aug 8, 2013 at 2:46 PM, Glen Anderson <[email protected]>wrote: > > A generic list of immutable objects > > cons T { > readonly T *car; > cons T *cdr > }; > So first, the type above omits Nil, so let's rewrite what you said: union list 'a is cons { car: readonly 'a; cdr: list 'a; } nil and now let's see what it means. The list type itself is a generic, mutable list. So far, so good. The mutate restriction is that the *target* of the /car/ field of this list is readonly. But this response doesn't capture my intent, because the list isn't generic in the way that I had in mind. My fault for not stating the problem clearly. I this particular example, we can use a completely vanilla list type: union list 'a is cons: { car : 'a; cdr: list 'a; } nil and instantiate that list as "list readonly T". That instantiation turns into: union list readonly T is cons: { car : readonly T; cdr: list readonly T; } nil which is what we wanted. And this is actually good, because it doesn't mean that we need two distinct generic list types in order to deal with read-only elements. > An immutable generic list of mutable objects > > cons T { > T *readonly car; > cons T *readonly cdr > }; > Rewriting: union list 'a is cons { car: 'a readonly; cdr: list 'a readonly; } nil So how well or poorly does this one fair if we try the generic version? It doesn't work. The problem is that the "readonly" in this type is a property of the list type rather than a property of the element type. And this sort of points out a syntactic problem, which suggests moving the "readonly": union rolist 'a is cons { readonly car: 'a; readonly cdr: rolist 'a } nil or maybe more simply: union rolist 'a is readonly cons { car: 'a; cdr: rolist 'a } nil; OK. There's a sleeping dragon here, but so far so good. This is indeed an immutable list of mutable objects. > The reference to the head of the list would have to be declared readonly. > Actually not. This is still an immutable list, even if we can overwrite the head reference. I do agree that most uses of the list would call for the head reference to be read-only. > > An appendable generic list of mutable (or immutable) objects > > An appendable list of deep immutable objects (sort of).... I realized a moment after posting that this is a horrible test case to try to express. Let me replace the challenge. What we want is an insertable list. The intuition here is that one thread is walking a list while another is updating it. Items in the list don't go away, but new items may be inserted. Now before somebody asks, I concede that we haven't got a type system strong enough to describe the "items cannot go away" constraint.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
