="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.

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.

The problem existed before "ubiquitous networking" if you realise that networking is just a specific kind of I/O. But I/O from a PL perspective is nothing more than sending or receiving bytes. PLs usually do not impose a format and a meaning on I/O because it would restrict the capabilities of the applications and libraries.

One could argue that PLs should impose such restrictions just like some PLs impose restrictions on memory access ("managed languages"). However, a huge difference between memory and I/O - and especially networking - is that they are unreliable by default: transmission errors, disconnections, lags, etc.

But even if you solve that, your PL can only speak to itself, which quite significantly restricts its practical usefulness. As far as I know, only languages specialized in distributed computing do that.

But for a general purpose language, high level networking is usually not something you want to be carved in stone (in the language's specs). You'd rather want to leave that in libraries, that can be replaced and enhanced.

Urbit is very happy to be an HTTP client and server. (Alas, HTTP has become the "everything protocol.") It also has its own network protocol, which it prefers for conversations between urbits.

The unreliability of network packet delivery (or more exactly, the unreasonable effectiveness of unreliable networking) is basically the greatest technical idea of the 20th century as far as I'm concerned.

There is actually a significant difference between processing unordered, unreliable packet streams, and ordered, reliable, message streams, with the "universal design." Neat thing about packets: you can drop them. If a packet sends the server into an infinite loop? Or at least, a timer detects an infinite loop? Drop the packet. From the network's perspective, the CPU is simply detecting congestion.

You can refuse to process a message, but that's not a stateless and passive operation; you have to return a failure report. But dropping a bad packet is the most wonderful thing in the world. By definition it doesn't change your server's state. It also doesn't leak information to the sender...

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

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

Or "normalization"

Any projection suffices.

If you want to clamp a value to some arbitrary range (a hint to the name), then any function that does so has this property.

    unsigned char f(unsigned long x) { return x & 255; }
    long f(long x) { return x < 0 ? x : -x; }

Put it this way: f(f(x)) never makes sense for those definitions of f; it would always indicate a programming error. And so the type system ought to prevent it.

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.

1. Specification of constraints on data - the function arguments and return values. This corresponds to usage of types in logic. The goal here is the correctness of the program (and ease of reasoning about it).

2. A way to define polymorphic functions, i.e. functions that do the same or similar operations with different kinds of data. Here we classify data as of some type so that we can define two functions with the same name, but different types, where the correct one is selected either during compilation or run time based on the parameter type. The goal is conciseness, to avoid explicit conditional statements everywhere or other ways of code duplication.

3. Finally, to specify way how the computer is to store data, or generally how to model abstract concepts (such as integers) within the computer. This becomes less relevant with time (as languages increase in abstraction), but is important use historically. For example, integers that can be modeled with many different types in C. The goal here is to have type as a reference to concrete and efficient representation of the abstract concept.

I think this is pretty much what the paper is suggesting, although IMHO not so clearly.

What I would say perhaps is that #2 and #3 are in a way complementary. In 2, we describe a common operation with a more abstract type, while in 3, we describe the specific representation with a more concrete type. So both #2 and #3 address issues of naming things on different levels of abstraction, which aren't directly related to the program specification or its correctness (use #1).

I think the distinction is that #3b-types, which denote the "encoding" of a value, mapping it to its meaning, are often used as a basis for a #2-types system (to parametrize operations).

I disagree - at least in machine code, the instruction code determines the type of the operands. If they were to be polymorphic, the type of operands would determine the specific instructions that are to be used (and so you could for example reuse the same code for different word lengths). Maybe modern assemblers can do that (and have a generic instruction name for addition, for example), it's been 20 years since I programmed in x86, I only recently used mainframe assembler where it is as I describe.

Polymorphism is all about names. You want the same name (and by extension, the same code) to refer to potentially different operations on data.

> I think the distinction is that #3b-types

I am still not sure how it is different from #3a in your definition. When I say 16-bit signed integer, I can also mean this as an encoding of abstract "integer number". The whole point of declaring type in sense of #3 is to be specific about encoding. In mathematics, you (typically) don't care about that; but you sometimes care about use case #2, which is typically dealt by mapping to more abstract concepts with some morphism.

http://dl.acm.org/citation.cfm?id=2661154

There was a good blog post by Stephen Kell that I can't find now (https://www.cl.cam.ac.uk/~srk31/blog/)

"The concept of "type" has been used without a consistent, precise definition in discussions about programming languages for 60 years. In this essay I explore various concepts lurking behind distinct uses of this word, highlighting two traditions in which the word came into use largely independently: engineering traditions on the one hand, and those of symbolic logic on the other. These traditions are founded on differing attitudes to the nature and purpose of abstraction, but their distinct uses of "type" have never been explicitly unified. One result is that discourse across these traditions often finds itself at cross purposes, such as overapplying one sense of "type" where another is appropriate, and occasionally proceeding to draw wrong conclusions. I illustrate this with examples from well-known and justly well-regarded literature, and argue that ongoing developments in both the theory and practice of programming make now a good time to resolve these problems."

For most of my life, I equated types with sets of values, but after learning Haskell and working with higher-kinded types, type classes, and existential types, I realized I don't know anymore what a type _is_. I know that type systems provide proof that certain classes of operations are impossible (like comparing a number to a string, or dereferencing an invalid reference).

It's pretty mindbending to use existentials or GADTs and pull two values of a record and not know anything about those values except that, for example, they can be compared for equality.

  data HasTwoEq = forall a. Eq a => HasTwoEq a a

  equalOrNot :: HasTwoEq -> Bool
  equalOrNot (HasTwoEq x y) = x == y

That's not the kind of thing you can express with, say, Java or Go interfaces, but it makes perfect sense once you start to break down the mental walls you've built in your head over the years.

I'm thrilled to see a growing body of accessible* PL and type theory literature, because these things are important to helping us develop software at increasingly large scales, and it's clear that very few people -- including myself! -- know enough about this topic.

* e.g. https://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-0...

I tried to do my part here: http://chadaustin.me/2015/07/sum-types/ and http://chadaustin.me/2015/09/haskell-is-not-a-purely-functio...

Perhaps what you're pointing out is that there are many dynamic and static ways to verify assertions about programs? Certainly.

When programmers talk about "type systems" I think they tend to mean a static, sound, computable approach to verifying assertions about programs.

JIF is a _type system_, albeit not a unification-based one like ML. Moreover, the situations the GP is discussing seem like things that don't need the powerful type system of JIF. Something like ML could handle those situations with ease.

I think contract often takes one of two meanings among non-researchers. Either people are referring to assertions that are dynamically checked or they're referring to very expressive assertions (regardless of when they're checked).

