Tim: Frank, is there a known way of expressing nontrivial type isomorphisms in programming languages, where the compiler can either autoderive the isomorphism itself, or let the user express it in such a way that the compiler can verify its validity? This seems like a necessity for what you're looking to do with Arrow.
I'm not sure what you mean by `nontrivial'. If I were to guess, I'd imagine you regard isos like the product associativity and commutativity isos, and the currying iso as trivial, while something like the iso between cartesian and polar coordinate representations is nontrivial. If that is the case, then I have to disappoint you since Arrow only treats the trivial ones, the ones which arise from the type structure itself.
To say it a bit more precisely, Arrow only treats isos which can be expressed as an `equation' on type schemes. The cartesianpolar one is not of this form, since it depends on arithmetic properties of the values involved.
Do you have any concrete examples of writing programs "up to isomorphism"?
I don't have any source code, but I have several applications in mind. One is to do with typesafe embeddings of formal languages. In my previous two papers I talked about a typesafe XML embedding and the latest one motivates using type isos to simplify this. The problem is essentially that when you translate a grammar to a type, you must make a choice about how to parse strings accepted by the grammar, since the values of the type represent parse trees not just strings. However different choices of how to parse the strings lead to isomorphic types. For example, if I have a grammar:
P ::= A B C
I can translate P in a number of ways:
(A,B,C)
((A,B),C)
(A,(B,C))
data P = P (A,B,C)
data P = P A B C
etc. These are all isomorphic. In Arrow you can write one piece of code which can process any/all of them. You can think of that feature as symmetric subtyping. Arrow also supports the more conventional, asymmetric form of subtyping. So, if you want, you can also write code which processes all of the above plus, for example:
data P = P A B C Line Column
There are many other examples which have nothing (on the surface) to do with formal languages and parsing, for example socalled extensible datatypes, differentiation and (I think) something like firstclass polymorphism. More generally, treating types up to isomorphism lets you separate the representation of a datatype from its `interface' or `shape', so it's good for software engineering in general. And (I have yet to prove this but) you get all this with decidable type inference; no type annotations needed, ever, unless you explicitly use a facility that requires nontrivial type equality like dependent types.
Right now things are going extremely well, so if you give me another month I think I will have actual source code (in the core language) to show you, as I hope to get a paper done in time for POPL. (Wishful thinking, but...)
For example, a monad's unit is only determinable from the monad's functor up to unique isomorphism. For example, with the Haskell list monad, three potential units are (x::t)>[] and (x::t)>(x::[]) and (x::t)>(x::x::[]).
I guess I don't understand you. None of these is the unit for what I understand as the list monad. The list monad's unit is a polymorphic function of type forall a. a > [a], and it's defined as x > x:[] (in Haskell syntax). Other functions typeable at instances of this type, like forall a. [a] > [[a]], are not the unit for the list monad, but rather a different monad, if any.
In any case, I don't quite know how inductive datatypes will work yet, but I don't think Arrow will try to guess at how to turn a particular functor into a monads.
Can you program with lists in a way that is generic with respect to list unit? Does the trivial case of [] tell us anything new about list programming? Does the fact that "doubleconsed" lists can't be exactly typed in most languages prevent this approach from working?
Again, I don't understand what you mean... and what is a `doubleconsed' list?
What I can tell you is that you will be able to write code which works for both cons and snoc lists, for example.
Actually I think there will be a sequence datatype, corresponding to the Kleene star. This will have the structure of a monad, and it will be builtin, and probably all inductive datatypes will factor through it.
