Spin has no types. It has no casts. Period. Repeatedly saying otherwise does not make it different.
That the front-end, probably the scanner, can interpret floating point notation and encode 32-bit values, does not equate to types by any informed definition of the word.
Spin certainly has types. It may not have casts (I suggest it does) but it does have type coercion.
Consider the following code:
VAR
long x
byte y
PUB start
x := 1000001
y := x
What happens in that last line?
i) y gets byte value of 1.
ii) y gets a byte value of 1 and the memory around it is corrupted with the other three bytes of x
ii) Some random other result because a long does not fit in a byte.
iii) The program crashes as you are asking it to do the impossible.
iv) The compilation fails with a type error.
The answer to that question demonstrates that Spin knows about the types of x and y. A long is coerced into a byte.
Things get messy when you are accessing memory through pointers (addresses created with @). Such pointers have no type and you have to take care of it in code.
In the following code I would go as far as to say that the use of "byte[...]" is cast.
VAR
long x
PUB start
incByte(@x)
PUB incByte(byteAddr)
byte[byteAddr] += byte[byteAddr]
The Spin language has no types. Period. You can't alter that fact by continually stating otherwise. You can't argue the language has casts because there is no casting. You can't argue it has type coercion because, again, there is no coercion - only assignment, which is defined as discarding upper bits in order to jam the 32-bit right-hand-side into the container designated by the left-hand-side.
Further, both of your recent example demonstrate that Spin has no types. Allow me to explain:
Let's look at your most recent example.
The declaration of y allocates an 8-bit container in the static, per-object-instantiation scope.
The assignment statement at the end of your example first evaluates the right-hand side of the assignment operator and then stores that intermediate value into the address designated by the left-hand side.
The evaluation of expressions in Spin always yields a 32-bit intermediate result.
This particular assignment operator stores into y using y's width of 8-bits. The semantics of assignment in Spin is to discard the upper bits when the container is less than 32-bits.
Were Spin a typed language, this assignment would cause a compilation error because of type mismatch at assignment. This is the essence of types, that operands of one type must be explicitly converted into operands of another type prior to operating upon them.
Similarly, your previous claim that the right-hand side of a constant declaration with literal syntax like 1E3 implies types, suggests that %101 also implies types - neither is remotely true. The syntax of a numeric constant has nothing to do with types.
All numeric literals in Spin are evaluated at compile time to create 32-bit signed values irrespective of whether they are expressed as float, decimal, hexadecimal, octal or binary. Named numbers, those things created with con sections of source code are similarly untyped.
However, for some bizarre reason known only to the authors of the original compiler, the evaluation of operators in the context of con declarations forbids mixing some forms of literal syntax (like 1e3) with other forms of literal syntax (like %101). The absurdity of this is most apparent once one realizes these things can be mixed in a runtime expression. For example:
con
C1 = 1e2
C2 = 123
C3 = C1 + C2 ' <- this statement is illegal
pub Foo
return C1 + C2 ' <- this statement is legal
That the expression in the return statement is legal demonstrates that there are no types. That the same expression is legal in one context and illegal in another suggests that the compiler author/language designer paid no attention to details; we see this throughout the syntax and semantics of Spin, which are haphazard at best. That the expression in the return statement isn't folded at compile time is further indication that the compiler author/language designer had no idea of how to write a compiler. This stuff has all been well understood for more than 40 years.
We seem to have different ideas about what "types" means.
In my example you quite rightly say "This particular assignment operator stores into y using y's width of 8-bits. The semantics of assignment in Spin is to discard the upper bits when the container is less than 32-bits."
That means that the compiler knows that x is a long and y is a byte. It generates different code than if both x and y were longs.
There is nothing in the line "y := x" that indicates doing different things depending on the size of y and x.
Ergo the compiler has to use the type information to generate the right code.
By your very own argument we see that Spin has types.
Our different views on types shows in your statement "Were Spin a typed language, this assignment would cause a compilation error because of type mismatch at assignment. This is the essence of types.."
It is not necessary for a language to produce a compilation error to be said to have types. We can write almost the same code in C and get the same behaviour. No error. C is a typed language is it not?
Our argument should be more refined: Is Spin a "stongly typed" or "strictly typed" language like Ada? Is a "weakly typed" language like C? "Dynamically typed" like Python or Javascript?
Seems no one can agree on the terminology much. Bottom line is that I'm sure if we look in the source code of a Spin compiler we will find symbol tables recording the types of variables.
Spin does what it does. "Strongly typed," "weakly typed," or "other" languages do what they do. ('Starting to sound like a Geico commercial? ) Anyway, as long as we understand what they "do," why are the exact application of terms even important? Semantics so often lead us down the rabbit hole for no practical utility that I can discern.
The storage size of an allocated variable is entirely separate from the variable's type. Calling the storage size a type does not make it a type. It remains a storage size.
Storage size is only pertinent to the implementation operations; usually only load and store. It is not relevant to semantics.
Type is only relevant to semantics; it has no bearing on any operations
That the compiler's implementation refers to the storage size attribute of a declaration as the declaration's type indicates the implementors of the compiler do not understand compilation in the traditional sense. It does not magically transform storage size into type in much the same way that had they called storage size World_Peace, it would not have changed the human condition.
As Phil points out we are just quibbling over the meaning "type" and "typed" in programming languages.
You want a rigorous definition that involves some or all of: type checking, errors on type mismatch, type coercions, casts and so on. This can be carried to extreme, as languages like Ada do. There is a whole formalism for it: https://en.wikipedia.org/wiki/Type_theory
I want to use "type" more loosely, perhaps "storage type" is enough for me. Perhaps syntactically distinct types are enough for me. Spin certainly has those. A floating point value is written in a different way than an integer and is translated into different bit patterns. Even the Propeller manual refers to types.
Would you consider Javascript typed? All values in js are introduced with "var". Don't see any different types there. But certainly it has types behind the scenes, float, integer, string, etc. Rather than produce type errors it does it's best to coerce anything into anything. Sometimes in bizarre ways.
The propeller manual foregoes 70+ years of nomenclature in an effort to obscure the details of a trivial core within a simple SOC. It is horrifically loose in its description of the operation of the device and the meaning of the Spin language to the point where the operation of either, in many cases, cannot be discerned despite the remarkably number of words used.
This approach is a huge disservice to those with a background in computers, computer architecture, system architecture and language design. It is a travesty in the education for those whose first encounter with computers is via Propeller.
To use that reference as the basis for anything having to do with generally accepted terms in the field of computer architecture or computer science is, expressed gently, questionable.
The meaning of type in the field of computer languages is not up for debate. If you enjoy wikipedia, look here. Your reference to Type Theory is only tertiarily applicable, but even that reference states "Type systems are a programming language feature designed to identify bugs" and Spin has no such mechanism.
You may choose to define things as you wish, but your choice, as with the Propeller Manual, has no bearing on the fields of computer architecture or computer science. It serves as much purpose as claiming this thread is written in greek, for your definition of greek.
Comments
That the front-end, probably the scanner, can interpret floating point notation and encode 32-bit values, does not equate to types by any informed definition of the word.
Consider the following code:
VAR long x byte y PUB start x := 1000001 y := xWhat happens in that last line?i) y gets byte value of 1.
ii) y gets a byte value of 1 and the memory around it is corrupted with the other three bytes of x
ii) Some random other result because a long does not fit in a byte.
iii) The program crashes as you are asking it to do the impossible.
iv) The compilation fails with a type error.
The answer to that question demonstrates that Spin knows about the types of x and y. A long is coerced into a byte.
Things get messy when you are accessing memory through pointers (addresses created with @). Such pointers have no type and you have to take care of it in code.
In the following code I would go as far as to say that the use of "byte[...]" is cast.
VAR long x PUB start incByte(@x) PUB incByte(byteAddr) byte[byteAddr] += byte[byteAddr]Further, both of your recent example demonstrate that Spin has no types. Allow me to explain:
Let's look at your most recent example.
The declaration of y allocates an 8-bit container in the static, per-object-instantiation scope.
The assignment statement at the end of your example first evaluates the right-hand side of the assignment operator and then stores that intermediate value into the address designated by the left-hand side.
The evaluation of expressions in Spin always yields a 32-bit intermediate result.
This particular assignment operator stores into y using y's width of 8-bits. The semantics of assignment in Spin is to discard the upper bits when the container is less than 32-bits.
Were Spin a typed language, this assignment would cause a compilation error because of type mismatch at assignment. This is the essence of types, that operands of one type must be explicitly converted into operands of another type prior to operating upon them.
Similarly, your previous claim that the right-hand side of a constant declaration with literal syntax like 1E3 implies types, suggests that %101 also implies types - neither is remotely true. The syntax of a numeric constant has nothing to do with types.
All numeric literals in Spin are evaluated at compile time to create 32-bit signed values irrespective of whether they are expressed as float, decimal, hexadecimal, octal or binary. Named numbers, those things created with con sections of source code are similarly untyped.
However, for some bizarre reason known only to the authors of the original compiler, the evaluation of operators in the context of con declarations forbids mixing some forms of literal syntax (like 1e3) with other forms of literal syntax (like %101). The absurdity of this is most apparent once one realizes these things can be mixed in a runtime expression. For example:
That the expression in the return statement is legal demonstrates that there are no types. That the same expression is legal in one context and illegal in another suggests that the compiler author/language designer paid no attention to details; we see this throughout the syntax and semantics of Spin, which are haphazard at best. That the expression in the return statement isn't folded at compile time is further indication that the compiler author/language designer had no idea of how to write a compiler. This stuff has all been well understood for more than 40 years.
We seem to have different ideas about what "types" means.
In my example you quite rightly say "This particular assignment operator stores into y using y's width of 8-bits. The semantics of assignment in Spin is to discard the upper bits when the container is less than 32-bits."
That means that the compiler knows that x is a long and y is a byte. It generates different code than if both x and y were longs.
There is nothing in the line "y := x" that indicates doing different things depending on the size of y and x.
Ergo the compiler has to use the type information to generate the right code.
By your very own argument we see that Spin has types.
Our different views on types shows in your statement "Were Spin a typed language, this assignment would cause a compilation error because of type mismatch at assignment. This is the essence of types.."
It is not necessary for a language to produce a compilation error to be said to have types. We can write almost the same code in C and get the same behaviour. No error. C is a typed language is it not?
Our argument should be more refined: Is Spin a "stongly typed" or "strictly typed" language like Ada? Is a "weakly typed" language like C? "Dynamically typed" like Python or Javascript?
There is much debate and confusion about types. For example: http://stackoverflow.com/questions/2690544/what-is-the-difference-between-a-strongly-typed-language-and-a-statically-typed
Seems no one can agree on the terminology much. Bottom line is that I'm sure if we look in the source code of a Spin compiler we will find symbol tables recording the types of variables.
I do agree that Spin is haphazard. Lacking any formal definition as it does. This becomes obvious when you try writing a parser for it.
-Phil
Some terms get so overloaded that no one knows what they mean any more.
Interestingly the Propeller manual has yet another definition of "type" that we have not mentioned:
OBJ
Num : "Numbers"
Term : "TV_Terminal"
This example defines Num as an object symbol of type "Numbers" and Term as an object
symbol of type "TV_Terminal".
Storage size is only pertinent to the implementation operations; usually only load and store. It is not relevant to semantics.
Type is only relevant to semantics; it has no bearing on any operations
That the compiler's implementation refers to the storage size attribute of a declaration as the declaration's type indicates the implementors of the compiler do not understand compilation in the traditional sense. It does not magically transform storage size into type in much the same way that had they called storage size World_Peace, it would not have changed the human condition.
Spin is not typed.
As Phil points out we are just quibbling over the meaning "type" and "typed" in programming languages.
You want a rigorous definition that involves some or all of: type checking, errors on type mismatch, type coercions, casts and so on. This can be carried to extreme, as languages like Ada do. There is a whole formalism for it: https://en.wikipedia.org/wiki/Type_theory
I want to use "type" more loosely, perhaps "storage type" is enough for me. Perhaps syntactically distinct types are enough for me. Spin certainly has those. A floating point value is written in a different way than an integer and is translated into different bit patterns. Even the Propeller manual refers to types.
Would you consider Javascript typed? All values in js are introduced with "var". Don't see any different types there. But certainly it has types behind the scenes, float, integer, string, etc. Rather than produce type errors it does it's best to coerce anything into anything. Sometimes in bizarre ways.
This approach is a huge disservice to those with a background in computers, computer architecture, system architecture and language design. It is a travesty in the education for those whose first encounter with computers is via Propeller.
To use that reference as the basis for anything having to do with generally accepted terms in the field of computer architecture or computer science is, expressed gently, questionable.
The meaning of type in the field of computer languages is not up for debate. If you enjoy wikipedia, look here. Your reference to Type Theory is only tertiarily applicable, but even that reference states "Type systems are a programming language feature designed to identify bugs" and Spin has no such mechanism.
You may choose to define things as you wish, but your choice, as with the Propeller Manual, has no bearing on the fields of computer architecture or computer science. It serves as much purpose as claiming this thread is written in greek, for your definition of greek.
Spin has no types.