6 ms·

Okay. Today I'll be the idiot. I don't get it. Or rather, I don't get the significance of the Curry-Howard Isomorphism. Questions: 1) Is there an example of a

by SilasX 3y ago

Okay. Today I'll be the idiot. I don't get it. Or rather, I don't get the significance of the Curry-Howard Isomorphism. Questions: 1) Is there an example of a proof and its corresponding program that makes you say "whoa, trippy, I didn't expect those to be related"? Like, yeah, an Int -> Boolean function "proves" you can construct a Boolean from an integer, but ... so what? What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program? 2) Are the "programs" referred to here to merely pure functions (i.e. side effect-free, global state-free ones)? It sounds like it is based on lines like this: >When a computer program runs, each line is “evaluated” to yield a single output. That ... seems to cram "computer programs" into some kind of Procrustean bed unless we're taking about pure functions. But then it also talks about how CHI has applications in verifiable programs, which, I'm told, can reason about side effects. Feel free to call me an idiot, as long as you can also inspire an aha-moment.

zmgsabst 3y ago
There are only side effects! When you compute a pure function, you’re still physically manipulating registers, cache, etc. You can use the proof-program perspective to formalize reasoning about a program: - you have some domain model; this expresses the “business logic” of your software - you have an abstract model, in a category for your programming language; this expresses an equivalent structure as the “business logic” - you have a concrete model, in a category for your hardware; this expresses an equivalent structure as it gets executed Reasoning about the translations between these steps, their properties, etc is why you want to connect software to proofs. For example, if you want to find an optimal implementation: you want the shortest path of atomic arrows in your hardware category, which corresponds to the desired computation in your language category. Category theory is the language in which we connect our theory of hardware to our theory of the business domain!
zozbot234 3y ago
Int -> Boolean is just the type of any arbitrary decidable property on Int's, so it's not very useful on its own. But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. The proof itself need not even be constructive, since the requirement for constructibility was taken care of by providing the code for that function. Constructibility becomes more of a big deal if you want to be able to compose constructive proofs, or write proofs that rely on instances of some other proof as input, since then the strategy of providing some construction as a bare algorithm and separately proving it correct may run into problems. And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.
- SilasX 3y ago
  > But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. Agreed, but that's beyond the scope of what's asserted with CHI, right? CHI is asserting that my implementation of some type-correct[1] (int-to-)Boolean function is, itself -- irrespective of what I can prove about it -- equivalent to some other proof. What's that proof, and what's interesting about the proof or the mapping? [1] i.e. really does take ints and always returns bools
  - zozbot234 3y ago
    CHI is just the observation that some logical steps in proofs behave as similar steps in programs. For instance, "Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens". Proof by cases can be expressed as a switch { } or match { } construct, and proof by induction behaves as recursion. This often simplifies the writing of "correct by construction" programs since a single construct can take care of both the computational and the logical side.
    - SilasX 3y ago
      >CHI is just the observation that some logical steps in proofs behave as similar steps in programs. It would have to be all, not just some, or it's not an isomorphism (or there are caveats about function purity I mentioned before). >"Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens". Okay, that helps. So where are the mind-blowing examples?
      - kaba0 3y ago
        I am absolutely not an expert here, but you probably want dependent types to have more interesting examples. Hopefully my made up syntax is understandable fermat x y z: Int -> Int -> Int -> c: (x^z+y^z=c^z and Int) This might only ever have an implementation if we hard code it to z=2.
