# Definition of a type

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?

• You have run directly down one hell of a deep rabbit hole, and it is awesome. Let's see if we can't just enhance your confusion with a couple links: en.wikipedia.org/wiki/Lambda_cube quality read there, and you should really inspect dependant typing because it sounds like you're are striking yourself directly upon it with your talk of listing the possible values within the definition of the type and function etc. I'm not sure I know how to answer your question or if there is a definitive one as much research happens in that space still Nov 26, 2013 at 20:40
• are you asking about computer science theoretical definitions of types, or practical ones? the set of 4 quarters in my pocket is functionally identical to the set of 4 quarters in your pocket, but my quarters are not your quarters, and vice-versa, yet both could be covered by a conceptual type of "my money" or "pocket change" or "collection of metal disks" and so on what constitutes a useful definition of a type depends on what you want to do with it if what you want to do is navel-gaze, check out lambda calculus and category theory ;) Nov 27, 2013 at 3:04

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.

• It's worth noting that many dependently typed languages provide an "out". Where the type system is a little unsound but you can state non-terminating programs. Nov 27, 2013 at 3:33

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.

• Thanks! It's hard for me to understand at this point, but I hope to reread this when I am more comfortable with the concepts you use. BTW, might you perhaps have swapped the "nominal" and "structural" terms? Or I misunderstood their meaning.
– max
Dec 1, 2013 at 9:46
• @max No I didn't. If `Foo` and `Bar` are different types then even if the values they contain are identical they aren't equal. Dec 1, 2013 at 15:51