Which type?
Will you have only one numeric type, or various numeric types?
I know you said you did not seek an answer, but I thought I might respond anyway, as to me (at least) the answer is obvious. I would have all the number values that are useful (and that are numbers). So, I would have all the integers, all the non-integer rationals, all the "constructible" reals (for some specification of constructing reals). I would have the (constructible) imaginary numbers and (I guess) quaternions and any other "respectable" numbers that mathematicians find useful. All these sets are obviously infinite, so some system of costing would also be needed to avoid users from racking up too much compute cost when asking for expressions to be evaluated. I would have named sets for these values, so the set of Rationals that is the union of the set of integers and the set of non-integer rationals. etc. I would probably put all such sets in a set named type. I might have another set called "domains" that contains named sets of all function input and output sets. Still, none of that implies that values "implicitly have a type"
P.S. I would have an "integer division" function (I think it is a useful function). It would just need a name that distinguishes it from (proper) division. (happy to have suggestions for such a name (and/or symbol))
P.P.S. I would also have non-number values that nevertheless act very much like number values. Example might be 10 kg or 10.00 or £10
Quote from Dave Voorhis on November 14, 2021, 7:35 pmQuote from Paul Vernon on November 14, 2021, 7:08 pmP.S. Is the TTM definition of scalar value and type not dangerously circular? A type is a named, finite set of scalar values. A scalar value carries with it its type. Which comes first, the type chicken or the value egg?
They are co-defined. A type is a set of values; a value is a member of a type. Consider them together.
I googled "co-defined". I did not get a good hit. Is it a thing? I can't see how you break the recursion even if you "consider them together".
What I can see is that if a value is defined first (without a type), you can then add it to a type afterwards. But I can't see it otherwise.
It afflicts the definition of a set too. I.e. If a set is a collection of atoms and sets; atoms have at least one type; a type is a set of atoms. I don't see how you break the infinite loop.
Maybe post a BNF?!
Quote from Paul Vernon on November 14, 2021, 8:47 pmI'm not saying that I would not have types. I mean, named set of values such as the set of integers, the set of evens, the set of primes are all very useful sets, certainly worth naming them and using them for constraints, or to guaranteeing that applying a function to a value that is known to be a member of such a set will return a result rather than empty. Such sets I might well call "types" for want of a better word (such as say domain)
What I'm saying is that values are not intrinsically typed - they they don't "carry their type(s) with them". I'm saying that types are not axiomatic. They are not foundational.
There is an important difference (a logical difference, as D&D would say) between the above two positions.
Values must be intrinsically typed in computer languages, even if it's the programmer who keeps track of the types rather than the computer, as is done in FORTH and machine language and some assembly languages.
Of course it's possible to have values outside computer systems that are untyped. Here's one now:
Guvf vf abg rapbqrq
But it's not very meaningful without knowing its type (except as type "gibberish", perhaps.) But if I tell you that its type is "ROT13 encoded string", then you can handle it meaningfully.
Quote from Paul Vernon on November 14, 2021, 10:30 pmQuote from Dave Voorhis on November 14, 2021, 7:35 pmQuote from Paul Vernon on November 14, 2021, 7:08 pmP.S. Is the TTM definition of scalar value and type not dangerously circular? A type is a named, finite set of scalar values. A scalar value carries with it its type. Which comes first, the type chicken or the value egg?
They are co-defined. A type is a set of values; a value is a member of a type. Consider them together.
I googled "co-defined". I did not get a good hit. Is it a thing? I can't see how you break the recursion even if you "consider them together".
What I can see is that if a value is defined first (without a type), you can then add it to a type afterwards. But I can't see it otherwise.
It afflicts the definition of a set too. I.e. If a set is a collection of atoms and sets; atoms have at least one type; a type is a set of atoms. I don't see how you break the infinite loop.
Maybe post a BNF?!
"Co-defined" simply means defined together. Computational systems often have self-referential or recursive definitions. Conceptually, they are no more a problem than, say, considering which came first, individual persons or families. Or, set S consists of members {a, b, c}. S is defined in terms of a, b, and c. The elements a, b, and c are only meaningful in terms of S.
Quote from Paul Vernon on November 14, 2021, 10:30 pmQuote from Dave Voorhis on November 14, 2021, 7:35 pmQuote from Paul Vernon on November 14, 2021, 7:08 pmP.S. Is the TTM definition of scalar value and type not dangerously circular? A type is a named, finite set of scalar values. A scalar value carries with it its type. Which comes first, the type chicken or the value egg?
They are co-defined. A type is a set of values; a value is a member of a type. Consider them together.
I googled "co-defined". I did not get a good hit.
Prefix 'co-' is in my dictionary fine. "Taken in English from 17c. as a living prefix meaning "together, mutually, in common," and used promiscuously with native words (co-worker) and Latin-derived words not beginning with vowels (codependent), including some already having it (co-conspirator)." 'living prefix ... promiscuously' means you can stick 'co-' in front of any word, it hasn't become ossified to only fixed forms.
'co-defined' = defined together, defined mutually, defined in common.
Is it a thing? I can't see how you break the recursion even if you "consider them together".
Consider a circle, its circumference and its radius. Can you have a circle without a radius? Or without a circumference? Can you have a circumference without a circle? Try defining any one of those ex nihilo without in effect defining the other two; they're co-defined.
What I can see is that if a value is defined first (without a type), you can then add it to a type afterwards. But I can't see it otherwise.
It afflicts the definition of a set too. I.e. If a set is a collection of atoms and sets; atoms have at least one type; a type is a set of atoms.
Not every arbitrary collection of atoms is a type. Even if you presume the atoms exist logically prior to the type (I don't); and you stipulate all atoms are to belong to some type or other; that doesn't mean you can just bundle atom 1 with atom 'h' and form a type. You're going to define the type with some notion of criterion for membership, you're thereby co-defining which atoms belong to the type -- and just as important, which atoms are excluded from that type.
I don't see how you break the infinite loop.
Maybe post a BNF?!
topdecl → data [context =>] simpletype [= constrs]
simpletype → tycon tyvar1 ... tyvark
constrs → constr1 | ... | constrn
constr → con [!] atype1 ... [!] atypek
| -- and stuff
This is from the Haskell language report 2010; but it's close enough to Idris you should be able to recognise it. italics for non-terminals; code style for keywords/terminals data, |; '...' for repeated elements; '[ ]' for optional. For example
data Bool = False | True
co-defines values False, True as elements of type Bool.
Re your other terminological obfuscations: 'domain' is a word I'd avoid -- at least without qualifying it. Codd 1970 used 'domain' for what these days I think we'd call 'type'. But at the time, 'type' in programming language usage was very much tied to machine representation (what D&D call 'PhysRep'), and Codd was quite right to avoid it. In function theory, 'domain' is relative to a function/operator: you might say the domain of most numeric operations (plus, times, minus) is any numeric type; but the domain of division is only floating-point or rational types; with a different operation (div ?) for dividing integer type(s), with truncation.
Quote from Paul Vernon on November 10, 2021, 1:26 pmIn other words, why must values carry with them a type? (Why can't they just be)
If we can have "safety" without axiomatic types, then types can just be any old (named) sets of values, rather than something foundational
And who gets to define these types anyway? Why is the prime numbers (to pick one example) not a type (or is it :-)?
I agree, probably. The way I look at it is every value is a singleton constant, and every type is just a set of those values, full stop. Everything else flows from that.
Quote from AntC on November 15, 2021, 4:13 amConsider a circle, its circumference and its radius. Can you have a circle without a radius? Or without a circumference? Can you have a circumference without a circle? Try defining any one of those ex nihilo without in effect defining the other two; they're co-defined.
That is not quite the right analogy. To my mind it would be: A circle is a circumference and a radius; A circumference is defined axiomatically; A radius is a circle.
That can only define me an infinite circle of never ending circles.
For example, If I try to use this BNF
set -> "{" element_list "}" | "{" "}"element_list -> element_list "," element | elementelement -> set | atomatom -> literal ":" typetype -> setliteral -> "1" |"2" | "3"
Then the only atoms I can define are infinite atoms such as
1:{1:{1:{1:{1:
I.e. I can never find an input string to which my parser does not say "Unexpected end of input".
Well, that is not quite true. I can define an atom such as
1:{1:{1:{1:{1:{}}}}}
or, more simply
1:{}
But then you can only have "the empty set" (or the set containing the empty set, or the set containing the set containing the empty set ...) as valid types.
(I was worried that maybe "co-definition" was some some magic thing that I'ld not heard of that can turn something infinite into something finite. It appears to be no such thing)
Quote from Paul Vernon on November 15, 2021, 10:24 amQuote from AntC on November 15, 2021, 4:13 amConsider a circle, its circumference and its radius. Can you have a circle without a radius? Or without a circumference? Can you have a circumference without a circle? Try defining any one of those ex nihilo without in effect defining the other two; they're co-defined.
That is not quite the right analogy. To my mind it would be: A circle is a circumference and a radius; A circumference is defined axiomatically; A radius is a circle.
That can only define me an infinite circle of never ending circles.
For example, If I try to use this BNF
set -> "{" element_list "}" | "{" "}"element_list -> element_list "," element | elementelement -> set | atomatom -> literal ":" typetype -> setliteral -> "1" |"2" | "3"
Yes, that kind of definition leads to infinite regress. You need an exit from the recursion, like -- for example -- defining 'true' and 'false' as axiomatic or implicit members of a boolean type. Thus you might say the above, but change the atom rule to:
atom -> literal ":" type | "true" | "false"
Quote from Darren Duncan on November 15, 2021, 5:26 amI agree, probably.
OK, So scores on the doors...
The No camp: 3
The Yes camp: 2
The It Depends camp: 1
So, the noes have it, the noes have it, unlock
(OK, so probably I should have placed David in both the No and the It Depends camp as he gave two answers. But then it would have been a score draw :-)
Quote from Dave Voorhis on November 15, 2021, 10:40 amQuote from Paul Vernon on November 15, 2021, 10:24 amQuote from AntC on November 15, 2021, 4:13 amConsider a circle, its circumference and its radius. Can you have a circle without a radius? Or without a circumference? Can you have a circumference without a circle? Try defining any one of those ex nihilo without in effect defining the other two; they're co-defined.
That is not quite the right analogy. To my mind it would be: A circle is a circumference and a radius; A circumference is defined axiomatically; A radius is a circle.
That can only define me an infinite circle of never ending circles.
For example, If I try to use this BNF
set -> "{" element_list "}" | "{" "}"element_list -> element_list "," element | elementelement -> set | atomatom -> literal ":" typetype -> setliteral -> "1" |"2" | "3"Yes, that kind of definition leads to infinite regress. You need an exit from the recursion, like -- for example -- defining 'true' and 'false' as axiomatic or implicit members of a boolean type. Thus you might say the above, but change the atom rule to:
atom -> literal ":" type | "true" | "false"
Agreed.
You need at (at least some) atoms to have their type defined axiomatically.
So do we have two types of type? One axiomatic, one not. I'm not sure I like that. I'm not sure picking (oh, say 9 types) as the axiomatic ones is a good idea.
How do we choose which ones should be axiomatic? Likely some minimal, plausible set. Maybe like the Von_Neumann_ordinals the empty set would suffice. Maybe just two bits. Humm.
Aside. I wonder if an "axiomatic TTM" would be a good thing to define (for those that think that TTM is (give or take) the right answer (to some question)) or do you think that as currently written TTM it is all but axiomatic anyway, even if not structured in the traditional mathematical sense of axioms, theorems and corollaries (and hence it would be wasted effort) ?