From: S Perryman on
Dmitry A. Kazakov wrote:

> On Sun, 18 Apr 2010 11:45:27 +0100, S Perryman wrote:

>>What I contend is that the maths skills I use to construct and
>>deduce type substitutability (utility and conflicts) in all the systems I
>>develop, is of the level I had pre-university.

>>If a type checker has the equivalent ability, then IMHO that would be
>>enough to be very useful to allow much better type substitutability
>>regimes than just basic structural equivalence etc.

> No doubt, but presently we cannot build a system as "simple" as a bee.
> Pre-university kids seem a little more intelligent... By that I only mean
> that this were not a good way to estimate the complexity of the problem. It
> might be simple, complex or "overly complex" (like when checking types were
> more complex than designing the program itself).

All I can state is what I believe is required in order to be useful.
Whether what is required is practically achievable with technology
(existing, near-future etc) , is for others to say.


>>Ideally at what is usually the "compile" phase, but if more practical to do
>>it at the "link" phase, so be it.

> But that would in effect disable dynamic linking.

Not at all.

With dynamic linking, the basic concept is that when use of an entity is
required, the loading process either finds the entity, or does not.
The overall program then continues to execute, or fails.

In a similar vein, you have to decide what the loading process entails
for multiple dispatch.

What information must be available in the running program +/- each
loadable unit, in order that the outcome is the same as if a type
checker statically analysed all the program units as one monolithic
system ??

Until this is known, all other issues (resource usage, distribution etc)
are moot.


Regards,
Steven Perryman
From: Dmitry A. Kazakov on
On Sun, 18 Apr 2010 16:59:15 +0100, S Perryman wrote:

> Dmitry A. Kazakov wrote:
>
>> On Sun, 18 Apr 2010 11:45:27 +0100, S Perryman wrote:
>
>>>Ideally at what is usually the "compile" phase, but if more practical to do
>>>it at the "link" phase, so be it.
>
>> But that would in effect disable dynamic linking.
>
> Not at all.
>
> With dynamic linking, the basic concept is that when use of an entity is
> required, the loading process either finds the entity, or does not.
> The overall program then continues to execute, or fails.

It is not that simple. There reason to fail must be all on the caller's
side. I.e. it can fail if I do something wrong, e.g. trying to bind to a
non-existent entity. The problem with failed consistency checks is that it
can fail because of something I cannot/will not control/foresee. This is
somewhat similar to loading libraries of incompatible versions, but much
worse. Most likely I will have no slightest idea what the problem is. One
library provides a new printer, another does a new shape, and I, the end
user, cannot use them together even if I don't use the missing combination.
Even worse, if I don't print anything, but there is a third library that
does, it won't load. That looks like a maintenance disaster.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
From: Nilone on
On Apr 18, 10:57 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de>
wrote:
> Tuples, arrays and records are classic examples of container types.

They're how containers have classically been implemented. I see a
container as an ADT which accepts and returns objects. Tuples (aka
records), arrays and relations are data structures, i.e. they're just
ways of logically arranging things. A tuple of values is a composite
value, e.g. the point (X:2,Y:3). A tuple of variables is a composite
variable, e.g. a point variable. A tuple of algebraic types is itself
an algebraic type, e.g. the cartesian plane / space.

> > The problem isn't with the values, but with the container.  A sequence
> > of things isn't the same as a sequence of things inside a container.
>
> A sequence is another word for ordered container.

The fibonacci sequence and the digits of my credit card aren't ordered
containers. They are arrays of values, though.

> > It's the algebraic vs coalgebraic difference again.
>
> I see no reason to promote such difference. It does not exist to me.

May I recommend the writings of William Cook and Bart Jacobs? ;)

> I seems that you consider containers having referential semantics. These
> are not equivalent.

I consider containers as objects which accept and return objects. I
consider data structures as arrangements of multiple objects.

>
> >> Consider an array of
> >> Boolean packed into a register. Does it bother you that X[3] physically
> >> does not exist in the memory?
>
> > Well, I can't subclass a boolean, so covariance isn't going to be a
> > problem, right?
>
> Why cannot you. Why Boolean is better or worse than Employee? Why should
> not I derive Belnap_Logical from Boolean?

OK, you can subclass it. Now what does it mean when someone writes
Boolean[] X = new Belnap_Logical[5]; in C#, and what happens to your
register?

> > You seem to associate arrays with physical layout in memory.
>
> I do not.

My apologies, you already said you view arrays as ordered containers,
which I assume means objects with methods and hidden representation.

>
> > I don't
> > see that the two are necessarily related.  An array is a logical
> > arrangement of things.  The compiler can implement it how it wants to..
>
> That is my point, not yours! (:-))

It's my point too! If you want it for yourself, you'll have to win
it. :P

> > If I say I want a variable for a relation over two ints, the rest is
> > implied.  I don't, however, think of layers of containers, instead I
> > think of one variable containing a complex value described by the type
> > RELATION (X INT, Y INT), and generic methods that can derive
> > relations, tuples and ints from that value.
>
> What is the profile of the operation SELECT, INSERT?

