Definition of a type

Question

Conceptually, I used to think of types as sets. However, I think I've seen people wishing to distinguish types A, B even if they represent identical collections of values. So I figured a better definition of type is a pair (type_name, set), where two different types cannot have the same first element.

Then I ran into a different situation. I thought a function is just a set of pairs (x, y). But then a function A->B (where A, B represent the same collections of values) cannot be distinguished from a function B->B or A->A or B->A, and again I think I've seen people want to distinguish them. So how do I define a function? As a tuple (A, B, (x1, y1), (x2, y2), ...), where each element of A appears exactly once as the first element in the pairs, and where each second element is of type B?

And the type F that represents all functions that takes A->B is then (F, ((A, B, (a1, b11), (a2, b12), ...), (A, B, (a1, b21), (a2, b22), ...), (A, B, (a1, b31), (a2, b32), ...))), where a1, ... are all the values represented by A, and b?1, b?2, ..., for any ?, are some of the values represented by B.

This all seems rather cumbersome, am I missing something?

Answer 1

I think your real struggle here is one with decidability, which is totally understandable in this context so let's talk about that for a moment.

Your first mention of a type system is quite simple, essentially you have a set and everything in that set represents it's type. Now what type each one of these elements in is unfortunately undecidable because they're just free standing values at this point. This kind of hampers the whole purpose of a type system and is really more indicative of an untyped system. This is similar to the untyped lambda calculus where there are sets but no identifier tied together with values to delineate their enclosing set.

So you realized this undecidability, and decided a solution that makes sense: tie the value to an alias that identifies it's enclosing set as it's "type" so you have every value as a tuple (type, value). This is very similar to the lambda-mu calculus which is effectively an extension to the aforementioned untyped lambda calculus above (or it might be closer to simply typed lambda calculus correct me if I got these mixed up). However ah; there's a catch there, again which type is tied to an input and output set for a function is undecidable in some situations.

So another refinement you decide, alright I'll dictate the input and output types and possible elements at in my function! Aha! Now we've made the determination of types quite decidable! Though it feels like a lot of cruft, and we now require recursive type definitions on all abstracting types to continue building pieces of pieces here, this feels a little messy and burdensome no? Well, yes, it is. Unfortunately this is just how that works, and now you have entered Dependant Typing.

The burdensomeness speaks to one of the reasons implementations of this type system are so rare. However there's another catch to this type system and it's a doozy: As yet it's unknown how to make a truly totality checked (this is the checking you get to do when you make your type system decidable which is what you seem to be after) type system which can be turing complete. The problem is that when you make it totality checked, all possible inputs and outputs are guaranteed by the compiler which means we now have decidability of the programs termination, thus no halting problem which is necessary for turing completeness.

Many non-turing complete languages are still very useful so this is not a necessity, and these types of languages are often used for proof assistants where the code dictates a bunch of input and output possibilities and the compilation itself basically says "Yes, this is a valid logical system." thus proving whatever the code declared.

Answer 2

Because someone has to, I'll approach this from a more mathematical perspective. Types do indeed resemble sets, but it's more pleasant to think of them "nominally" rather than "structurally".

This essentially means that a : Foo /= a : Bar.

Now with this in mind, we can think of types as sets, but this is rather difficult to talk about since sets are often viewed structurally. Things get interesting when we consider these as objects of a category. Then total functions between types (a function that is never undefined) form arrows in this category. I'll refer to this category as STLC.

The set of specialized identity functions (id :: Foo -> Foo...) forms the identity arrow and function composition f . g == f (g x) forms composition. Now that we have a category, it's pleasant to think of other category theoretic concepts, the two interesting ones are products and exponentials.

For products we consider 3 operations

cross  : A -> B -> A X B
first  : A X B  -> A
second : A X B  -> B

So we notice that tuples form products in STLC.

Next consider exponentials. These form the interesting backbone of higher order functions. We want 2 functions for some arrow f : A X B -> C

curry(f) : A X B   -> C^B
eval(f)  : C^B X B -> C

This formalizes the notion behind higher order functions, they are the exponentials of STLC. So a function

f : A -> (B -> C)

Is really an arrow from A to the exponential C^B.

There is a unique arrow to every type from the falsy type. This is a type with no witnesses of any kind. In Haskell

data Falsy =

Last but not least, consider a terminal object T. This is trivially formed by a type with exactly one witness. Traditionally this is called Unit, or True. In Haskell

data Unit = Unit

With these, we can actually state what the representation of a value is, it is a "point" (an arrow from Unit -> A). In a sane type system, the category it forms is well-pointed. Or, there are exactly enough arrows from p : Unit -> A so that if for all p, f . p = g . p, then f = g.

The category I've outlined here describes the type systems of Haskell, ML, and most other mainstream languages.

So as a direct answer to your question. A type is an object of a closed cartesian category with the initial and terminal objects being curry-howard False and True respectively, function values forming expontentials as well as arrows and pairs forming products.