4 ms·

> I don't get the significance of the Curry-Howard Isomorphism. * Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you ca

by mrkeen 3y ago

> I don't get the significance of the Curry-Howard Isomorphism. * Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you can build a Haskell. * If you have affine logic, you can make Rust. Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time. > What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program? It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4. > But then it also talks about how CHI has applications in verifiable programs, which, I'm told, can reason about side effects. Not every effect is a side-effect. A suitable definition of "side-effect" might be "an effect which is able to punch a hole through whatever type system decided it was valid." If your programming language represents effects as types, then it can reason-about/type-check them just as well as pure functions. [1] https://www.idris-lang.org/docs/idris2/current/contrib_docs/docs/Data.String.Parser.html https://www.idris-lang.org/docs/idris2/current/contrib_docs/...

SilasX 3y ago
>Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you can build a Haskell. * If you have affine logic, you can make Rust. That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages; if the latter is more general it probably should have, and would have, been phrased that way. >Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time. Sorry, what's the connection to CHI here? >It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4. I meant "non-trivial" to apply to the mapping as well. As best I can tell, CHI just says there's some useless program that maps to every proof, and a useless proof that maps to every program. So what? What is the significance of that? So I can write a meaningless program that corresponds to Pons Asinorum? You're not really taking the challenge seriously here -- you're just asserting the same trivialities about which I was asking, "is that all there is?"
- tome 3y ago
  > That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages But proofs are written in systems of logic and programs are written in (programming) languages, so if there's a correspondence between the first there really ought to be a correspondence between the second!

by mrkeen 3y ago

SilasX 3y ago

>Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you can build a Haskell. * If you have affine logic, you can make Rust. That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages; if the latter is more general it probably should have, and would have, been phrased that way. >Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time. Sorry, what's the connection to CHI here? >It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4. I meant "non-trivial" to apply to the mapping as well. As best I can tell, CHI just says there's some useless program that maps to every proof, and a useless proof that maps to every program. So what? What is the significance of that? So I can write a meaningless program that corresponds to Pons Asinorum? You're not really taking the challenge seriously here -- you're just asserting the same trivialities about which I was asking, "is that all there is?"

tome 3y ago
> That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages But proofs are written in systems of logic and programs are written in (programming) languages, so if there's a correspondence between the first there really ought to be a correspondence between the second!