SELECT derives a relation from a relation - in the same way as copying
an image (or part of it) is itself an image. INSERT is shorthand for
a read-modify-write type operation (like i++), i.e. the relation in
the variable is replaced with an updated relation.

>
> >> But that is not all. Let you derive positive from int. What happens with
> >> the table? How the table, result sets of positive is related to the table
> >> of ints? Can you reuse operations of the latter?
>
> > If the positive type is a subset of the int type,
>
> Types are not sets. The domain set of positive might be a subset of int.

Yes, that's what I meant. However, look back at your question (result
sets of positive?), I'm not sure I understand what you meant. A
relation over the domain set of int will always be a relation over the
domain set of int. A relation over the domain set of positive is a
different relation. You could derive one from the other, using an
explicit or implicit function from the source to target domain set.

>
> > then positive is
> > already included in the relation and it applies without any
> > modification.
>
> Really? Does it mean that I can insert (-1,-1) into the table?

Assuming the obvious meaning of int and positive, you can insert (-1,
-1) in a relation over (X int, Y int) if it isn't already in there.
You couldn't insert it into a relation over (X positive, Y positive).

>
> Note that positive is not an LSP subtype of int. But even if it were, the
> problem is when and how a container type (or any other type built by a
> type-algebraic operation) based on a subtype is a subtype of the
> corresponding container type, based on the supertype. This is not a trivial
> question.

That's my point, not yours! ;)

That's what I referred to with array covariance problems, and what I
meant when I said a sequence of objects isn't the same as a sequence
of objects in a container. You express it much more clearly, though.

The problem is easily resolved with algebraic data structures.
Consider the statement int[] X = new positive[10]; in C#. Excuse the
pedantic language below, I'm trying to explicitly distinguish between
different points of view in which the same words are used.

View 1 (what I call the coalgebraic view): X is an object (the
variable) which contains an object (the value) which contains 10
positive objects. The variable object, like any other mutable object,
can accept instances of subtypes of the declared type/class. Although
the language allows us to assign an object containing positive objects
to X, it's a mistake because an object containing positive objects is
not an object containing int objects. If we pass the contents of
variable X to a method which accepts an int[] and assigns a negative
object to the third slot, we'll get an error.

View 2 (what I call the algebraic view): X is a variable (not an
object) containing int slots (not objects) to which we assign 10
positive objects, i.e. each positive object goes into a slot of the
variable. If we pass variable X to a method which accepts a variable
of int[], it can assign a negative object to the third slot without
any error since it replaces the positive object in that slot. If we
pass the contents of variable X to a method which accepts an array of
int values, the objects in the slots are copied to the slots of the
variable provided by the method, and the method will read a sequence
of int objects as it expects.

Nilone
From: Nilone on
On Apr 18, 9:18 pm, Nilone <rea...(a)gmail.com> wrote:
> > A sequence is another word for ordered container.
>
> The fibonacci sequence and the digits of my credit card aren't ordered
> containers.  They are arrays of values, though.

I mean sequences of digits. Same thing. I'm sure you got the point.

> Yes, that's what I meant.  However, look back at your question

I meant "looking back", obviously.

Nilone
From: Dmitry A. Kazakov on
On Sun, 18 Apr 2010 12:18:04 -0700 (PDT), Nilone wrote:

> On Apr 18, 10:57�am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de>
> wrote:
>> Tuples, arrays and records are classic examples of container types.
>
> They're how containers have classically been implemented. I see a
> container as an ADT which accepts and returns objects. Tuples (aka
> records), arrays and relations are data structures, i.e. they're just
> ways of logically arranging things.

Isn't container a "data structure"?
How are arrays "implemented"?
What does it mean to "arrange" "things"?
What is "thing"?
------------------------------------------
Ergo: many superfluous words.

> A tuple of values is a composite
> value, e.g. the point (X:2,Y:3). A tuple of variables is a composite
> variable, e.g. a point variable. A tuple of algebraic types is itself
> an algebraic type, e.g. the cartesian plane / space.

Tuple value /= tuple object /= tuple object. Compare: integer value,
integer object, integer type. Array value is a container value. Array type
is a container type. Array object is a container object. In short, array is
a container.

>>> The problem isn't with the values, but with the container. �A sequence
>>> of things isn't the same as a sequence of things inside a container.
>>
>> A sequence is another word for ordered container.
>
> The fibonacci sequence and the digits of my credit card aren't ordered
> containers. They are arrays of values, though.

See above. You are mixing values and objects, the program and its
semantics.

In the same vein: the digit sequence of your credit card is a pigmented
plastic surface. So?

>>> It's the algebraic vs coalgebraic difference again.
>>
>> I see no reason to promote such difference. It does not exist to me.
>
> May I recommend the writings of William Cook and Bart Jacobs? ;)

An argument to authority? May I suggest that you misinterpreted their
point? (:-))

>> I seems that you consider containers having referential semantics. These
>> are not equivalent.
>
> I consider containers as objects which accept and return objects.

1. Container value
2. Container type
3. Container object

You use #3 in order to say something about #2. That does not go.

> consider data structures as arrangements of multiple objects.

I thought we agreed earlier that there is no data. How could something
non-existent have a structure? Anyway, I don't care about structures of
data.

>>>> Consider an array of
>>>> Boolean packed into a register. Does it bother you that X[3] physically
>>>> does not exist in the memory?
>>
>>> Well, I can't subclass a boolean, so covariance isn't going to be a
>>> problem, right?
>>
>> Why cannot you. Why Boolean is better or worse than Employee? Why should
>> not I derive Belnap_Logical from Boolean?
>
> OK, you can subclass it. Now what does it mean when someone writes
> Boolean[] X = new Belnap_Logical[5];

This means "type error". Boolean and Belnap_Logical are different types.
Remember another point I made earlier. There is a difference between a
specific type Boolean and the type of the closure of the Boolean class. The
former cannot accommodate Belnap_Logical. In a properly typed language:

X : Boolean := Uncertain; -- TYPE ERROR (a Belnap value)
Y : Boolean'Class := Uncertain; -- This is OK, a polymorphic object Y

>>> You seem to associate arrays with physical layout in memory.
>>
>> I do not.
>
> My apologies, you already said you view arrays as ordered containers,
> which I assume means objects with methods and hidden representation.

(Objects do not have methods, types do)

>>> If I say I want a variable for a relation over two ints, the rest is
>>> implied. �I don't, however, think of layers of containers, instead I
>>> think of one variable containing a complex value described by the type
>>> RELATION (X INT, Y INT), and generic methods that can derive
>>> relations, tuples and ints from that value.
>>
>> What is the profile of the operation SELECT, INSERT?
>
> SELECT derives a relation from a relation - in the same way as copying
> an image (or part of it) is itself an image.

No it is not same, because SELECT may return other type, e.g. a table with
a reduced number of columns.

> INSERT is shorthand for
> a read-modify-write type operation (like i++), i.e. the relation in
> the variable is replaced with an updated relation.

Whatever, what is the profile of these operations, which, by the way, are
methods? You have to declare ALL of them. My wild guess is that the number
of such methods is countable infinite! Which is the core problem.

Here is an analogy. An integer type is an enumeration (discrete type) plus
some operations of Abelian group. Now imagine a language without integer
types. Let you wanted to declare one using enumeration:

enum int {0, 1, -1, 2, -2, // see the problem?

A language of enumerations is to weak for integers. Contemporary OOPL type
systems are too weak for relational ADTs.

>>> then positive is
>>> already included in the relation and it applies without any
>>> modification.
>>
>> Really? Does it mean that I can insert (-1,-1) into the table?
>
> Assuming the obvious meaning of int and positive, you can insert (-1,
> -1) in a relation over (X int, Y int) if it isn't already in there.
> You couldn't insert it into a relation over (X positive, Y positive).

q.e.d.

>> Note that positive is not an LSP subtype of int. But even if it were, the
>> problem is when and how a container type (or any other type built by a
>> type-algebraic operation) based on a subtype is a subtype of the
>> corresponding container type, based on the supertype. This is not a trivial
>> question.
>
> That's my point, not yours! ;)
>
> That's what I referred to with array covariance problems, and what I
> meant when I said a sequence of objects isn't the same as a sequence
> of objects in a container. You express it much more clearly, though.
>
> The problem is easily resolved with algebraic data structures.
> Consider the statement int[] X = new positive[10]; in C#. Excuse the
> pedantic language below, I'm trying to explicitly distinguish between
> different points of view in which the same words are used.
>
> View 1 (what I call the coalgebraic view): X is an object (the
> variable) which contains an object (the value) which contains 10
> positive objects.

This is obviously wrong, because X is declared of int.

> View 2 (what I call the algebraic view): X is a variable (not an
> object) containing int slots (not objects) to which we assign 10
> positive objects, i.e. each positive object goes into a slot of the
> variable.

Variable is an object.

> If we pass variable X to a method which accepts a variable
> of int[], it can assign a negative object to the third slot without
> any error since it replaces the positive object in that slot. If we
> pass the contents of variable X to a method which accepts an array of
> int values, the objects in the slots are copied to the slots of the
> variable provided by the method, and the method will read a sequence
> of int objects as it expects.

Copy vs. referential semantics is irrelevant here. An integer array is an
array of integers. Period.

When you assign an array of positive to an array of integers AND this is
not intended to be a type error (which is a subject of choice), THEN there
is an implied conversion of types in play. Whether this conversion produces
new physical objects (e.g. copy semantics) or else reuses existing objects
(e.g. reference semantics) is an implementation detail, which is irrelevant
so long the program semantics does not change. Your argument brings these
details in, and thus is misplaced.

Since there is only one possible view the distinction is irrelevant. If you
wanted an array of polymorphic int values you should declare it as an array
of the closure int's class. Elements of this array were polymorphic. See?
There is only one view. Make it properly typed and this ambiguity
disappears. This is not the problem I meant.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de