|
|
|
|
|
|
by ukj
1594 days ago
|
|
|
From the lens of the Curry-Howard isomorphism where logic, category theory and type theory are just different perspectives on the same sort of mental human activity... Implication (logic) is the same thing as internal hom (Category theory); or Function type (type theory). It is just syntax. B |- A in logic translates to f::B -> A in Haskell. https://ncatlab.org/nlab/show/computational%20trilogy#rosett... And then the context left implicit is the transformation of B to A e.g the concrete steps for tranforming B to A. The implementation of f. There is no escaping The Hierarchy. https://en.wikipedia.org/wiki/Chomsky_hierarchy#The_hierarch... |
|
|