You cannot produce an output of type B in a generic way, even if you are given access to an element of type A.
...except in Haskell, where we can make functions for generating instances given a desired type. (Such as Magic Haskeller.) I still feel like it’s accurate to say that general-purpose languages correspond to trivialism.
Thanks, though! I didn’t think of the generic version. So, in general, inhabited types all act like “true” in the isomorphism. (We have A->B wherever B is a specific inhabited type.)
What I’m trying to say is that the types that type theorists use look a lot more like propositions than the types that mundane programmers use.
I’m fully aware of that, and I enjoy the correspondence. What bothers me is that people seem to go from a specific isomorphism (which has been extended greatly, granted) to a somewhat ill-defined general principle.
My frustration comes largely from hearing mistakes. One extreme example is thinking that (untyped!) lambda calculus is the universal logic (capturing first-order logic and any higher-order logic we might invent; after all, it’s Turing complete). Lesser cases are usually just ill-defined invocations (ie, guessing that the isomorphism might be relevant in cases where it’s not obvious how it would be).
Magic Haskeller and Augustsson’s Djinn are provers (or to say it another way, comprehensible as provers, or to say it another way, isomorphic to provers). They attempt to prove the proposition, and if they succeed they output the term corresponding (via the Curry-Howard Isomorphism) to the proof.
I believe they cannot output a term t :: a->b because there is no such term, because ‘anything implies anything else’ is false.
...except in Haskell, where we can make functions for generating instances given a desired type. (Such as Magic Haskeller.) I still feel like it’s accurate to say that general-purpose languages correspond to trivialism.
Thanks, though! I didn’t think of the generic version. So, in general, inhabited types all act like “true” in the isomorphism. (We have A->B wherever B is a specific inhabited type.)
I’m fully aware of that, and I enjoy the correspondence. What bothers me is that people seem to go from a specific isomorphism (which has been extended greatly, granted) to a somewhat ill-defined general principle.
My frustration comes largely from hearing mistakes. One extreme example is thinking that (untyped!) lambda calculus is the universal logic (capturing first-order logic and any higher-order logic we might invent; after all, it’s Turing complete). Lesser cases are usually just ill-defined invocations (ie, guessing that the isomorphism might be relevant in cases where it’s not obvious how it would be).
Magic Haskeller and Augustsson’s Djinn are provers (or to say it another way, comprehensible as provers, or to say it another way, isomorphic to provers). They attempt to prove the proposition, and if they succeed they output the term corresponding (via the Curry-Howard Isomorphism) to the proof.
I believe they cannot output a term t :: a->b because there is no such term, because ‘anything implies anything else’ is false.