4 ms·

Over many years of reading various essays on "types", this is the list of synonyms I've accumulated: ="constraints" ="rules" ="policies" ="contracts" ="sem

by jasode 11y ago

Over many years of reading various essays on "types", this is the list of synonyms I've accumulated: ="constraints" ="rules" ="policies" ="contracts" ="semantics" (separate concept of MEANING from underlying DATA BIT representations) ="compatible semantics" ="capabilities" ="propositions" (and functions can be "theorem proofs") ="facts" about code that compiler attempts to "prove" ="tags" or "metatags" for compiler checking ="documentation" that's enforced by compiler specify what is NOT ALLOWED e.g. "you can't do that" ="substitution", "compatibility" ="A set of rules for how to semantically treat a region of memory." Because the list is synonyms, many concepts overlap. In my mind, the highest level of unification about "types" is the concept of "constraints". Related topics such as polymorphism is a practical syntax pattern that arises from data types' constraints. Personal anecdote: I initially learned an incomplete and misleading idea about "types" from K&R's "The C Programming Language". From that book, I thought of "types" as different data widths (or magnitudes). An "int" held 16bits and a "long" held 32 bits, etc. It was later exposure to more sophisticated programming languages that a much richer expressiveness of "types" is possible that the C Language "typedef" cannot accomplish. For instance, if want a "type" called "month", I could encode a "rule" or "constraint" that valid values are 0 through 11 (or 1 to 12). A plain "int" is -32768..+32767 and having "typedef int month;" provides a synonym but not a new policy enforceable by the compiler.

yarvin9 11y ago
Urbit actually wound up with three different concepts which all want the word "type," and can't all have it. Worse, none of these quite matches the PL-theory meaning. So none of them wound up with the word. One easy way to state a type is to state it as the range of a function. The function accepts all values, and produces some subset of all values; ideally, all values in its range are fixpoints, f(x) == f(f(x)). This is kind of nice because you've defined both a constraint and a validation function. We often want to validate untyped data and make it typed. On the other hand, this range (Urbit's "span") is not the same concept as the function itself (Urbit's "mold"). Moreover, when you send data over the network, you don't want to send the range or even the function; you want to send the name of the function, which hopefully is bound to something compatible on the other side. This namespace becomes a third level of type (Urbit's "mark"): like a MIME type, if a MIME type was an executable specification. One of the problems with most PL type systems is that they predate ubiquitous networking; so they're not designed to address the problem of describing external data, eg with MIME types, XML DTDs, protobuf schemas or whatever.
- wyager 11y ago
  No offense, but this is exactly the sort of nonsense I associate with urbit. >ideally, all values in its range are fixpoints, f(x) == f(f(x)). This doesn't make any sense whatsoever. The only function for which this is true is identity, and I assure you it takes more than just the identity function to make a useful program. This isn't even possible unless the function has the type "a -> a". The only other thing I can see you trying to express here is some butchery of set notation, where by f(x) you actually mean {f(x) | forall x of the correct type}. Even then, what you're saying is still completely nonsensical. I honestly cannot tell if urbit is some sort of coordinated trolling effort.
  - tel 11y ago
    Identity is not the only function for which that holds. As an immediate example, constant functions have this property as well. More interesting examples exist as well. Also what was stated was not an equation for any old fixed point but instead idempotence—a specific kind of fixed point. In particular, this describes precisely the shape of a "validation" function so long as it either succeeds on all inputs or has a notion of failure in either its computational context or it's range ("span" I guess).
    - dllthomas 11y ago
      'a "validation" function' Or "normalization"
      - yarvin9 11y ago
        Yeah, that's exactly right. I usually say "normalization."
  - yarvin9 11y ago
    To be slightly clearer, the values here are Urbit "nouns." A noun is an atom or a cell. An atom is an unsigned integer of any size. A cell is an ordered pair of nouns. I am fairly confident that many useful sets can be specified as the fixpoint set of a function in this space.

by jasode 11y ago

yarvin9 11y ago

Urbit actually wound up with three different concepts which all want the word "type," and can't all have it. Worse, none of these quite matches the PL-theory meaning. So none of them wound up with the word. One easy way to state a type is to state it as the range of a function. The function accepts all values, and produces some subset of all values; ideally, all values in its range are fixpoints, f(x) == f(f(x)). This is kind of nice because you've defined both a constraint and a validation function. We often want to validate untyped data and make it typed. On the other hand, this range (Urbit's "span") is not the same concept as the function itself (Urbit's "mold"). Moreover, when you send data over the network, you don't want to send the range or even the function; you want to send the name of the function, which hopefully is bound to something compatible on the other side. This namespace becomes a third level of type (Urbit's "mark"): like a MIME type, if a MIME type was an executable specification. One of the problems with most PL type systems is that they predate ubiquitous networking; so they're not designed to address the problem of describing external data, eg with MIME types, XML DTDs, protobuf schemas or whatever.

wyager 11y ago
No offense, but this is exactly the sort of nonsense I associate with urbit. >ideally, all values in its range are fixpoints, f(x) == f(f(x)). This doesn't make any sense whatsoever. The only function for which this is true is identity, and I assure you it takes more than just the identity function to make a useful program. This isn't even possible unless the function has the type "a -> a". The only other thing I can see you trying to express here is some butchery of set notation, where by f(x) you actually mean {f(x) | forall x of the correct type}. Even then, what you're saying is still completely nonsensical. I honestly cannot tell if urbit is some sort of coordinated trolling effort.
- tel 11y ago
  Identity is not the only function for which that holds. As an immediate example, constant functions have this property as well. More interesting examples exist as well. Also what was stated was not an equation for any old fixed point but instead idempotence—a specific kind of fixed point. In particular, this describes precisely the shape of a "validation" function so long as it either succeeds on all inputs or has a notion of failure in either its computational context or it's range ("span" I guess).
  - dllthomas 11y ago
    'a "validation" function' Or "normalization"
    - yarvin9 11y ago
      Yeah, that's exactly right. I usually say "normalization."
- yarvin9 11y ago
  To be slightly clearer, the values here are Urbit "nouns." A noun is an atom or a cell. An atom is an unsigned integer of any size. A cell is an ordered pair of nouns. I am fairly confident that many useful sets can be specified as the fixpoint set of a function in this space.