Joachim Lambek has described an adjunction between the category of graphs and the category of positive intuitionistic calculi with iteration, see e. g. Introduction to Higher Order Categorical Logic part 1, chapter 4. For me, as a computer scientist, the cartesian closed functors in the free category of this adjunction seem like a good setting for defining the semantics of the Hindley Milner type system. Has anyone tried this, or anything remotely similar?
$\begingroup$
$\endgroup$
asked Oct 10, 2023 at 5:42
Add a comment
|