1. 9

  2. 2

    “Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.”

    I had to stop right there. Most of us in imperative languages using types use them or structure. Especially in terms of structs or objects. This says types have nothing to do with structure. Makes me wonder if that’s inaccurate or type theory doesn’t cover what imperative/OOP programmers normally call types. Or do they have another definition of structure outside the mainstream definition. I have a feeling a certain amount of confusion that happens in type theory discussions might have started right there.

    Regarding the RedPRL prover, one person on it is the person who wrote Practical Foundations for Programming Languages. People might find those interesting by themselves.

    1. 8

      An example of something that structural interpretations of types have trouble with is equality of functions. Many programming languages have a very limited or outright broken notion of function equality, but it’s important if you want to prove a program conforms to a specification. It’s also important to have a language for what function equality means. Are a quicksort and a merge sort equal functions?

      Bob Harper is both the author of this blog post and PFPL.

      1. 3

        Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.

        I took “behaviour” to mean the ‘externally visible’ aspects of a value/program. For example, that something with function type Foo -> Bar can be called with a Foo value to produce a Bar value; that something with product type Foo * Bar can be projected to give both a Foo value and a Bar value; that something with sum type Foo + Bar can be projected to give either a Foo value or a Bar value but not both; etc.

        I took “structure” to mean the ‘internal’ aspects of a value/program. For example, the different parts it may be made out of, any functions/computations that it uses (delayed or already completed), the syntax it was written as, etc.

        In this sense:

        • We can make these “behaviours” as complex and precise as we like, by making the types more complex and precise. For example, with dependent pairs and functions we can encode arbitrarily complicated mathematical relationships between values, inputs/outputs, etc.

        • We can’t use types to classify the “structure” of a value/program.

        As a provocative example, we can think about a value of product type Foo * Bar. We might think that the type tells us some ‘structural’ properties about the value, like “it contains a Foo” and “it contains a Bar”, but that’s not quite right. All we know is the “behaviour”, that we can project the value to get a Foo and a Bar, but we don’t know what will happen during that process. For all we know, the value might be an integer plumbed into an ‘unpairing’ function, like with Cantor pairing or Goedel numbering. Should we say that such a value “contains” a Foo and a Bar? What if that same integer is also used elsewhere to generate a boolean, a list of bitmaps, etc.? We’d at least have to weaken what we think of as “containing” or “structure”.

        One example which I’ve heard discussed about type theory as opposed to set theory, is that in set theory we can (and very often do) ask whether a value is contained in a set, e.g. foo ∈ {foo, bar} and foo ∈ {high, low} are propositions which may be true or false. In type theory we can’t ask whether a value has a particular type, e.g. foo : (Foo * Bar) and foo : (High * Low) aren’t true/false propositions; they’re logical statements, which may be well-typed (valid) or ill-typed (invalid).

        This is important for the “behaviour” vs “structure” distinction, since in set theory we can distinguish between isomorphic sets, e.g. {foo, bar} and {high, low} are isomorphic (they “behave the same”), but the foo ∈ x predicate is true for one and false for the other (they’re structured differently). Since type theory doesn’t let us do this, isomorphic types are indistinguishable (within the theory), so we can only reason about “behaviour”. This has connotations for modularity, reusability, optimisations, etc.

        1. 3

          You’re right that the types discussed in here are not being used in the same way that types in many c likes primarily use them. The goal is essentially different in scope. C types mostly capture the size of memory required for allocation of something. Types in the type theory sense can capture this idea, but can also contain much richer and complicated concepts in the types themselves.

          also aside from PFPL Bob Harper is known for his work on SML and LF

          1. 2

            Yeah I don’t think you can do type theoretic proofs in say C# without a lot of work with interfaces and tuples. After all you don’t even have “Product and Sum types”. Heck it’s even hard right now in F# due to the fact that you have to explicitly name everything.

            So for example say you have a function which takes a tuple of an int and (bool or string) and returns either a tuple of an int and a bool or and int an a string. int * (bool | string) -> (int * bool) | (int * string) //this would be the function signature. More amusingly

            Old * (dumb | fat) -> (Old * dumb) | (Old | fat) // if I’m old and (dumb or fat) this implies I’m either old and dumb or old and fat

            This is equivalent to A ^ (B v C) = (A ^ B) v (A ^ C). in logical propositions.

            we can the write a function which takes an int and either a bool or a string, and return an int and bool, or an int and string and we know we have covered all possible return combinations.

            In this way the function signature, the “Type” represents the lemma and then function itself exists as proof.

            This as I understand it is merely the beginning of the whole thing. There’s a good computerphile video on the subject.