Re: A Logical Model for Lists as Relations
Date: 10 May 2006 09:52:45 -0700
Message-ID: <1147279965.202378.274740_at_g10g2000cwb.googlegroups.com>
Hi Marshall,
At this point, I'm going advise extreme caution; type systems are wonderful things, but they are also deep forests where many dangers lurk. Can I advise that if you haven't read the following papers, to do so then revisit your ideas ?
- Mario Coppo, "An Extended Polymorphic Type System for Applicative Languages" Proceedings of the 9th Symposium on the Mathematical Foundations of Computer Science,p.194 - 204, September 1980, available in Lecture Notes in Computing Science volume 88 (Springer Verlag)
- R. Milner, "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences 17 (1978), 348 - 375.
It's been a while since I read these, but they are seminal works. They can be a bit heavy going - read them in conjunction with the Haskell tutorial and with a Haskell interpreter to hand (http://haskell.org) and it should be a bit clearer.
Pressing on :
Marshall Spight wrote:
> Bob Badour wrote:
> > Marshall Spight wrote:
> >
[ snippage ]
> I'm not convinced that "there is only assignment" is the right design.
> (It certainly works as a theoretical basis, though.) If the kernel
> language supports only assignment, and not, say, insert, then
> the implementation of insert must necessarily be hugely expensive.
>
Not at all; you have abandon thinking about the surface syntax and consider what is actually happening. That is, on the surface (in the lingo, in your concrete syntax) you might have some syntactic sugar that lets you say
insert(mylist, myvalue);
but under the surface (in your abstract syntax - the thing your language design would actually work on) you would really be saying
mylist := insert_operator(mylist, myvalue);
The fewest number of concepts make life easiest; so, if you really *must* have variables (and I really don't think we do, but there you are) then having one and only one operator that fiddles around with assigning values to variables makes life so much easier. In passing, if your stick with the "operators working on values" idea, you can pretty much stop thinking about "special cases" and work on the general principles of what you're working on.
> I hate to bring the physical into the conversation, but there are
> times when the logical model constrains the physical implementation,
> and imperative operations is one of those times.
>
You'll have to explain that one to me; more often, the physical implementation can't keep up with the logical model (consider Wirth's Euler language, and the relational model itself). And if you're working at the level of creating a model for lists, you shouldn't be thinking about the physical world at all. As long as it faithfully implements the logical model, any physical implementation is correct (it may not be "acceptable" for other reasons, such as time or space performance, but that's the physical implementation's problem).
> I hate to respond with such a generic answer, but "for ordered data"
> is as specific as I can get. Character strings are a good example.
>
Given the amount of head scratching and work you're going to be getting into to make this work properly all round the houses, you'd better have a better battle cry than that !
> Convenience merely. But it is a *lot* of convenience.
>
Convenience can be dealt with in all sorts of places, way way above the logical or computational model. Consider the applicative languages (OCaml, ML, Haskell, Hope, etc etc). All of them are in effect different syntactic sugars for the lambda calculus. Is what you're trying to achieve possibly better dealt with at the language level ? Or with macros ?
> Different authors use these terms different ways; for myself,
> I don't see a useful distinction. Maybe "list" is logical and
> "array" is physical? Dunno.
>
Different operators ? Can you address lists by ordinal position (e.g. list_name[3]) ? (In which case, what happens if you attempt to address a non-existent element ?) Can you insert into the middle of an array by shuffling the ordinals of later array elements or can you only overwrite whatever was in a fixed set of locations ? Do arrays have fixed bounds, but lists none ?
[snippage]
Type systems and logical models are *difficult*; there's no getting away from it, however much we might like to try convincing ourselves. And the only way to know that you haven't left some bizarre nook or cranny lying with a nasty surprise in wait for the first person to wander there is to sit down and do a full scale formal exposition of your idea. And no, "formal" English doesn't cut it. I did it once - a while ago - and those 30 pages of equations have left a long term mark on me. That's why I'm deeply cautious about the D type system, and at this point tend towards viewing useful progress as being a combination of Milner's type system (a la ML or Haskell) for thinking about individual data elements with the relational model for thinking about facts involving those data elements. (While accepting that D's possreps have possibly unexpected handy side benefits in version control.)
I've been typing lots and typing quickly, so I've probably made a whole pile of howlers here. I would wait, but I might not get another chance to reply to this for a little while !
- Tony