hs-plugins, trying to get a version of my generated propositional calculus code working as a dynamically loaded plug-in. I've run into some difficulties with the type signatures of the plug-in API, a concrete plug-in, and the plug-in user.One person present during the defense described it as if I were “chasing five motherf***ers down the street with a baseball bat in my underwear.”
Sounds... spirited.
PS: I have used ∇ above to stand in for the filled box used in the paper, primarily because I can't be bothered making an image of a black box. In addition, neither the ☐, nor the ◊ are all that appropriate either.
Viper Comics: Dead@17: The Complete First Series
Aria Volume One
Remote Volume One
Believe it or not, there's a work of contemporary philosophy devoted to this topic: Saul Kripke's Naming and Necessity. Anyone else here know it? If I remember correctly and follow his arguments from that work (two big ifs), it'd be girl with the same name that Daria should talk to.
Argh!--just realized this: since the hypothesis of the story is that Daria analogue opens the open, then n world Daria should open the door, i.e., the girl who looks like Quinn, etc, but is named Daria. There's potential for "who's on first" dialogue:
<snip>
The issue of trans-world identity is quite interesting philosophically and is one in which there are a lot of points of view.
I, personally, like the counterpart theory (due to Lewis), in which there are no objects that are the same from world to world. What we mean when we speak of Daria from world n is the thing that is most similar to the actual Daria (i.e. the one we thing is "real"). All the "Daria"s are equally real, and completely unrelated, except through the counterpart relation.
There are alternative views in which the Darias are all part of one trans-world object, a kind of Uber-Daria. This is called mereology (IIRC) and the various Darias are just world indexed parts of the trans-world Daria. This view is somewhat related to the idea of temporal identity (i.e. am 'I' the same thing that sat here yesterday and browsed this forum?). The temporal variant is pretty much the same (just replace "world" with "time"), but also a lot stronger as a person has some form of spacial continuity between instants (i.e. I'm pretty close to where I was from one instant to the next), whereas there is no continuity between objects at different worlds.
Another view which might be taken into account is haecceity (literally, "this-ness") in which there is some ineffable thing (a je ne sais quoi if you'll forgive the pretension) that makes Daria-n identical to Daria-m, even if one is a person and the other a cement block. This is, needless to say, a little weird, but the whole concept of trans-world identity is a bit strange anyway.
If anyone cares to read more, I can post some references, or you can just look for books on modal logic (if you like formalisms) or the attendant philosophy of possibility (and lots of other stuff) in your local library.
First of all, I'm no expert, so you'll have to take what I've said, and will say with a grain of salt. Additionally, I'm more interested in the formalisms of modal logic than the attendant philosophical issues, so I don't pay as much attention to them than I might otherwise. I'm writing this the better part of three months after the end of my unit on modal logic. Needless to say, I'll probably make a few mistakes.
If you're familiar with formal logic, you might be familiar with the concept of an interpretation which assigns values to logical formulae. In propositional calculus, or PC, (ordinary two-valued logic with 'and', 'or', 'not', 'implies' and 'equals' and an alphabet of propositional parameters 'p', 'q', ... which stand for propositions). An interpretation of PC is simply a function v [the Greek letter nu, if you can type it :-)], which is a function from logical formulae to true or false.
PC is normal everyday logic. It is simple, obvious, and to most people fairly intuitive. It also doesn't really match the way we speak or think about a lot of things. Things like possibility and necessity ("Surely it is possible that I be Prime Minister."), temporality ("Tomorrow, we will try to take over the world!"), belief ("If Jill knows that John is drunk, she'll ...") and a whole bunch of other things that we talk about can't really be encoded into PC without causing problems.
Modal logic is one approach concerned with reasoning formally about these concepts. In general, modal logic is concerned with reasoning about relational structures, like possible worlds, or instants in time, or any set of things that can be represented as a graph (or network).
The most basic interpretation of modal logic is, as set of Worlds, a Relation between them, and an interpretation function that is a little more complex than that for PC.
I'll skip the whole great big raft of crap on modal operators and more than one modality here, as there are plenty of books on the subject and I wouldn't be able to write a passingly good blurb, never mind a book.
Another form of logic for reasoning about relational structures is quantification theory (QT). The main difference between modal logic and QT, is their perspective. In modal logic, one examines the structure from the inside (e.g. from the "world n", or "time t", etc) whereas with QT one has a gods eye perspective (e.g. you can see all the objects, not just the ones you can reach from here).
With plain modal logic, W (the set of worlds, times, whatevers) contains the "things" with which the logic is concerned and the most we can do regarding things IN the worlds (or times, etc) is say "the cat is green" is true or not. Combining QT with modal logic however we can say things like: it is possible that, for all objects x, if x is a cat, then it is green (which would be something like:<>(Ax . isACat(x) -> isGreen(x))where the <> is a diamond modal operator and the A should be upside down and stands for "forall", but I can't be bothered trying to type the correct symbols).
This then leads to a number of logics, one of which has the interpretation, a Domain of all objects (all the objects in all the worlds), a set of Worlds (times, etc), an accessibility relation between the members of W, and v (the truth function). Then all the mess comes in about objects being present in two worlds (if there is me in world n and me in world m, then are they two different objects in D? Are they the same object in D? If they're the same object, how can they be in two worlds at the same time?, etc). There is LOTs of stuff about this, Lewis is a good start (a search for Lewis and modal logic will probably get you heaps), Meinongianism is an interesting perspective where there are non-existent objects like the proverbial pigs-with-wings (Routley Exploring Meinong's Jungle and Beyond). On the other hand, modal logic is not a give and does have detractors. The only one that springs to mind is W. V. Quine.
Merging QT and K (the basic modal logic) as above leads us to questions about identity between objects in different worlds. Is the Daria in canon the same person as the Daria in John? There are four approaches to this that I'm familiar with. The first is to say that there is no identity between worlds, that canon-Daria and John-dating-Daria are completely different entities. This is called extreme essentialism and one proponent is Chisholm.
The second is the counterpart theory proposed by David Lewis and explained, however briefly, in my post on the message board.
The third is haecceitism, also covered above. It is also something of a cop-out to say that "canon-Daria and John-dating-Daria are identical because they are" (in my opinion at least).
The fourth is mereology. This holds that canon-Daria and John-dating-Daria are parts of Uber-Daria, a trans-world "whole" composed of all the Darias in all the worlds. This is similar to an approach to temporal identity, as I explained previously. An interpretation of a mereological modal logic might bewhere the Domain is a set of parts (the things in worlds) and the members of the set of Worlds (times, etc) are linked by a Relation. There is also a set of Functions which, given a world, return a part from D. The members of D then, are the things that exist in worlds, and the functions in F are "individuals". That is, f (a member of F) represents Daria. At the world canon, f returns canon-Daria, which is the thing that is "Daria" at the world canon. At the world John, it returns John-dating-Daria, which is the thing that is "Daria" at the world John. There are a few philosophical approaches that result in a semantically equivalent logics, but I can't really remember them.
If you're interested, I'd recommend seeing if your local University offers a course about modal logic, and see if you can go along. There are also a wealth of fairly good books on modal logic. If you like formalisms (i.e. mathematical proofs, etc) "Modal Logic" a volume in the Tracts in Theoretical Computer Science series from Cambridge University Press is good as well as detailing the true generality of modal logic (the modal operators and multiple modalities mentioned above). Finally, there are a large number of resources on the web. There are lots of 'blogs by students of logic, and you should be able to find a lot of paper, most of which won't make much sense.
I'd like my language to have a type system that includes a number of features usually only found in heavy weight languages like Java, Common Lisp and C#. First amongst these is some form of inheritance and polymorphism. This has fairly obvious benefits, and is something I missed during my brief foray into the world of Haskell (either because it isn't possible, or I didn't know how). Second is some form of parametrised types to implement generics (and whatever else one uses parametrised types for). Parametrised types and generics are a more subtle beast. I don't really know if they will be any harder [than inheritance and polymorphism] to implement, but they will make any language immeasurably more usable, especially for collections and various patterns involving proxying of one form or another.
Another aspect of the type system that will be essential is being light weight. If the language winds up supporting run-time loading of objects (like Java, C#, et al) it will need to support run-time type checking, which means that it'll have to have some form of type tagging, boxing, etc. I would like to keep this as minimal as possible, ideally, it would be [at most] a single word per object.
Hand in hand with the specialisation and polymorphism and parametrisation (in my opinion at least) is support for object-oriented programming techniques. Whilst I'm still of two minds about making everything an object, I do think that the <object>.<verb> form makes a lot of sense for certain operations. I also think that supporting a restricted multiple inheritance, be it mix-ins or just interfaces, paired with polymorphism, can provide similar amounts of power to operator overloading in C++, or type classes in Haskell.
In addition to object orientation, I think that fine grained access to memory is essential. One of the main goals I have is to be able to do similar things with objects and collections in my language, as I can do with arrays of structs in C, with similar efficiency. This will probably mean that the user will need to have some way of controlling memory access, probably via the type system.
Whilst I do like functional programming, sometimes (especially when dealing with things like the "tables" described in point 3) a little bit of statefulness is essential. As cool as the monads in Haskell are, I'm going to try making functional-ness optional. Things like predicates should be functions. Things like operators should, arguably, be functions. Accessor methods probably shouldn't.
I love the idea of language level support for concurrency. Transactional Memory (see my earlier posts) is a brilliant idea. The paper on undo in C# is also fairly interesting. I intend to use native threading support in my run-time to implement things like co-routines and actors as well as more traditional concurrency primitives. This is one the aspects I find most interesting. Adding support for high level concurrency primitives will have, I hope, a similar degree of impact on the languages usability as generics.
