4 ms·

The idea of a type hole sounds really nice! Also, I hadn’t thought of Idris, but it makes sense that the more advanced a type system, the more they can take ove

by ahuth 7y ago

The idea of a type hole sounds really nice! Also, I hadn’t thought of Idris, but it makes sense that the more advanced a type system, the more they can take over for tests.

TheAsprngHacker 7y ago
Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statements) and their terms (the expressions of that type) are proofs. It's a straightforward syntactic correspondence: - A -> B (Function type) and A => B (Logical implication) - A * B (Product/Tuple type) and A /\ B (Logical conjunction) - A + B (Sum/Tagged union type) and A \/ B (Logical disjunction) Proving that A implies B is the same thing as writing a function that takes a proof of A and returns a proof of B. Proving the logical conjunction of A and B is the same thing as pairing together a proof of A and a proof of B. So writing a definition that has a certain type is the same thing as proving a theorem. Dependent types [1], which Coq, Agda, and Idris have, further the Curry-Howard correspondence. With dependent types, you can mention programs inside types and therefore express theorems about programs. You have: - The dependent function type (x : A) -> B(x), where the return type B(x) is a function of the input x. This is the same thing as universal quantification, "for all x of type A, B(x) holds." - The dependent tuple type (x : A) B(x), where the type of the second element is a function of the first element x. This is the same thing as existential quantification, "there exists an x of type A where B(x) holds." So with dependent types, you can write mathematical proofs about programs. For example, you can show that a binary operation is commutative. Another good example is the "vector" type [2], which is like the functional-style linked list type, but parameterized over a length. Thus, you can prove that an index out-of-bounds error cannot happen. If you want to learn more about the theory, keywords to search up are "constructive math/proof," "intuitionalistic logic," and "Martin-Lof/intuitionalistic type theory." [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [2] https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...
- ahuth 7y ago
  Very interesting, and I'd never heard of Curry-Howard correspondence. I've also always wondered how dependent types worked conceptually (as in, what's going on there, what are we proving, etc). Thanks for the insights and the links!

by ahuth 7y ago

The idea of a type hole sounds really nice! Also, I hadn’t thought of Idris, but it makes sense that the more advanced a type system, the more they can take over for tests.

TheAsprngHacker 7y ago

Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statements) and their terms (the expressions of that type) are proofs. It's a straightforward syntactic correspondence: - A -> B (Function type) and A => B (Logical implication) - A * B (Product/Tuple type) and A /\ B (Logical conjunction) - A + B (Sum/Tagged union type) and A \/ B (Logical disjunction) Proving that A implies B is the same thing as writing a function that takes a proof of A and returns a proof of B. Proving the logical conjunction of A and B is the same thing as pairing together a proof of A and a proof of B. So writing a definition that has a certain type is the same thing as proving a theorem. Dependent types [1], which Coq, Agda, and Idris have, further the Curry-Howard correspondence. With dependent types, you can mention programs inside types and therefore express theorems about programs. You have: - The dependent function type (x : A) -> B(x), where the return type B(x) is a function of the input x. This is the same thing as universal quantification, "for all x of type A, B(x) holds." - The dependent tuple type (x : A) B(x), where the type of the second element is a function of the first element x. This is the same thing as existential quantification, "there exists an x of type A where B(x) holds." So with dependent types, you can write mathematical proofs about programs. For example, you can show that a binary operation is commutative. Another good example is the "vector" type [2], which is like the functional-style linked list type, but parameterized over a length. Thus, you can prove that an index out-of-bounds error cannot happen. If you want to learn more about the theory, keywords to search up are "constructive math/proof," "intuitionalistic logic," and "Martin-Lof/intuitionalistic type theory." [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [2] https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...

ahuth 7y ago
Very interesting, and I'd never heard of Curry-Howard correspondence. I've also always wondered how dependent types worked conceptually (as in, what's going on there, what are we proving, etc). Thanks for the insights and the links!