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:
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