bo1024 3y ago
Maybe not trippy, but a simple set of examples are existence theorems, i.e. "Given these objects, X exists." An example are fixed point theorems. Theorem: For any function g from a convex, compact set to itself, there exists a fixed point of g. program f: g --> x where g is a function from a convex, compact set C to itself, and x satisfies g(x) = x. If you can write the program and it is correct for all such g, that is a proof that such a g always has a fixed point (in particular, you output one). Note the "type" of g is "function from convex, compact set to itself" and the "type" of x is "fixed point of g".
c-cube 3y ago
I also still don't get it, years later. I wrote a short post on this (a bit too inflammatory, tbh, sorry for the URL): https://blag.cedeela.fr/curry-howard-scam/ https://blag.cedeela.fr/curry-howard-scam/ . A lot of logic and theorem proving can be done without ever thinking about CH. In classical logic I think it's not even that convenient anyway, and classical logic is a pragmatic choice.
armchairhacker 3y ago
You won't see many examples of "traditional" languages taking advantage of Curry-Howard. Though you can, e.g. an `Admin` class whose constructor checks that the credentials are for an admin, and functions like `deleteDatabase` which take an `Admin` instance and don't check for admin credentials because they're already "proven". loginAdmin(name: &str, password: &str) -> Result<Admin, AuthenticationError> deleteDatabase(admin: Admin, dbConnection: &DbConnection, dbName: &str) -> Result<(), ConnectionError> But 2) is correct: these aren't real proofs, because globals and errors can break Curry-Howard, not to mention unsafe coercions. let evilAdmin: Admin = unsafe { std::mem::transmute([0; size_of<Admin>()]) }; deleteDatabase(evilAdmin, dbConnection, "important_data"); You can't even allow functions which infinitely loop: in theorem-proving languages, every function must be proved terminating. Otherwise you allow: anything : a anything = recurse 0 where recurse i = recurse (i + 1) But in theorem-proving languages, the idea that "this type represents a logical statement, an instance only exists if it's true" is used very often. A classic example is fixed-size vectors data Nat where 0 : Nat S : Nat -> Nat -- n + 1, "S"uccessor data Vec (n : Nat) a where Nil : forall a, Vec 0 a Cons : forall n a, a -> Vec n a -> Vec (S n) a You will see declarations like: -- Instances of `IsTrue b` only exist if `b = True` data IsTrue (b : Boolean) where Trivial : IsTrue True -- Instances of `Every pred vec` only exist if every element in `vec` satisfies the predicate (so that `pred elem = True`) data Every (pred : a -> Boolean) (vec: Vec n a) where Every_nil : forall pred, Every pred Nil -- Every item of an empty vector satisfies an arbitrary predicate -- Prepending an element which satisfies some predicate to a vector where every element satisfies the same predicate, produces a vector where every element satisfies the same predicate Every_cons : forall pred x xs, IsTrue (pred x) -> Every pred xs Every pred (Cons x xs) foosAreFoo : Every (\n -> n == "foo") (Cons "foo" (Cons "foo" (Cons "foo" Nil))) foosAreFoo = Every_cons Trivial (Every_cons Trivial (Every_cons Trivial Every_nil)) On the other hand, the requirement that all functions must be "logical statements" is essential. Otherwise the programs will crash and the generated proofs will be illogical (and, notice that "crashing program" = "illogical proof"). For example, if one can define the following (impossible to prove) function, one can create programs which crash trying to extract the first element of an empty vector, and proofs which incorrectly assume that all vectors have a first element. head : Vec n a -> a head Nil = ??? head (Cons x _) = x One can define this function though, taking advantage of the fact that there's no such instance `Nil : Vec (S n) a` so only the `Cons` case needs to be matched (which is why this typechecks even though we didn't handle the `Nil` case, while the above example doesn't. Sorry if it's confusing and/or sounds like a cop-out, that's just how it works and real languages accept this kind of pattern matching): head : Vec (S n) a -> a head (Cons x _) = x And, to answer the second point, theorem-proving languages can represent and prove properties of programs with side-effects and even straight-line programs. The former is commonly done using Monads or Algebraic Effects, and the latter using Hoare Logic or another kind of logic data Var a = String -- Example IO monad which represents side-effects (stdin, stdout, and variables) through constructors data IO a where Pure : a -> IO a ReadLine : IO String PrintLine : String -> IO () ReadVar : Var a -> IO (Maybe a) WriteVar : Var a -> Maybe a -> IO a (>>=) : IO a -> (a -> b) -> IO b -- "Pure" program which reads first and last name and prints full name. -- The "interpreter" lazily computes the value of `main` and simultaneously evaluates `IO` actions to get their inner values: -- When it encounters (x >>= y) it computes `x`, evaluates `x` to get the inner value at runtime, -- then computes and evaluates `y` main : IO () main = PrintLine "What is your first name?" >>= \() -> ReadLine >>= \firstName -> PrintLine "What is your last name?" >>= \() -> ReadLine >>= \lastName -> Pure (firstName ++ " " ++ lastName) >>= \fullName -> PrintLine ("Hello " ++ fullName ++ "!") foo : Var Int foo = Var "Foo" -- Proving properties of programs is done with Hoare Logic. -- This is a lot more complicated and full of boilerplate... data Predicate where True : Predicate (!==) : forall a, Var a -> a -> Predicate (/\) : Predicate -> Predicate -> Predicate data HoareTriple (pre : Predicate) (stmt : IO ()) (post : Predicate) where Obvious : forall pre stmt, HoareTriple pre stmt True Merge : forall pre stmt post1 post2, HoareTriple pre stmt post1 -> HoareTriple pre stmt post2 -> HoareTriple pre stmt (post1 /\ post2) WeakenL : forall pre1 pre2 stmt post, HoareTriple pre1 stmt post -> HoareTriple (pre1 /\ pre2) stmt post WeakenR : forall pre1 pre2 stmt post, HoareTriple pre2 stmt post -> HoareTriple (pre1 /\ pre2) stmt post Specific : forall varN n, HoareTriple (varN !== n) (ReadVar varN >>= \nValue - WriteVar (varN + 1)) (varN !== (n + 1)) example : HoareTriple (foo !== 4 /\ foo !== 5) -- Precondition (ReadVar foo >>= \fooValue -> WriteVar (fooValue + 1)) -- Statement (foo !== 5 /\ foo !== 6) -- Postcondition example = ... -- Some combination of Merge, WeakenL, WeakenR, and Specific, but I've written enough
mjw1007 3y ago
I don't think you're being an idiot. There are some connections in mathematics that are quite "magical", where you get something like a correspondence between a family of curved surfaces and a family of integer-valued equations, and it's not at all obvious why that might be until you study it deeply. And sometimes articles about the Curry-Howard Isomorphism suggest that it's an example of that sort (I think this article does, to some extent). But (as I understand it), that isn't the case: here we have a simple directly-constructed correspondence. It's valuable, but not the sort of thing that mathematicians think of as a wonderful result.
miloignis 3y ago
Hmmm, I can try to address your questions. 1) The trippy one I know of is that the Church encoding of numbers is the induction principle for naturals. 2) Generally the programs that are proofs you would want to be pure, but it wouldn't be strictly necessary. The impurity would have to be handled by the type system though, so explicit effects not side-effects. Also, note that even though you want the programs-that-are-proofs to be pure, that doesn't mean you can't prove things about programs that are impure - that is, you have a pure-program that has a type, and that type is a proposition about a different impure program. That is, I can create a pure program that is a proof about my impure program. EDIT: I think something that is a sticking point for a lot of people is looking for a program that is useful by itself that is also the proof of something useful. This is possible, but a bit rare-er - oftentimes you have useful programs with trivial types, or useful programs-that-are-proofs that you don't actually care to run. These are still super useful though! It is possible to have ones that are both - decidability of things is what comes to mind. You could write a program that determines if two naturals are equal - that's a useful program, albeit one of the simplest - and that program also serves as a proof that two naturals are either equal or not - a kind of particular instantiation of the law of excluded middle. One style of programming with dependent types always returns a proof along with the returned value, which might be kind-of what you're looking for. (Think of a regular expression engine that along with the yes/no does this string match this regular expression, returns a proof that the string does or doesn't match, demonstrating its own correctness)
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?"
mostlylurks 3y ago
2) Being restricted to pure functions is not actually much of a restriction at all. Any impure input can be trivially replaced with parameterization over values representing that input and any impure output can be trivially replaced by including state updates or the updated state in the return value. Then your entire codebase can be entirely pure and you can let the language runtime or the compiler deal with that pure data at the very top level of the program, performing the IO as needed. This may be slightly more inconvenient than allowing impurity, but not enough that it would be by any means infeasible, and languages like Haskell have facilities which narrow the gap even further, so it's not much of a restriction at all.
valyagolev 3y ago
I know a Pons Asinorum that kinda was mind-blowing to me. It uses topology connection to define an unexpected function. "Infinite search in finite time" https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ https://math.andrej.com/2007/09/28/seemingly-impossible-func... https://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/ https://math.andrej.com/2008/11/21/a-haskell-monad-for-infin...

