Darren New wrote:
> Invisible wrote:
>> I have absolutely *no clue* what the hell any of that means. But try 
>> it yourself here:
> 
> That makes sense except to the extent that I don't know what LIFT{[]} 
> means.
> 
>> Indeed, all Haskell types are ADTs. Except things like integers, 
>> arguably. OTOH, you could claim that Integer is defined as
>>
>>   data Integer = 1 | 2 | 3 | 4 | ...
> 
> An abstract data type has to define the operators also.

Yeah, I was talking about *algebraic* data type when I said "all Haskell 
types are ADTs". ;-)

>> As for "like say a stack", I'm not really sure what you mean.
> 
> Well, an ADT has to define the type in terms of the operations on that 
> type, not in terms of a list of values/literals.

I think we're still talking about two different meanings of ADT. ;-)

> In other words, for an ADT, there is no indication at all of the 
> representation of values. The value of the stack with 1, 2, and 3 pushed 
> is actually
>  push(push(push(new,1),2),3)
> and not some list expression. *That* is an ADT.
> 
> The advantage is that you can prove things about the behavior without 
> understanding what it's "supposed" to do. For example, you can see it's 
> impossible to pop an empty stack, or to look at the top element of an 
> empty stack, because there's no matching expression for top(new). You 
> can also do things like prove you've covered all the possibilities, 
> prove that one ADT is a superset of another, and so on.

I always wandered what a abstract data type actually is...

The Eiffel guy had a chapter implementing a stack and "proving" that it 
matches the spec. (He attempted to claim that the code *is* the spec.) I 
think he was trying to counter the old "there is no mathematical theory 
to OOP".

At the time, I believed him. Having seen Haskell, and its evil twin the 
Lambda Calculus, I now understand what they mean by "no theory of OOP"...!

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message

Orchid XP v8 wrote:
>> An abstract data type has to define the operators also.
> 
> Yeah, I was talking about *algebraic* data type when I said "all Haskell 
> types are ADTs". ;-)

Sorry. I get them mixed up, since the definitions changed since I studied 
them. I don't hold that "objects" or "classes" are "abstract data types" at 
all, so the two terms mean the same for me.

>>> As for "like say a stack", I'm not really sure what you mean.
>>
>> Well, an ADT has to define the type in terms of the operations on that 
>> type, not in terms of a list of values/literals.
> 
> I think we're still talking about two different meanings of ADT. ;-)

Possibly.

> I always wandered what a abstract data type actually is...

That's what it is. There's even a programming language called "ACT.ONE" (or 
maybe "ACT.1", I forget which) that really has abstract/algebraic data 
types, in that you (for example) don't give actual sequential steps for 
pushing and popping, but you actually wrote the kind of thing that I wrote.

> The Eiffel guy had a chapter implementing a stack and "proving" that it 
> matches the spec. 

That's actually impossible to do, since Eiffel isn't a formal language. 
There's no definition for what "X = Y" means in the language (as in 
assignment operator) so he can't mathematically prove it matches the spec.

> (He attempted to claim that the code *is* the spec.)

Well, it's the spec for what his code does, but that's trivially true of any 
safe language.

 > I think he was trying to counter the old "there is no mathematical theory
> to OOP".

And for the most part there isn't. There's hand-waving mathematics, but not 
something precise enough you can automate it.

> At the time, I believed him. Having seen Haskell, and its evil twin the 
> Lambda Calculus, I now understand what they mean by "no theory of OOP"...!

Yep, exactly. ADTs are the sorts of high-level data types you build out of 
lambda-calculus type rewrite rules. LOTOS is the only actual programming 
language I know of that goes all the way down to that level of mathematical 
detail.

-- 
   Darren New, San Diego CA, USA (PST)
   Why is there a chainsaw in DOOM?
   There aren't any trees on Mars.

Post a reply to this message

>> The Eiffel guy had a chapter implementing a stack and "proving" that 
>> it matches the spec. 
> 
> That's actually impossible to do, since Eiffel isn't a formal language. 
> There's no definition for what "X = Y" means in the language (as in 
> assignment operator) so he can't mathematically prove it matches the spec.

The Eiffel assignment operator is actually ":=", with "=" representing 
(value) equality. But hey, I wouldn't know a "formal lanuage" if it hit 
me...

>> I think he was trying to counter the old "there is no mathematical 
>> theory to OOP".
> 
> And for the most part there isn't. There's hand-waving mathematics, but 
> not something precise enough you can automate it.

