🚀 go-pugleaf

On 13 Mar 91 07:48:23 GMT, gudeman@cs.arizona.edu (David Gudeman) said:

gudeman> I'm not entirely sure I understand what you are getting at, but
gudeman> that's never stopped me from talking before...

Same feelings on my side. I actually think that I expressed myself quite
obscurely, because it seems that we talking of different things...

gudeman> In article <PCG.91Mar12135254@aberda.test.aber.ac.uk> Piercarlo
gudeman> Antonio Grandi writes:

pcg> No, no, we have *two* misunderstanding here. I have never said that
pcg> in this example one need declare *explicitly* the types of the
pcg> arguments of an operator; simply, that a type is defined by the
pcg> operators that can be meaningfully applied to the values of that
pcg> type.

gudeman> What does "meaningfully applied" mean?  In a dynamically typed
gudeman> language, any function can be legally applied to any value.  So
gudeman> are you suggesting that every value has the same <type>?  Or do
gudeman> you want "meaningfully applied" to mean that the function
gudeman> doesn't produce an error message when called with that value?

Let's say then that a type is the intersection of the codomains of a
given group of functions , or something like that.

gudeman> Then what do you do with something like

gudeman>   procedure foo(x1,x2)
gudeman>   if number(x1) then return x1 + x2
gudeman>   else return x2
gudeman>   end

gudeman> where x2 must be a number if x1 is, but otherwise can have any
gudeman> type?

This is the problem of procedures with multiple arguments. We all know
that it can be argued that functions with multiple arguments either have
a single structured argument or are functionals...

This said, let's arbitrarily choose the single composite argument view:
the procedure defines the type of all cartesian products where as you
say either the argument are both numeric, or are of any type at all. In
other words, this procedures by itself defines the type of all pairs,
because it will never fail on any pair of values.

gudeman> I think the whole concept is on shakey ground.

Not much more than other definitions of type... And probably much less,
because it gives an operative definition. Look at the intersection of
the codomains of a given group of functions, and that's a type.

Note that this includes the encoding functions, the typeof function, if
any, and so on. I know it is terribly difficult to "see". Maybe I have
not made very clear that that values and their denotations are *very*
different things in my view, thus encoding (and representation) is
crucial to my argument.

pcg> ... is regrettable and is only really an efficiency hack, just like
pcg> the one between 'eq' and 'equal', and it generates much the same
pcg> class of problems...

gudeman> An aside, 'eq' and 'equal' are semantically distinct.  I would
gudeman> consider the language to be lacking an important operation if
gudeman> it were missing either one.  The same applies to 'eql'.  They
gudeman> all serve different purposes.

No, all, except 'equal', are redundant. We have already been thru this
discussion, and I still maintain that ideally if two values are the same
number, they *must* represent the same denotation. Saying that they
actually encode different denotations simply means, IMNHO, that actually
part of the value has been encoded in its address, which is an
efficiency hack.

pcg> This is wrong, as far as I can see, because then there is no way to
pcg> know the <type> or <typing> of a value...  I think you are wrongly
pcg> assuming, in other words, in your definition above, that there is
pcg> some magic way to know which set a value belongs to, without
pcg> encoding it into the value itself...

gudeman> I wasn't making any assumptions about the representation of
gudeman> values.

Neither I am, but maybe I did not make it clear that to me <value> is
the same as <number>. Period.

gudeman> Frankly, I'm surprised to see representation come up at all,
gudeman> since I don't see what it has to do with the subject at hand

Because I am interested in <type> as in a computer, where all
denotations must be represented by a number which is some string of
digits base 256 (usually).

So, what's a type? Essentially, the (finite!) set of all the the bit
strings that a given set of functions can operate upon, because that's
about as good as you can get. Again, note that typeof maybe one of these
functions, and used by these functions as a filter, and then we have
<typing>, which is a far more restrictive idea.

gudeman> (unless you are thinking of <type> as a particular way of
gudeman> interpreting a group of bytes as a value.  That doesn't fit
gudeman> your definition though.)

Well, it's close to that. Maybe we are reading different thing sin my
definition, maybe you are assuming that we have the same idea of what is
a <value>.

pcg> ... On the other hand if you encode the set into the value itself,
pcg> then you are defining types as equivalence classes, and your
pcg> definition and mine are exactly equivalent.

gudeman> Not at all.  Your definition has the <type> of a value changing
gudeman> when new functions are added.  Mine doesn't.