by SilasX 3y ago

zmgsabst 3y ago

There are only side effects! When you compute a pure function, you’re still physically manipulating registers, cache, etc. You can use the proof-program perspective to formalize reasoning about a program: - you have some domain model; this expresses the “business logic” of your software - you have an abstract model, in a category for your programming language; this expresses an equivalent structure as the “business logic” - you have a concrete model, in a category for your hardware; this expresses an equivalent structure as it gets executed Reasoning about the translations between these steps, their properties, etc is why you want to connect software to proofs. For example, if you want to find an optimal implementation: you want the shortest path of atomic arrows in your hardware category, which corresponds to the desired computation in your language category. Category theory is the language in which we connect our theory of hardware to our theory of the business domain!

zozbot234 3y ago

Int -> Boolean is just the type of any arbitrary decidable property on Int's, so it's not very useful on its own. But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. The proof itself need not even be constructive, since the requirement for constructibility was taken care of by providing the code for that function. Constructibility becomes more of a big deal if you want to be able to compose constructive proofs, or write proofs that rely on instances of some other proof as input, since then the strategy of providing some construction as a bare algorithm and separately proving it correct may run into problems. And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.

SilasX 3y ago
> But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. Agreed, but that's beyond the scope of what's asserted with CHI, right? CHI is asserting that my implementation of some type-correct[1] (int-to-)Boolean function is, itself -- irrespective of what I can prove about it -- equivalent to some other proof. What's that proof, and what's interesting about the proof or the mapping? [1] i.e. really does take ints and always returns bools
- zozbot234 3y ago
  CHI is just the observation that some logical steps in proofs behave as similar steps in programs. For instance, "Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens". Proof by cases can be expressed as a switch { } or match { } construct, and proof by induction behaves as recursion. This often simplifies the writing of "correct by construction" programs since a single construct can take care of both the computational and the logical side.
  - SilasX 3y ago
    >CHI is just the observation that some logical steps in proofs behave as similar steps in programs. It would have to be all, not just some, or it's not an isomorphism (or there are caveats about function purity I mentioned before). >"Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens". Okay, that helps. So where are the mind-blowing examples?
    - kaba0 3y ago
      I am absolutely not an expert here, but you probably want dependent types to have more interesting examples. Hopefully my made up syntax is understandable fermat x y z: Int -> Int -> Int -> c: (x^z+y^z=c^z and Int) This might only ever have an implementation if we hard code it to z=2.