It's more the point that every OOP language has a slightly different 
idea about the precise definition of "object", "class", "inheritance", 
and so forth. (Some have SI, some have MI, some have class methods, some 
don't, some have private methods, some don't, some allow public 
attributes, some don't...)

>> At the time, I believed him. Having seen Haskell, and its evil twin 
>> the Lambda Calculus, I now understand what they mean by "no theory of 
>> OOP"...!
> 
> Yep, exactly. ADTs are the sorts of high-level data types you build out 
> of lambda-calculus type rewrite rules. LOTOS is the only actual 
> programming language I know of that goes all the way down to that level 
> of mathematical detail.

Even Haskell doesn't actually possess a denotational semantics - what 
ever the hell *that* means!

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message

Orchid XP v8 wrote:
> The Eiffel assignment operator is actually ":=", with "=" representing 
> (value) equality. But hey, I wouldn't know a "formal lanuage" if it hit 
> me...

A formal language is one with semantics defined by rewrite rules, for 
example. I.e., one concrete enough you can actually prove things about it. 
Eiffel's pre and post conditions are a first step towards that.

>>> I think he was trying to counter the old "there is no mathematical 
>>> theory to OOP".
>>
>> And for the most part there isn't. There's hand-waving mathematics, 
>> but not something precise enough you can automate it.
> 
> It's more the point that every OOP language has a slightly different 
> idea about the precise definition of "object", "class", "inheritance", 
> and so forth. 

That's not really the problem, as long as you define it precisely.

> Even Haskell doesn't actually possess a denotational semantics - what 
> ever the hell *that* means!

I need to go watch some football with the wife, but I'll give you an example 
of LOTOS's semantics later, if you remind me. :-)

-- 
   Darren New, San Diego CA, USA (PST)
   Why is there a chainsaw in DOOM?
   There aren't any trees on Mars.

Post a reply to this message

>> Even Haskell doesn't actually possess a denotational semantics - what 
>> ever the hell *that* means!
> 
> I need to go watch some football with the wife, but I'll give you an 
> example of LOTOS's semantics later, if you remind me. :-)

Or, perhaps *I* need to go watch some football or something? Depending 
on how you look at it... o_O

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message

Orchid XP v8 wrote:
> Or, perhaps *I* need to go watch some football or something? Depending 
> on how you look at it... o_O

That too. Speaking of American football (aka gridiron or olive ball), I was 
highly amused to see the defense players doing teabagging guestures while 
celebrating a particularly effective sack.

-- 
   Darren New, San Diego CA, USA (PST)
   Why is there a chainsaw in DOOM?
   There aren't any trees on Mars.

Post a reply to this message

Darren New wrote:
> A formal language is one with semantics defined by rewrite rules, for 

Of course, wikipedia already has pages on it.

http://en.wikipedia.org/wiki/Process_calculus
   See especially the "reduction" part.

http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes
   See especially the "formal axioms" part.
   I'm sure a bright guy like you can see how this could develop
   into something that would allow you to (for example) prove
   that deadlock can't develop, or that some sequence of states
   is always possible, and so on.

-- 
   Darren New, San Diego CA, USA (PST)
   Why is there a chainsaw in DOOM?
   There aren't any trees on Mars.

Post a reply to this message

Darren New wrote:
> Eero Ahonen wrote:
>> It's not a about Linux, it's about filesystems. How many times you have
>> actually managed to measure any benefit from defragging NTFS partition?
> 
> I have, in very rare cases.  But that's when I've created a file in a 
> way that (for example) made 300,000 fragments of it, which happens very 
> rarely. (It was screwing up some other disk analysis tool which 
> apparently decided to allocate fixed memory blocks for stuff and not 
> check they were big enough.)

Ever seen an NTFS partition with 0 bytes free space on it? ;-)

Post a reply to this message

Invisible wrote:
> Ever seen an NTFS partition with 0 bytes free space on it? ;-)

Only by accident!  :-)

Any FS is going to fragment if you fill it up.

-- 
   Darren New, San Diego CA, USA (PST)
   Why is there a chainsaw in DOOM?
   There aren't any trees on Mars.

Post a reply to this message

Darren New wrote:
> Invisible wrote:
>> Ever seen an NTFS partition with 0 bytes free space on it? ;-)
> 
> Only by accident!  :-)
> 
> Any FS is going to fragment if you fill it up.

Er, yeah. Majorly. And having a defra tool suddenly becomes wildly useful.

I still miss the old days when you could take a filesystem offline to 
defrag it properly... :-(

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message