No, not necessarily, depends on two things: whether you add the new
functions to the group that defines the <type>, and then on whether the
new functions are more restrictive or not.

For example, if 'unsigned' is define by + and -, adding * does not
change the relevant set of values. But adding / does, because its
second argument can only belong to a set smaller than 'unsigned'.
So we have that bitstring '1' belongs to two <types> then.

	Note: in the above the curried function view of multiple
	argument is implicitly used.

gudeman> Then no separate notion of <typing> is needed.

pcg> ... The end result of your proposal is to drop the notion of <type>
pcg> and keep only that of <typing>, not viceversa.

gudeman> I'm throwing away your concept of <type>, as I said.

But I am trying to persuade you that <type> as distinct from <typing> is
a useful notion, at least as an ideal. Having a concept of <type> as I
see it does easily account for example for things like coercions,
multiple inheritance, and mutable typing, which are hard to explain well
if you only have <typing>.

pcg> ... when a new release of Unix switches the implementation of
pcg> /etc/passwd from a text file to an hash file, you need a program to
pcg> convert formats, whose role is essentially that of converting one
pcg> <type> to another to maintain ther illusion that <typing> has not
pcg> changed.

gudeman> The job of the program is to convert from one representation to
gudeman> another.  The set of operations on the file has not changed, so
gudeman> the the <type> hasn't changed, by your definition.

No, it has, it has, because the set of operations also includes, and
here you miss I think one of the crucial points, the set of *encoding*
functions. I tried to be very clear about this; for example I have
written that under my definition

	struct complex1 { float re,im; }
	struct complex2 { float im,re; }

are two different *<types>*, even if their denotation is the same. Why?

Because the following two functions are *different*:

	complex1 operator + (const complex1 a, const complex1 b)
	{ return complex1(a.re+b.re,a+im,b+im); }

	complex2 operator + (const complex2 a, const complex2 b)
	{ return complex2(a.re+b.re,a+im,b+im); }

Because the .re and .im functions in each are *different*.

I think that you are missing that in my view of the world, given the two
struct definitions given above, .re and .im are two *functions* from 64
bit values into 32 bit values, and that they are overloaded on complex1
and complex2; something like:

	float operator .re(complex1 c) { ... }
	float operator .re(complex2 c) { ... }
	float operator .im(complex1 c) { ... }
	float operator .im(complex2 c) { ... }

Just to show you how radical is my approach, to me 32 bit floats are
just four digit base 256 numbers with peculiar definitions of +,-,...
(on most byte machines, that is).

gudeman> Again though, it looks like you mean <representation> when you
gudeman> say <type>.

Not the same thing, but it *includes* the encoding. I am not discussing
category theory, I am discussing <types> in computers languages, where
for example, all types are necessarily finite sets.

Maybe you are assuming that to me <value> == denotation, which is not
what I have written (this is a difficulty I have had with somebody else
by e-mail).

pcg> ... I know no language that IMNHO does a satisfactory job of
pcg> reconciling the gross rigidities of doing <typing> with the reality
pcg> that <types> are equivalence classes.

gudeman> Are you familiar with Common Lisp?  What sort of type do you
gudeman> need that you can't define in that language?

In Common Lisp (minus CLOS) I can define the <typings> I want
(defstruct), but not <types>, not at all.

gudeman> How is an equivalence class different from a set?  And what
gudeman> equivalence relation are you refering to?

We are really talking past each other. Let's say that at a level in
which unfortunately <typing> is already there, CLOS comes pretty close
to implementing my idea of types as equivalence classes of all values to
which a group of functions is applicable.

gudeman> It looks at times as though you mean $equiv(x,y) iff typeof(x)
gudeman> = typeof(y)$ -- which makes <type> and <typing> identical.

No, no, that is what *you* mean. That's <typing>:

gudeman> ...  It also gives you a fairly simple way to define the result
gudeman> of the 'typeof' function(s)...

pcg> This is just <typing>, according to my terminology. You have thrown
pcg> away the notion of <type> entirely.

gudeman> Yeah, that's what I said.  (I get the feeling we aren't
gudeman> communicating...)

I get the distinct feeling that while I see all your points, you disagree
because you don't see some of mine. It may be that maybe I have been too
terse :-).
--
Piercarlo Grandi                   | ARPA: pcg%uk.ac.aber@nsfnet-relay.ac.uk
Dept of CS, UCW Aberystwyth        | UUCP: ...!mcsun!ukc!aber-cs!pcg
Penglais, Aberystwyth SY23 3BZ, UK | INET: pcg@aber.ac.uk