bo1024 3y ago

Maybe not trippy, but a simple set of examples are existence theorems, i.e. "Given these objects, X exists." An example are fixed point theorems. Theorem: For any function g from a convex, compact set to itself, there exists a fixed point of g. program f: g --> x where g is a function from a convex, compact set C to itself, and x satisfies g(x) = x. If you can write the program and it is correct for all such g, that is a proof that such a g always has a fixed point (in particular, you output one). Note the "type" of g is "function from convex, compact set to itself" and the "type" of x is "fixed point of g".

c-cube 3y ago

I also still don't get it, years later. I wrote a short post on this (a bit too inflammatory, tbh, sorry for the URL): https://blag.cedeela.fr/curry-howard-scam/ https://blag.cedeela.fr/curry-howard-scam/ . A lot of logic and theorem proving can be done without ever thinking about CH. In classical logic I think it's not even that convenient anyway, and classical logic is a pragmatic choice.

armchairhacker 3y ago

You won't see many examples of "traditional" languages taking advantage of Curry-Howard. Though you can, e.g. an `Admin` class whose constructor checks that the credentials are for an admin, and functions like `deleteDatabase` which take an `Admin` instance and don't check for admin credentials because they're already "proven". loginAdmin(name: &str, password: &str) -> Result<Admin, AuthenticationError> deleteDatabase(admin: Admin, dbConnection: &DbConnection, dbName: &str) -> Result<(), ConnectionError> But 2) is correct: these aren't real proofs, because globals and errors can break Curry-Howard, not to mention unsafe coercions. let evilAdmin: Admin = unsafe { std::mem::transmute([0; size_of<Admin>()]) }; deleteDatabase(evilAdmin, dbConnection, "important_data"); You can't even allow functions which infinitely loop: in theorem-proving languages, every function must be proved terminating. Otherwise you allow: anything : a anything = recurse 0 where recurse i = recurse (i + 1) But in theorem-proving languages, the idea that "this type represents a logical statement, an instance only exists if it's true" is used very often. A classic example is fixed-size vectors data Nat where 0 : Nat S : Nat -> Nat -- n + 1, "S"uccessor data Vec (n : Nat) a where Nil : forall a, Vec 0 a Cons : forall n a, a -> Vec n a -> Vec (S n) a You will see declarations like: -- Instances of `IsTrue b` only exist if `b = True` data IsTrue (b : Boolean) where Trivial : IsTrue True -- Instances of `Every pred vec` only exist if every element in `vec` satisfies the predicate (so that `pred elem = True`) data Every (pred : a -> Boolean) (vec: Vec n a) where Every_nil : forall pred, Every pred Nil -- Every item of an empty vector satisfies an arbitrary predicate -- Prepending an element which satisfies some predicate to a vector where every element satisfies the same predicate, produces a vector where every element satisfies the same predicate Every_cons : forall pred x xs, IsTrue (pred x) -> Every pred xs Every pred (Cons x xs) foosAreFoo : Every (\n -> n == "foo") (Cons "foo" (Cons "foo" (Cons "foo" Nil))) foosAreFoo = Every_cons Trivial (Every_cons Trivial (Every_cons Trivial Every_nil)) On the other hand, the requirement that all functions must be "logical statements" is essential. Otherwise the programs will crash and the generated proofs will be illogical (and, notice that "crashing program" = "illogical proof"). For example, if one can define the following (impossible to prove) function, one can create programs which crash trying to extract the first element of an empty vector, and proofs which incorrectly assume that all vectors have a first element. head : Vec n a -> a head Nil = ??? head (Cons x _) = x One can define this function though, taking advantage of the fact that there's no such instance `Nil : Vec (S n) a` so only the `Cons` case needs to be matched (which is why this typechecks even though we didn't handle the `Nil` case, while the above example doesn't. Sorry if it's confusing and/or sounds like a cop-out, that's just how it works and real languages accept this kind of pattern matching): head : Vec (S n) a -> a head (Cons x _) = x And, to answer the second point, theorem-proving languages can represent and prove properties of programs with side-effects and even straight-line programs. The former is commonly done using Monads or Algebraic Effects, and the latter using Hoare Logic or another kind of logic data Var a = String -- Example IO monad which represents side-effects (stdin, stdout, and variables) through constructors data IO a where Pure : a -> IO a ReadLine : IO String PrintLine : String -> IO () ReadVar : Var a -> IO (Maybe a) WriteVar : Var a -> Maybe a -> IO a (>>=) : IO a -> (a -> b) -> IO b -- "Pure" program which reads first and last name and prints full name. -- The "interpreter" lazily computes the value of `main` and simultaneously evaluates `IO` actions to get their inner values: -- When it encounters (x >>= y) it computes `x`, evaluates `x` to get the inner value at runtime, -- then computes and evaluates `y` main : IO () main = PrintLine "What is your first name?" >>= \() -> ReadLine >>= \firstName -> PrintLine "What is your last name?" >>= \() -> ReadLine >>= \lastName -> Pure (firstName ++ " " ++ lastName) >>= \fullName -> PrintLine ("Hello " ++ fullName ++ "!") foo : Var Int foo = Var "Foo" -- Proving properties of programs is done with Hoare Logic. -- This is a lot more complicated and full of boilerplate... data Predicate where True : Predicate (!==) : forall a, Var a -> a -> Predicate (/\) : Predicate -> Predicate -> Predicate data HoareTriple (pre : Predicate) (stmt : IO ()) (post : Predicate) where Obvious : forall pre stmt, HoareTriple pre stmt True Merge : forall pre stmt post1 post2, HoareTriple pre stmt post1 -> HoareTriple pre stmt post2 -> HoareTriple pre stmt (post1 /\ post2) WeakenL : forall pre1 pre2 stmt post, HoareTriple pre1 stmt post -> HoareTriple (pre1 /\ pre2) stmt post WeakenR : forall pre1 pre2 stmt post, HoareTriple pre2 stmt post -> HoareTriple (pre1 /\ pre2) stmt post Specific : forall varN n, HoareTriple (varN !== n) (ReadVar varN >>= \nValue - WriteVar (varN + 1)) (varN !== (n + 1)) example : HoareTriple (foo !== 4 /\ foo !== 5) -- Precondition (ReadVar foo >>= \fooValue -> WriteVar (fooValue + 1)) -- Statement (foo !== 5 /\ foo !== 6) -- Postcondition example = ... -- Some combination of Merge, WeakenL, WeakenR, and Specific, but I've written enough

