Dear Anthony, you asked a detail question, so I'll give a detailed answer. This may not be of interest to all the readers of this list, so I hope people will feel free to skip this message. As I mentioned, the application is a bit minor (but nevertheless fun). Suppose in Haskell (or another functional programming language), you need to define a data type F(X) that is parametric (often functorial) on another type X. One basic example is that of lists: data List x = Nil | Cons x (List x) For those not familiar with Haskell syntax, this simply corresponds to the categorical equation List(X) ~= 1 + X x List(X), which can be solved by taking an initial algebra of the functor F(A) = 1 + X x A. There are two constructors "Nil" and "Cons". Now suppose that, for some reason, we need a third constructor "Third", but we want that constructor to be available *only* when X is equal to some particular type X_0. In other words, we want: data List x = Nil | Cons x (List x) { when x is not x0 } data List x = Nil | Cons x (List x) | Third x { when x is x0 } It is of course not possible in Haskell to define a polymorphic type by case distinction like this. We could get around it by defining data List x = Nil | Cons x (List x) | Third x for all x, and making it a *convention* that the third constructor is only going to be used when x = x0. However, this does not work well, because many reasonable programs will not type-check. The problem arises when one needs to define a function from List x to some other type by case distinction. When it comes to the third case, the type checker cannot prove that x = x0, and in general, it may not be possible to define the desired function so that it works for arbitrary x. The solution is to define an identity type data Identity a b = Identity (a->b, b->a) and four functions reflexivity :: Identity a a symmetry :: Identity a b -> Identity b a transitivity :: Identity a b -> Identity b c -> Identity a c identity :: Identity a b -> a -> b. (And we make sure that no additional primitive functions of this type can be defined, for example by making it an abstract type). Then we can define data List x = Nil | Cons x (List x) | Third (Identity x x0) x And this does exactly the right thing. When it comes to doing a case distinction on the type List x, in the third case, we can actually *prove* that x is equal to x0, because the identity type contains a witness of this fact. The specific thing we needed this for in Quipper is in our library for arithmetic with fixed-but-arbitrary length quantum integers. We needed a type Int(X) representing integers in fixed-length binary notation, but using elements of the type X instead of the usual {0,1} as the digits. This gives us, for example, a type Int(Bool) of classical integers, and a type Int(Qubit) of quantum integers. Working with fixed-length integers is sometimes a bit tedious, because when you write an arithmetic expression such as 0 + a, you need to first specify what the length of 0 is, and then it needs to match the length of a. In order to infer this kind of information automatically, we added an alternative to the type Int(Bool), where one could store an ordinary integer (not yet specialized to a particular number of digits). However, this was only going to work for Int(Bool) and not, e.g., for Int(Qubit). So we used the above trick to do it. (Before starting a long discussion, I should add that we are of course aware that there are other ways of dealing with fixed-but-arbitrary length integers in Haskell, for example, by using type-level integers to parameterize a type Int(n) of n-bit integers. The above is just one particular example of something we did; I'm not saying that it is the only or even the best way to do it). -- Peter Anthony Bordg wrote:
Hi,
can you describe the application of identity types from type theory that you found ?
Best wishes
Anthony
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]