IRC log started Thu Apr 22 00:00:00 1999 [msg(TUNES)] permlog 1999.0422 -:- SignOff Tril: #TUNES (Ping timeout for Tril[sloth.wcug.wwu.edu]) -:- Tril [dem@sloth.wcug.wwu.edu] has joined #TUNES -:- mode/#Tunes [+o Tril] by ChanServ -:- ivan [ivandrago@ih-172.arrakis.es] has joined #Tunes -:- SignOff ivan: #TUNES (Ping timeout for ivan[ih-172.arrakis.es]) -:- Connection closed from king.openprojects.net: Success -:- Connecting to port 6667 of server king.openprojects.net [refnum 0] -:- BitchX+Deb1an: For more information about BitchX type /about -:- Welcome to the Internet Relay Network TUNES -:- Your host is king.openprojects.net, running version u2.10.04.resolv9.nmt.egcs4.tok.pten.tlim4.admin.upper4.whisper3.gipl.modeless7 -:- This server was cobbled together Sat Jan 23 1999 at 21 33:38 EST -:- king.openprojects.net u2.10.04.resolv9.nmt.egcs4.tok.pten.tlim4.admin.upper4.whisper3.gipl.modeless7 dioswkfcg biklmnopstv -:- [local users on irc(3)] 1% -:- [global users on irc(74)] 33% -:- [invisible users on irc(152)] 67% -:- [ircops on irc(13)] 6% -:- [total users on irc(226)] -:- [unknown connections(0)] -:- [total servers on irc(33)] (avg. 6 users per server) -:- [total channels created(58)] (avg. 3 users per channel) !king.openprojects.net Highest connection count: 6 (5 clients) -:- Mode change [+f] for user TUNES -:- Mode change [+iws] for user TUNES -:- JOIN activated by "TUNES #tunes tunes@bespin.cx " -:- TUNES [tunes@bespin.cx] has joined #tunes -:- [Users(#Tunes:3)] [ TUNES ] [@Tril ] [ Fare ] -:- Channel #Tunes was created at Sun Feb 28 08:48:06 1999 -:- BitchX+Deb1an: Join to #tunes was synced in 6.822 secs!! -:- Mode change [-s] for user TUNES -:- hcf [nef@me-portland-us1004.javanet.com] has joined #tunes -:- abi [abi@bespin.cx] has joined #tunes -:- SignOff hcf: #TUNES (Leaving) -:- SignOff Fare: #TUNES (Back to the Tunes OS project -- /whowas Fare) -:- Fare [rideau@quatramaran.ens.fr] has joined #Tunes -:- SignOff Fare: #TUNES (Connection reset by pear) -:- iee [ODO@153.34.221.215] has joined #Tunes -:- iee [ODO@153.34.221.215] has left #Tunes [] -:- Fare [rideau@quatramaran.ens.fr] has joined #Tunes -:- ^lilo [lilo@varley.openprojects.net] has joined #Tunes lilo!!!! 02:00pm -:- SignOff Fare: #TUNES (Connection reset by pear) -:- Iepos [root@d16.t1-6.tecinfo.com] has joined #TUNES -:- SignOff Iepos: #TUNES (Read error to Iepos[d16.t1-6.tecinfo.com]: Connection reset by peer) * Tril/#TUNES is back from the dead. Gone 18 hrs 14 min 21 secs * Tril/#TUNES is away: (afk) [BX-MsgLog Off] -:- Iepos [root@d12.t1-10.tecinfo.com] has joined #TUNES -:- SignOff Iepos: #TUNES (Iepos) -:- _QZ [brand@p0wer.qzx.com] has joined #tunes -:- Iepos [root@d22.t1-1.tecinfo.com] has joined #TUNES -:- SignOff Iepos: #TUNES (Leaving) * Tril/#TUNES is back from the dead. Gone 3 hrs 35 min 26 secs -:- Iepos [root@d9.t1-1.tecinfo.com] has joined #TUNES hello hello hoy, Iepos whats up? i'm revising my spec :) have you read it? yes a couple days ago i'm going to look at it again. i forgot most of it reload it if you want to see what I changed so far. I made the new parts in green so you can find them okay... is this your "intensional metamodel" i heard you were working on earlier ? yeah, sure! it's tunes :) or my tunes, anyway so this is more your goal for tunes than a way for implementing it? the way of implementing it is completely left out :) yeah ... :-) that's what a specification is, it's the part that defines something. implementation may change, but the spec doesn't. Specifications and implementations will be part of the system, much later. i like the idea of hiding IDs ... or at least not forcing the user to manually manage them users should be able to refer to objects using any naming concept, not just by an ID... i mean naming system if you want to manage them, you have to modify the code for the Persistent Store. but you are right, you shouldn't ever have to do that. names are just part of an object, and you don't need to modify the PS to use them. 06:50pm Sometime I'm going to have to write up a doc that descibes what i want in TUNES... ok hmm ... in fact, I might start on it tonight ... :) :-) actually, this spec is similar in many ways to what I want... I think I might approach evaluation a little different, though... Evaluation, as i understand, is the process of representing a concept in a certain desired form (a "normal" or "fully-reduced" form)... in what way But I don't see the need for just _one_ system ... system-wide standard for what a normal form is. different users may like information presented in different forms... that's why I listed about 10 different kinds of evaluators. for instance, some may like decimal or some hexadecimal... some english, some french, etc. there's even more than that, so you can choose the one that uses the form you want. or some other language yeah but I thought those evaluators were just different ways of doing basically the same thing ... ? actually, I want to encourage people to design programs to be evaluators themselves. (VMs) all of computing is different ways of doing the same thing. in TUNES, we say the one thing is "translation between two types" but since you can do anything as a translation between two types, calling it that has no meaning, it's just terminology. hmm ... ? what does it mean to translate between two types? however, that is the paradigm that *I* want to use. Anyone else is free to modify tunes to change that. (more likely, just ADD theirs instead of change it) that's what a function is for, to take something in one type and produce something else in another type 07:00pm yes, in a finished system users should be able to describe things in whatever way is most convenient ... no need for a fixed "paradigm" ... parts of the system described using one paradigm with work seamlessly with parts written in another "paradigm" ... oh ... i see a function as really more of a transformation though than a translation... because the return value is a different concept than the parameter ... the return value is not just the parameter written in a different language. but maybe that is what you mean by translation. yeah you can do transformations, and some of them might be translations. but whether a transformation is a translation or not, depends on what you do with the result. yes, i was planning on basing my system on functions also ... I'm not sure about the type system though... and since the meaning depends on what you do with the result, I don't need to worry about it in the spec I was planning on definitely having types separate from objects... objects will not have "attached" types ... types will contain objects... this seems to be how you appoach it also... sort of it doesn't really make sense to attatch a single type to an object, anyway. i used to think of it that way, but now I decided that it's both. types contain objects, yes I agree but, in my system, the object IS the set of all types that it is in. which probably makes no sense. most of all, i want to strive for a system in which the user can communicate exactly what he means, without needing to overspecify or conform to a rigid paradigm... how would you do that? (it's a good idea) 07:10pm i don't know how :-) how about having a bunch of information known for each object, and then be able to hide parts that you don't care about, and show the parts that you do? I agree, it doesn't really make sense :-) For instance, it doesn't make sense for an "apple" to be the set of types it is in (fruit, object, etc.) ... at least not to me not just a bunch of information, but ALL information known about an object. I agree that it would be nice if properties of objects could be defined inductively ... Meaning that in creating an object it is not necessary to immediately specify everything about it... Although, actually, in my system there would not really be "creation" of objects in the traditional sense... I think maybe I'm thinking of a higher-level system... One with an almost English-like interface... maybe you mean "abstractly"? in my system, you can create an object and know absolutely nothing about it. All that it is is a unique ID. That is, the system can tell it's different from every other object. but that's it. until you know something about it. I'm saying that users should be able to describe all kinds of facts to system, not justs commands to create or manipulate objects ... that's what i use types for Similarly, in my system, the user would be able to use language symbols to reference concepts that have not been "defined" ... The system will be able to tell it apart from other concepts but will know nothing else until you tell it... types ... (added 2 more paragraphs to the ? section) by saying that an object belongs to a type, you are essentially giving a property of the object... not really important (you dont have to read it now) that is what you're saying I think. yup You can describe all kinds of properties of objects just by saying what types it is in. and the meaning of that property depends completely on what functions are defined on that type. This is a useful paradigm... but I think it could get awkward at times maybe. for instance, say you are describing a number object ("x"), and you want to say that it is a positive number. Then the type paradigm would work well ... but ... what if you wanted to say that your number "x" times itself equals 9. then the type paradigm gets awkward. 07:20pm I'm thinking of a system in which you can describe properties of concepts (objects as you call them) in all kinds of ways ... not just saying that they belong to a type. why is that awkward. In the first case, x is an infinite set. in the second, it's a set of 2. Sounds simpler to me :) what kinds of ways No, actually I was intending to describe a specific number "x", not a set of numbers. i know that if x is positive, then it is in the type of positive numbers but how would you say "x times itself equals 9" using the type paradigm? if x is the square root of 9, it is in the set of {3, -3}. "x belongs to the type of numbers that when multiplied by themself yield 9" ? {3, -3} is a type you are identifying, and then stating that x is in it. you may identify the type in many different ways... okay, that makes sense. but in order for that to work you would already have to know that in belonged to the type {3,-3} what if it was a big number that you didn't know the square root to off the top of your head? then you would have to revert to that big statement I made earlier ? "x belongs to the type of numbers that when multiplied by themself yield 9" ? go back to the first example. if x is positive, I can't list all the positive numbers yes, actually I guess what I'm saying is that the type paradigm would work, but since I see types as a special case of a function (a function returning a proposition (or boolean as you call it) indicating whether the parameter is in it), I don't see why the user should be forced only to use that paradigm... since the paradigm can be used for anything, I don't see why the user is limited if I describe the system using this paradigm. he isn't... it just seems awkward to me... but maybe you were planning on having a nice sugary syntax on the outside to make it better ? I'm talking about the specs, the bare bones. Everything else is built using some extremely simple concepts. yes ... I'm just suggesting that maybe there is no need for the bare bones to include types... since the essence of types can be captured using functions and booleans. 07:30pm then again, if we're interested in just bare bones, then maybe we should go back to combinatory logic with just S, K, and U ... :-) not just functions and booleans. You also need my persistent evaluator. because you're going to be referring to some of those functions and booleans over and over again, in your type definitions. I never learned S, K, and U... i don't suppose you could explain them wait, I thought all you needed was S and K oh they're very simple concepts that can be combined to represent lots of things ... but it is very awkward to program manually using them. K is a function-making function. K x y = x That is, K returns a function that always returns its parameter S is also a function-making function... a function-making-function -making function :-) what's S S x y z = (x z)(y z) you can make all kinds of functions just by combing S and K, but it's very awkward. ok what's U so S and K are just names for commonly used lambda expressions? U is also a function-making-function-making function. it's a little weird i know a bit about lambda calc. yes but they can be used to generate _any_ lambda expression. just S and K suffice for any lambda expression but U is necessary for propositions. why? >>> Tril [dem@sloth.wcug.wwu.edu] requested PING 924834918 622705 from #TUNES specifically, U is "\x y z.forall z, not (x z & y z)" you can use it to say "this and this" or "this or this" or "forall x, forall y, x+y = y+x" ... forall, not, and & can all be written as lambda expressions? not really, combinatory logic with U is more than lambda calculus... if so, then you contradicted yourself lambda calculus doesn't have an "and" or an "or" by itself... although you could pretend there was by using special expressions to represent them. 07:40pm anyway, my point is that a "bare bones" system isn't necessarily the most useful system... although describing the system in "bare bones" terms can give insight in how to implement it... i don't think that's what i meant by bare bones this was a little more extreme than what you meant... i think. what did you mean? well, what did you mean I dont need types, and the same thing can be done with functions and propositions? well, as I see it, the essence of a type can be captured in a function that returns a boolean, indicating whether the parameter is a member of the type. yes. for instance, you could use "\x.x>0" to represent the "type" of all positive numbers... but there's also the evaluator, which must always check that proposition, and abort evaluation of the function if the argument is not in the type. And you need to be able to associate the function, with that proposition. hmmm .... well .... I'm actually not seeing the evaluator as the center of the system... It is often useful to represent a concept using a certain form or data structure, though... the evaluator is required to use any functions. let me think.... 07:50pm in my system, you can't just use a proposition that returns a boolean indicating membership in a type. not really. I can say "2*2 = 4" and I am using a multiplication and equality function but not an evaluator necessarily. now ... many kinds of useful computations may require an evaluator because you also need to know what objects the proposition is applicable to. ie. its type. 2*2 = 4 is not a computation. true it's a theorem :) it is a statement... ok, it's a statement, that becomes a theorem if you prove it. but the system, i hope, should be able to take in arbitrary statements, not just commands... ok, i'm waiting on an answer to my comment about the proposition. heh heh i can prove it, but i'd have to make certain assumptions. :-) all right... let me think all right, the answer is that I am not planning on integrating a type system into my evaluator ... hmm... in other words, your "proposition" isn't a proposition , but a chain of nested propositions. And I call a particular chain of nested propositions, a type. there would be many cases when the evaluator cannot represent the desired concept in the desired form because the form is not adequate or because a function is mis-applied in a meaningless way... i don't see a need to make type errors a special case. huh? the parts of your sentence before and after the ... don't seem to go together. what? i think i am calling a proposition a "proposition". huh ? :-) okay, let me try again. an evaluator converts a concept into a certain form... for instance, one evaluator might convert the concept of the number 12 into the string "12" ... or the number 3*4 into the string "12" ok, i guess. go on there might not always exist a string that represents the concept, because the concept could be malformed... let me explain ... oh, we might just have different concepts of an "evaluator".. lets say there is a function which is only meaningful when applied to numbers ... my evaluator is the center of every DYNAMIC part of the system. Any CHANGE of state must go through the evaluator. It has nothing to do with converting a concept to a certian form. hmmm crap perhaps you are thinking of an evaluator that transforms data structures, like a lambda-calculus reducer ? what did i do what's wrong? hello >>> Tril [dem@sloth.wcug.wwu.edu] requested PING 924836367 401392 from #TUNES -:- Tril [dem@sloth.wcug.wwu.edu] has left #TUNES [] hello ? 08:00pm -:- Tril [dem@sloth.wcug.wwu.edu] has joined #TUNES -:- mode/#Tunes [+o Tril] by ChanServ hello again ... I hit something, my irc client did something because of it, and i didnt know how to get out. heh heh. i think it was a scrollback. oh anyway, is that maybe the kind of evaluator you were thinking of... one that transforms data structures, like a lambda-calculus reducer ? not exactly. it's like the CPU it eats instructions, and it does stuff depending on them. except the instructions can be complex expressions, and you can redefine which ones it eats. oh, okay ... i get it now. my main evaluator is exactly like that, it doesn't output anything, its sole job is to have side effects on the persistent store, and possibly on other entities not represented in the persistent store. let me ask ... is it necessary to specify this evaluator, since it seems to be sort of low-level? not "sort of low-level". It's a single entity in teh system representing a single concept hmmm this is different from how I was planning on doing it ... but go for it... if it works, great. right now, neither of our systems work :-) it has a use. you have to go through it to do anything. the idea of the evaluator is, to start a computation, you put expressions in it any expressions in it are currently being computed. And when they are done, they are no longer in the evaluator. I think the key difference is that I was not planning on the user needing to explicitly tell what should be computed... The user would just tell what he would like the system to do, and the system would do it... Maybe you would consider that a computation though... this isnt really the user level. user interfaces are way above what I'm writing in the specification. except, this is the essential user interface oh ... i think that is where I am lost then... i thought the specs were about the user level... no! At the user level, we have had specs for a long time. "Name a feature? You got it. What does it do? Anything." those are not very specific "specifications" :-) The specs are for a "framework", in which all of those features can be built. actually, I don't think we really do have user specs. yes, well, every user will have different specs. We know We know we want orthogonal persistence, unification of abstractions, security through proofs, etc. etc... That's WHY we don't have user specs. keep listing those, this might be useful though true 08:10pm but surely many users will want many common features oh lets see... there's a big list on the TUNES web site in the FAQ... "What features will TUNES have?" this spec is the unification of abstractions part. It depends on persistence already, but the proofs will be built on top of these specs. (albeit VERY CLOSELY on top) But I do think some detailed user specs could be useful, even though such specs may be too specific for all users (some may like it a different way)... That is why I was thinking of specifying the user interface of how I would like TUNES to be... 3.1 What are the main features of TUNES? 3.1 What are the main features of TUNES? ...Computing System, based on a fully reflective architecture. the reflective architecture is what this spec is for. hmm the wording is wrong, too :) you don't build AROUND a reflective architecture yes I think I see what you are saying... you build in it, and whatever you build gets integrated into it. you're giving specs for a specific way to implement the reflective architecture... albeit, not _too_ specific. anyway, I'm getting sleepy... it's been nice talking with you... i have to leave in a few mins, too all right i'll write up my user specs sometime and see what you think... yeah, i enjoyed it ok see you later! bye * Tril/#TUNES is away: (afk) [BX-MsgLog Off] -:- SignOff Iepos: #TUNES (Leaving) 08:20pm -:- pionero33 [omar@207.248.14.45] has joined #Tunes hello .... -:- pionero33 [omar@207.248.14.45] has left #Tunes [] 09:30pm -:- SignOff _QZ: #TUNES (BRiX [http://www.qzx.com/brix] :: sleep) -:- princesa [gatitarose@dialin50.panama.pointecom.net] has joined #Tunes hola hola -:- princesa [gatitarose@dialin50.panama.pointecom.net] has left #Tunes [] 11:20pm [msg(TUNES)] newlog 1999.0423 IRC log ended Fri Apr 23 00:00:00 1999