mjw1007 3y ago

I don't think you're being an idiot. There are some connections in mathematics that are quite "magical", where you get something like a correspondence between a family of curved surfaces and a family of integer-valued equations, and it's not at all obvious why that might be until you study it deeply. And sometimes articles about the Curry-Howard Isomorphism suggest that it's an example of that sort (I think this article does, to some extent). But (as I understand it), that isn't the case: here we have a simple directly-constructed correspondence. It's valuable, but not the sort of thing that mathematicians think of as a wonderful result.

miloignis 3y ago

Hmmm, I can try to address your questions. 1) The trippy one I know of is that the Church encoding of numbers is the induction principle for naturals. 2) Generally the programs that are proofs you would want to be pure, but it wouldn't be strictly necessary. The impurity would have to be handled by the type system though, so explicit effects not side-effects. Also, note that even though you want the programs-that-are-proofs to be pure, that doesn't mean you can't prove things about programs that are impure - that is, you have a pure-program that has a type, and that type is a proposition about a different impure program. That is, I can create a pure program that is a proof about my impure program. EDIT: I think something that is a sticking point for a lot of people is looking for a program that is useful by itself that is also the proof of something useful. This is possible, but a bit rare-er - oftentimes you have useful programs with trivial types, or useful programs-that-are-proofs that you don't actually care to run. These are still super useful though! It is possible to have ones that are both - decidability of things is what comes to mind. You could write a program that determines if two naturals are equal - that's a useful program, albeit one of the simplest - and that program also serves as a proof that two naturals are either equal or not - a kind of particular instantiation of the law of excluded middle. One style of programming with dependent types always returns a proof along with the returned value, which might be kind-of what you're looking for. (Think of a regular expression engine that along with the yes/no does this string match this regular expression, returns a proof that the string does or doesn't match, demonstrating its own correctness)

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?"

mostlylurks 3y ago

2) Being restricted to pure functions is not actually much of a restriction at all. Any impure input can be trivially replaced with parameterization over values representing that input and any impure output can be trivially replaced by including state updates or the updated state in the return value. Then your entire codebase can be entirely pure and you can let the language runtime or the compiler deal with that pure data at the very top level of the program, performing the IO as needed. This may be slightly more inconvenient than allowing impurity, but not enough that it would be by any means infeasible, and languages like Haskell have facilities which narrow the gap even further, so it's not much of a restriction at all.

valyagolev 3y ago

I know a Pons Asinorum that kinda was mind-blowing to me. It uses topology connection to define an unexpected function. "Infinite search in finite time" https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ https://math.andrej.com/2007/09/28/seemingly-impossible-func... https://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/ https://math.andrej.com/2008/11/21/a-haskell-monad-for-infin...