On 8 August 2013 23:08, Jonathan S. Shapiro <[email protected]> wrote: > 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.
I figured this is confusing enough without using syntax I'm unfamiliar with so opted for the comfort of C. In hindsight I should've gone with Haskell. Fortunately your translations have helped a lot so perhaps next time I'll be a little more adventurous. As an aside, you'll also have to excuse my (lack of) use of proper terminology. While I can follow discussions without too much trouble, the terminology isn't ingrained enough for right language to come to mind when discussing language theory. > 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. The fact that the annotation can cross the "polymorphism boundary" breaks all the intuition I have about polymorphic types yet the same in this case the explanation is perfectly reasonable. Even after realising this it's difficult to reason about these cases. >> > 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 Slight tangent into syntax here as I think I'm missing something, this isn't the translation I'd have come up with. Based on the what I know of BitC's syntax I'd translate this back to: cons T { readonly T *car, readonly cons T *cdr }; > 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 This is what I think corresponds to my C-style struct. > 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. > While I agree with this, it strikes me as another example of how adding const/readonly type annotation can seriously mess with intuition. If we don't have const/readonly annotations in our language (or they're rarely used) then conceptually a head reference and the list itself are equivalent. When we add const/readonly annotation this is only true with a read-only head reference and I find myself getting caught out by accidental mutable head references because if I'm passing an immutable list I expect that the callee will always be working with exactly that list. Even if/once the technical challenges for const/readonly types are solved, getting programmers to reason about them effectively is going to be tough. >> >> > 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 > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
