On Sun, Feb 5, 2012 at 6:54 PM, Viktor Cerovski
<[email protected]> wrote:
> Raul Miller-4 wrote:
>> http://blog.lab49.com/archives/3011
>> It's amusing to try to think of how to characterize J arrays using
>> that methodology.
>>
>> Conceptually speaking, J has one type: array, and it's statically
>> typed.
>>
> In other words, we are having here dynamic type.

This is a matter of perspective.

It's also a single static type.

More importantly, J's operations on this type do not, as a general
rule, exhibit "polymorphism", where we have conflicting definitions
which we choose from depending on the type of the data.

[There are exceptions to this rule, especially if we include bugs,
where the implementation conflicts with the dictionary.)

But a bigger problem is that we don't really have a good definition of
"type".  And by "good" I mean:

a. concise,
b. accurate, and
c. consistent.

>>  But other concepts can either specialize that type (let's say
>> that we have a context where we know that the array contains real
>> numbers) or generalize that type (in the context of parsing we might
>> need to deal with verbs).
>>
>> But, for example, the type of the result of i. 2 might be int*int and
>> the type of the result of i. 3 might be int*int*int.  So what is the
>> type of i. i. 4?
>>
>> Maybe 1*(int)*(int*int)*(int*int*int)?
>>
>> No, that does not work -- we are not dealing with shape, yet, instead
>> we want to count elements.

> Exactly, there's no shape information here.  In fact, the type
> you give is just int^6, i.e 6 ints, due to the associativity of the
> product of types, and since the unit type is, well, exactly like 1
> wrt multiplication, it does not play any role here.  More generally,
> 1*int is to be isomorphic to int in monoidal category.

Yes, exactly.

Note also that i. i. 4 has 0 ints... and a shape of four.  So the type
here might be "1" though if you also consider the shape information
the type here might be int*int*int*int.

But there's a bigger fallacy here -- and that fallacy is the idea I
introduced, which is that algebraic data types can be used to describe
individual values.  They can't.  A value only has one possible value
-- itself -- so its algebraic representation would be 1.  Algebraic
data types maybe describe regions of memory (or other concepts which
can be used to represent multiple values...)

>>   So the value representing the type of an
>> empty array is 1, and the type of a bit is 2, and the type of 2 bits
>> is 4...

> What you're doing here, and then continue with more examples,
> is to try to build the type system starting from bits.  That's not
> how we would like to use types however, but rather to just specify
> explicitly some types called, say, Int32, Int64, Word32, SingleFloat,
> etc.

Yes, though my "doing here" is largely motivated by the structure of
algebraic data types.

> Types are only half of the story---there are also operations over types,
> and that's also what we need to take into account when talking about
> types.

That sounds good, though this also introduces other issues.  For
example, every operation needs at least two types (an argument type --
the domain -- and a result type -- the range).  Also, the types which
are associated with operations are often "smaller" than the underlying
type systems.  (I remember the terms "one-to-one" and "onto"
describing the exceptional cases -- where the full range of a "type"
would be used.)

> We should be provided with some operation like + that sums Ints,
> etc, and it is not necessary to have them defined at the bit level at all.

I do not know what this sentence means.  But I will agree that in the
general case of mathematical work we often work with entities which
have no concrete, finite representation.

> So we start with some number of types and operations, and then
> algebraically build new types as well as operations, but the starting
> choice of types and corresponding operations is not necessarily fixed.

This sounds contextual.  In some contexts this would be true, in other
contexts it would be false.

> More importantly, there is no some canonical choice of starting types
> from which everything else could be built up.

Here, I imagine you are talking about the general case of mathematics
rather than the specific case of a programming language
implementation?

-- 
Raul
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm

Reply via email to