4 ms·
Do we not get a category if we take morphisms from A to B to be expressions of type B with a free variable of type A (thus, morphisms are non-closed terms), and
by Chinjut 10y ago
Do we not get a category if we take morphisms from A to B to be expressions of type B with a free variable of type A (thus, morphisms are non-closed terms), and composition of f with g to be substitution of g into the free variable in f? This is automatically associative with proper identities, anyway, even with a purely syntactic notion of morphism equivalence. Of course, one will probably want to impose a coarser notion of equivalence to reason categorically about Haskell in near-usual ways, and perhaps subtleties plague all attempts to do so usefully.