Programming based on category theory

[gmhwxi]

Happy New Year!

Recently, I have got interested in doing some programming in ATS based on category theory.
It is a lot of fun, and it is certainly a very good way of learning category theory. I see that a lot
of people in the Haskell community are deeply into this sort of thing.

Here are two interesting examples I did by essentially rewriting Haskell code in ATS:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/YonedaLemma.dats
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/CoYonedaLemma.dats

So this style of programming based on category theory can indeed be done in ATS. The syntax
for type annotation in ATS can actually offer great help in locating source of type-errors.

What is missing in ATS right now is the ability to synthesize an argument according to the type
of the argument. For instance, when we use Yoneda_psi (which is called runYoneda in Haskell), we
need to pass explicitly the argument functor_list0 of the type functor(list0):

Yoneda_psi (functor_list0) (...)

However, there is exactly one value of the type functor(list0); so we should be able to synthesize
this value solely based on its type. In Haskell, this is handled by the type-class mechanism.

Cheers!

--Hongwei

[Brandon Barker]

My (likely incorrect) understanding from theory is that type families are required for dependent types, or are even synonymous with dependent types. When you said " the ability to synthesize an argument according to the type
of the argument", it sounds like a type family. And ATS has support for dependent types, but maybe it is too restricted for this?

[gmhwxi]

What I had in mind is proof search.

Given a type, which represents a theorem, synthesizing an argument
of the type is like searching a proof for the theorem. Sometimes, a theorem
has only one (natural) proof. In such a case, there is no ambiguity as to which
proof should be used: There is only one.