3 ms·

Um, maybe you missed the point about dependent types? You can express a function, that takes no arguments, that returns primes below 1,000,000 as it's type! Tha

by codemac 12y ago

Um, maybe you missed the point about dependent types? You can express a function, that takes no arguments, that returns primes below 1,000,000 as it's type! That's kind of the point of the talk, and is supposed to be possible in languages like Agda and Idris (I don't know enough about them to give any syntax here). See jules' comment below about how curry-howard does not mean your implementation is a full proof as well. Considering code that flies planes and shoots guns generally is written using proofs on control systems (if not required by law), your examples are a bit weak.

AnimalMuppet 12y ago
But the "proofs" of those control systems isn't anything that looks like a type system, is it? (An argument of the form "due to Curry-Howard, all proofs are type systems" will be regarded as uninteresting at best.)
- codemac 12y ago
  Absolutely not, at least not to me. I'm not a huge type theory guy or anything. But saying that "proofs are a burden especially for things with side effects like shooting a gun" when systems that shoot guns specifically do have proofs in spite of their type systems invalidates the example, if not the argument. The presenters certainly think these languages will help construct those proofs.. that I'm less certain of.
cousin_it 12y ago
It seems to me that using dependent types to express the type "the number of primes below one million" would take at least as much code, and be at least as error-prone, as writing that function in a dynamically typed language directly. In fact I'd be surprised if the dependently typed version were less than 2x the size of the direct version.
- codemac 12y ago
  This is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played with Coq or Agda.. because expressing these things are not that much code at all. Also the presentation literally covers that complaint, and how they think more programming languages are needed.
kestert 12y ago
The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite as a GADT: data Composite : Nat -> Type where factors : (x : Nat) -> (y : Nat) -> Composite ((S (S x)) * (S (S y))) but there is no analogous construction of a prime type. Luckily most day to day programming looks more like the composite case than the prime case.
- gergoerdi 12y ago
  As an example, here's how primality is defined in the Agda standard library. It is simply the negation of the property 'has a divisor and is greater than 2'. http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.html http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.ht...

by codemac 12y ago

AnimalMuppet 12y ago

But the "proofs" of those control systems isn't anything that looks like a type system, is it? (An argument of the form "due to Curry-Howard, all proofs are type systems" will be regarded as uninteresting at best.)

codemac 12y ago
Absolutely not, at least not to me. I'm not a huge type theory guy or anything. But saying that "proofs are a burden especially for things with side effects like shooting a gun" when systems that shoot guns specifically do have proofs in spite of their type systems invalidates the example, if not the argument. The presenters certainly think these languages will help construct those proofs.. that I'm less certain of.

cousin_it 12y ago

It seems to me that using dependent types to express the type "the number of primes below one million" would take at least as much code, and be at least as error-prone, as writing that function in a dynamically typed language directly. In fact I'd be surprised if the dependently typed version were less than 2x the size of the direct version.

codemac 12y ago
This is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played with Coq or Agda.. because expressing these things are not that much code at all. Also the presentation literally covers that complaint, and how they think more programming languages are needed.

kestert 12y ago

The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite as a GADT: data Composite : Nat -> Type where factors : (x : Nat) -> (y : Nat) -> Composite ((S (S x)) * (S (S y))) but there is no analogous construction of a prime type. Luckily most day to day programming looks more like the composite case than the prime case.

gergoerdi 12y ago
As an example, here's how primality is defined in the Agda standard library. It is simply the negation of the property 'has a divisor and is greater than 2'. http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.html http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.ht...