🚀 go-pugleaf

In article  <PCG.91Mar15201131@aberdb.test.aber.ac.uk> Piercarlo Antonio Grandi writes:
]gudeman> What does "meaningfully applied" mean?  In a dynamically typed
]gudeman> language, any function can be legally applied to any value...
]
]Let's say then that a type is the intersection of the codomains of a
]given group of functions , or something like that.

OK, so what is the codomain of a function?  You have only pushed off
the problem, not solved it.

]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...

Not unless the appropriate tuples or functionals are in the language.
Otherwise you have to deal with real multi-argument functions.  In any
case, you still haven't said what you mean by "meaningfully applied".
I don't believe you can make it mean anything outside of a statically
typed language.

]...values and their denotations are *very*
]different things in my view, thus encoding (and representation) is
]crucial to my argument.

OK, this is what you seem to be saying

<value>  --  a bitstring

<encoding>  --  a rule for translating <value>s to values and vice versa.

<denotation>  --  the value represented by some <value> under some
<encoding>.

<type>  --  an <encoding>.

The obvious question is: why try to redefine two useful commonly
understood terms, namely <value> and <type> to mean things that
already have perfectly good terms, respectively "bitstring" and
"encoding"?  I know, you claim that <encoding> is only a part of
<type>, but I don't see it.  You just say that a certain set of
functions use a certain <encoding> to interpret their arguments, and
that these functions define a <type>.  But that is no different than
saying that a <type> is an <encodig>.

[about 'eq, 'eql, and 'equal]

]No, all, except 'equal', are redundant. We have already been thru this
]discussion, 

(not with me)

]and I still maintain that ideally if two values are the same
]number, they *must* represent the same denotation.

Why?

] 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.

First, it is unlikely that the same bitstring represents two different
values.  Rather, two different bitstrings may represent the same
value.  But this is low-level implementation detail, and shouldn't
enter into a discussion of semantic issues.

Semantically, Lisp objects can be mutable, and when you have mutable
objects there is a difference between identicality of objects and
equivalence of values.  Furthermore the difference is important for
algorithmic reasons, not for efficiency reasons.  When you have two
lists, A and B, and you want to know if a side effect to A might
change B, you can't find out with 'equal.

]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.

You are assuming that values (<denotations>) are represented as
numbers (actually bitstrings).  You are also assuming that the same
bitstring must represent a different value for different types.
Neither assumption is reasonable.

]... 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).

I am interested in <type> as in programming languages, where you don't
have to specify the hardware representation of values.  Your
definitions are no more than a formalization of the way types and
values are implemented in statically typed languages.  They are not
suitable for discussion of more general types of programming languages
nor for discussion of high-level, abstract issues.

]... 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>.

These things are all quite trivial to explain using the notion that a
type is a set or a unary predicate.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman