IRC log started Sat Oct 16 00:00:01 1999
[msg(modtunes)] permlog 1999.1016.mod
-:- hcf [nef@me-portland-us208.javanet.com] has joined #modtunes
-:- mode/#modtunes [+o hcf] by ChanServ
* Tril/#modtunes is back from the dead. Gone 24 hrs 36 min 42 secs
-:- water [water@tnt-10-134.tscnet.net] has joined #modtunes
-:- mode/#modtunes [+o water] by ChanServ
-:- SignOff hcf: #modtunes (Ping timeout for hcf[me-portland-us208.javanet.com])
<water> Tril!
<water> we _must_ continue our discussion from a week ago
06:30pm
<Tril> which
<water> the one about types
<Tril> well, ok
<water> not interested right now?
<Tril> maybe shortly 
<Tril> i'm at an installfest
<water> ok, i'm not in a hurry
<water> it's just that i wanted to explain how "types as sets of values" and "types as abstract specs" are not so incompatible
<water> (and i was cut off too quickly)
06:40pm
<Tril> yes, I remember your isp hung up and you never came back the last time
<water> it was a phone system problem... anyway, it's fixed now
<water> anyway, an abstract data type could be characterized as a set of operations which can be performed on the type
<water> the "actual data" stored would then be a stream of states as defined by an initial selector and a following sequence of operator selectors
06:50pm
<water> (with an implicitly-cached updated value stored for quick access)
<Tril> well, i understand that an ADT  is a set of operations on the type..
<Tril> and I dont understand the rest of what you said
<water> well, you could consider the ADT to be the set of operations *without* the type
<water> i mean, the type being the formalism for the data
<water> unfortunately, that doesn't explain how the ADT is mapped to each type
<Tril> no, it doesnt explain how to eliminate the circularity of "definition of a type"
<Tril> If an ADT depends on the set of functions available on the type,
<Tril> and the function definition depends on the set of values in the type, 
<Tril> then the system makes no sense.
<water> hmm
<Tril> It ruins the definition of functions as pairs of values
<Tril> err, sets of pairs of values
<water> not necessarily
<Tril> Instead, functions must rely on intuition and there are then 2 different kinds of types- those that have distinct values, and those that are open-ended in membership
<Tril> anyway the main issue is:
<Tril> if I want to typecheck something, say, "is x in type A?"
<water> in formal logical specifications of algebra, the abstraction is provided by "equivalence classes"
<Tril> and the definition of type A is that operations B and C work on the object
<Tril> err
07:00pm
<Tril> what abstraction is "the" referring to in that sentence?
<water> er... the abtraction _process_
<water> er... the abstraction _process_
<Tril> the abstraction process is provided by equivalence classes? what does that mean and how does it have to do with types?
<water> like describing rationals when you only have integers or naturals
<water> a rational number is the equivalence class of all pairs of integers satisfying a particular multiplication equation
<water> "q={(a,b) : a = b * q}
<water> "q={(a,b) : a = b * q}"
<water> q=a/b
<water> it doesn't specify _how_, it specifies _meaning_
<Tril> fine, that is perfectly clear
<water> really? wow
<Tril> but the question I have is, how do you take a reference to a specific rational number, given the definition you gave of a rational number.
<water> ah
<water> you must have a system that recognizes _representations_ of that number
<Tril> I.e. you need a more specific definition of the set of values that correspond to each possible rational number.
<Tril> values would be the abstraction that is independent of representation 
<water> btw, there is an entire theory of representations (how to make abstract types realizable with formal languages, formally)
<water> i'm not sure what you mean by "more specific"
<water> i mean, i _can_ specify it via formal logic
-:- hcf [nef@me-portland-us230.javanet.com] has joined #modtunes
-:- mode/#modtunes [+o hcf] by ChanServ
<water> and representation theory provides for making effective functions that can parse languages to determine type
07:10pm
-:- Kaufmann [Kaufmann@dial485.infolink.com.br] has joined #modtunes
<water> darn, i forgot the syntax for giving someone a voice
<water> sorry kauf, i'll figure it out
<Tril>  /mode #modtunes +v kaufmann
-:- mode/#modtunes [+v Kaufmann] by hcf
<water> thanks, guys
-:- eihrul [eihrul@usr5-ppp49.lvdi.net] has joined #modtunes
-:- mode/#modtunes [+v eihrul] by water
<hcf> water: +v doesnt matter atm since #modtunes is -m
<water> hmm
<water> btw, check the logs, all, for discussion history. the first part was over a week ago, and now we continue
-:- mode/#modtunes [+m] by water
<water> Tril: so, what would we need beyond that? (i'm definitely for the notion that much is needed for integrating these formal languages)
<Tril> there is some confusion in my mind because there are 2 different kinds of types that I am thinking of
<Tril> one kind, doesnt ever need to be typechecked because its type is tagged (or part of representation) when it is created
07:20pm
<Tril> the other kind clearly does- but do I even need that second kind?
<water> give an example
<water> not sure what you mean by "other kind"
<Tril> ok I'm working on this assumtpion:
<Tril> the persistent store is a set of cells, and every cell has a specific value
<Tril> this is so the store can be actually implemented.
<water> right
<Tril> Each cell has a type AND a value.. when creating the cell, you MUST specify the initial value
<Tril> once you have cells like this, you never need to typecheck them.
<water> ok, i follow so far
<Tril> I guess I should do some work on the abstract types
<water> huh?
<Tril> If you want to have a cell that contains a value that might be in more than one type,
<Tril> but it  will only be in one type at a time, then just use a "Sum" type 
<water> dynamic coersion, then
<Tril> well, not technically, because the  operations on the original types dont automatically apply to the "sum" type, 
<water> tell me more about what this "sum" type will do
<Tril> sum is an operation that takes two or more types and returns a type
07:30pm
<Tril> the "sum type" as an ADT has two operations available on it
<water> is there an analogue of this in usual programming?
<Tril> yes, they are called "union" in C
<Tril> type sum is called disjoint union in mathematics
<Kaufmann> Well, I'm off
<water> hmm.. what operations, then?
<Tril> my reference says, type sum (of two types) is constructed by two functions, that take elements of the original types and return elements of the new type
-:- SignOff Kaufmann: #modtunes ("Jesus would make a good main character for a Seinfeld spinoff" - Amber << Well, it got my attention... coming soon, the pilot episode of BEN YOSSEF! Sundays at Atheist News Network!)
<Tril> sum: A x B -> C  , would yield   a function C1: A -> C and a function C2: B -> C
* water/#modtunes makes a note to not give "voice" until requested
-:- mode/#modtunes [-v eihrul] by water
<Tril> and there would be a unique element in C for each element in A and one unique element in C for each element in B
<Tril> the representation for C is usually the same as for A or B with a "tag" added that identifies it as a member of C
<water> sounds "quick and dirty"
<Tril> well, whatever, reps arent important
<water> well, what does it do for the type system, abstractly?
<water> i mean, disjoint unions don't sound very robust
<water> darn it, i must go for now
<Tril> the theory is, if an object is a member of both A and B, it will have two distinct objects in C
<Tril> but if we assume A and B are made of unique elements anyway that would never be possible.
<Tril> 
<water> Tril, think about this stuff. i will be on later, and maybe we can meet and continue this
<Tril> leaving?
<Tril> sorry my net connection dropped (someone unplugged )
<water> yeah, i still mst share my phone line with roommates
<water> s/mst/must
<Tril> ok
<water> btw, i consider your "objects" idea to be my "representations" idea
<Tril> my objects idea is gone for now
<Tril> I dont know what idea you refer to
07:40pm
<water> when you use the word object, i would only use representation
-:- mode/#modtunes [+v eihrul] by hcf
<Tril> when I use object , I'm not sure what I mean
<Tril> bye
<water> i don't consider the object notion to have primal consideration
<water> yeah, bye
07:50pm
-:- mode/#modtunes [+o water] by ChanServ
!Hyrlaris:*! We need more linpeople q3 people @ quake3.roundtablepizza.com
<Tril> huh?
<Tril> sure
* water/#modtunes is thinking of how to continue
<water> what would your "type of types" be like?
<Tril> well, like I said, I thinking about a language that describes sets of values
<Tril> so the type of types would correspond to the set of expresions in that language
<Tril> it would be capable of describing sets of values that are infinite in more than one dimension
<Tril> like real numbers for instance
<water> but"it would be capable of describing sets of values ..."?
<water> the description is an expression, too
08:30pm
<Tril> that's not of a primary importance
<water> i'm not saying the idea is invlaid, it's just weak
<water> maybe i'm asking the wrong question
<water> perhaps this: "what is a set of values used for?"
<water> for instance, the "variable assignment" metaphor is unsafe in general
!Hyrlaris:*! We need desperatly need more linpeople q3 people @ quake3.roundtablepizza.com
<Tril> hjold on, sorry
<water> oh
<water> it just seems that a "set of values" is only good for variables (objects with state), which is unsafe by tunes-standards
-:- SignOff hcf: #modtunes (Ping timeout for hcf[me-portland-us230.javanet.com])
-:- mode/#modtunes [+o hcf] by ChanServ
<Tril> ok
08:40pm
<water> (keep in mind that i've been lisping all week)
<water> :P
<Tril> what are sets of values for ?
<water> if you have, say, a "set of objects", then you apply functions to those objects, not ones with state consisting of that object
<water> set-membership is a predicate
<Tril> here's what I use values for
<water> or a function, if you only see one set per object
<Tril> a value exactly specifies one member of a type, which is not equal to any of the other members of the type, and is equal to itself
<Tril> and I have no idea what you mean by state
<water> state is that which is only updated by assignments
<Tril> ok, cells store state, agreed?
<Tril> so that the store can be implemented?
<water> right, but that's not what the type system sees
<water> not a functional one
<water> s/functional/purely-functional
<Tril> what do you mean
<Tril> (what does the type system see?)
<water> the store is a cache... it should be implicit
<Tril> in what way?
<Tril> implicit?
<water> well, the store as an object is only useful because it has to be modelled to be implemented
08:50pm
<water> remember what i was saying last week about persistent stores for functional languages?
<Tril> no, where did you say it
<water> (10/08)
<Tril> 1999.1008.mod? line number?
<Tril> well, at least you're modem isn't hanging up
<Tril> your
<water> still looking, sorry
<water> 1008.mod @ 6:50pm (sorry, no good text-ed at hand)
<water> the store essentially is a cache for function results, which for high-order languages includes functions themselves
09:00pm
<water> this could be generalized to the notion of caching expressions
<Tril> how do the function inputs originally get in the store?
<water> they would be the outputs of other functions
<Tril> what about just functions that take values that can be exactly represented?
<Tril> are we talking about the same thing?
<water> it seems not
<Tril> my "store" is the API at which data is saved and retrieved
<water> i'm thinking of the store abstractly... the data could be cahced in multiple places
<Tril> it's explicit saving/trestoring,  not any implciit auto-save or implicit- GC
<water> or not at all, whenever the data is quickly calculable
<water> eek
<Tril> yes, assume it's above the level of specific locations like disk or memory, but below the level of caching function resuilts
<water> why?
<water> why pick that level of modelling?
<water> sorry, i'm arguing over a pointless issue :(
09:10pm
<water> i just can't understand why you're discussing low-level issues
09:20pm
<water> still here?
<water> well, at least for the logs, i'll mention that your store's "slots" would probably be better modelled as a finite bit-field
09:50pm
-:- SignOff eihrul: #modtunes ([x]chat)
[msg(modtunes)] newlog 1999.1017.mod
IRC log ended Sun Oct 17 00:00:00 1999