@abs It is a theorem. but it springs from a letter-exchange between curry & howard (therefore curry-howard-correspondence).

Basically sais that Types ~ Mathematical preposistions, Values ~ Mathematical proofs.

i.e. if you can implement a function that produces X, you know that at least one X exists & that you can construct it.

fun :: a -> a can be read as "given 'a', prove that 'a'.". if you implement it as "fun x = x" you just proved that identity works :)

@abs the same works for all functions in programming:

f :: Int -> String -> [String] means "given an Int and a String you can create a List of Strings"
ONE implemenation can be:
f 0 y = []
f x y = [y] ++ f (x-1) y

It gets more interesting if you do not use concrete, but abstract types, as they RESTRICT what you can create.
e.g.: the function above explods on f -1 "..".
If you restrict enough there may be only 1 implementation that can be found automatically.

@Drezil I do know what the Curry-Howard correspondence is, I'm just wondering if there actually exists a properly stated theorem (that actually corresponds to our intuition of CH) with a proper proof. Of course it's (relatively) easy to state and prove for any specific combination of logic and type system, but I'm wondering if there is a way to state the correspondence generalized over logics and type systems.

@abs https://www.youtube.com/watch?v=iXZR1v3YN-8
at 18:13 there are all three formulations on the board.

They are just different notations of the same thing.

@Drezil But that's still just specific examples of CH(L), right?

@abs That are just definitions for the axiomatic operations in each one.

look at the first: true, false, and, or & implications are all you need to get everything of boolean logic.
(), Void, x, +, -> are everything you need in whole programming, the third one is everything you need for whole category-theory.

you have a proof in one, you change the syntax & get a proof in the other one.

But in each one some things are more obvious than others.

@abs the first two are needed for the latter 3 definitions to have meaning.. ;)

like () + () x () + () x () x () + ... for the definition of a datatype isomorphic to "positive int"