These are all different ways of proving statements about programs.

I've always considered the primary purpose of type systems to be restricting how data can flow through a program.

See also "A Perspective on Information-Flow Control": http://www.cse.chalmers.se/~andrei/mod11.pdf

It seems like modeling data flow via messages would be pretty natural semantics for something like this. But first I need to dig into what Hoare logic is and how it applies.

Therefore, I am also a bit dubious about IFC. It seems to me that Data Flow Analysis is more suitable.

We are essentially hinting at the same thing I guess, but I expect some type system tie-ins. Otherwise it might become too abstract.

Now, I don't actually know much about type theory at all and came here to try to remove some of my ignorance. As such, I can't really help you much, but I will try my best. You might want to look at: https://en.wikipedia.org/wiki/Type_theory

If I read it correctly (and if it is written correctly), a "term" is essentially anything with a "type". So 1, 2 and 3 are terms and they have a type. A "function" is something that takes terms and "reduces" them to other terms. You can "apply" a function to some arguments in order to reduce them. So if we have a function, "myfunc x", we can apply that to 2 and have "myfunc 2". Both "myfunc x" and "myfunc 2" are terms, but they have different types.

Let's make a function that doubles an integer (let's call the type "int"). So "double x" is a term with a type of "int -> int": it maps an int onto an int. "double 2" is a term with a type of int. The term "double double 1" can be "reduced" to the term "double 2". "double 2" can be "reduced" to the term "4". 4 is known as a "normalized term". It can not be reduced any further.

Now, you may be saying "How is this different from what I said?" From what I can tell, the main difference is that a type is not a set of "values" (or normalized terms). Functions applied to terms also have a type. Functions with free variables also have a type. Anything that is a term in an expression has a type. So 1, 2 and 4 are of type int. "double 1", "double 2", and "double double 1" are also all of type int. If we had a function called "fortytwo" that just returned 42, it would also be of type int.

It may seem like a small (possibly insignificant) difference, but it really depends on your point of view. We can completely ignore the type if we want to. Many programming languages make that very easy. We could also subscribe to the idea that a type is just a set of values, like you said. We can write many fine (and many not-so-fine) programs with that point of view.

These views limit the kind of analysis we can do on the code that is written, though. The point of using type theory in computer languages is to help us reason about the code analytically. So my answer to your (unasked) question is, it doesn't have to be complicated. It proves useful to include all of the nuances that type theory gives us. Intentionally putting blinders on to make it seem simple, just deprives us of potentially useful capabilities.

Hopefully someone who actually knows something about this topic will chime in and correct whatever horrible mistakes I've made.

> Functions applied to terms also have a type.

Yes, and those types are sets of values. For example, "int -> int" is the set of all functions that map integers to integers. (Remember that functions are also values, just like any other value, in functional programming.)