6 ms·

I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another

by mafribe 11y ago

I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another posting in this thread (inability to extend dependent types beyond pure functions, and forcing the full cost of verification on early states of software productions when specifications are unstable), I predict the opposite: dependently typed verification will give way to program logic, the only question is when.

jules 11y ago
Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependently typed languages doesn't mean that you must. It is perfectly possible to program in them like you would in a normal language. That's what I was trying to get at: dependent types are also more expressive, not just more constraining. Now that I know about dependent types I regularly run into situations where I think "gosh, if I had dependent types I wouldn't have had to put in these type casts or handle these error cases that I know for sure cannot happen". So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above: > Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying reverse : Vec n a -> Vec n a or reverse : (xs : List a) -> {ys : List a | length xs == length ys} you can do reverse : List a -> List a and a lemma reverse_preserves_length : forall xs. length (reverse xs) == length xs It's just not the only option you have. What's this forall you say? A dependent function type of course!
- mafribe 11y ago
  Thanks your your reply. Idris has ... is that not satisfactory? I'm not an expert in Idris, but I think effects are encapsulated / encoded somehow in Idris. I don't think full Idris a logic, only the pure sublanguage (please correct me if I'm wrong), so you loose the coincident between programs and proofs. That probably means that there is some "encoding tax" when reasoning about stateful computation. The more complicated the effects the higher the encoding tax. Just imagine you'd have to reduce full concurrency (e.g. pi-calculus) to lambda-calculus. That would be painful. It is perfectly possible to program in them like you would in a normal language. I don't think that's true with current systems. For a start you have to prove termination, even when you use simple types. (Which leads to another shortcoming of the Curry-Howard approach to verification, non-termination.) I regularly run into situations where I think "gosh, if I had dependent types Sure, and I often think the same. But that doesn't address the key point: (1) you can always do the same with program logic, prove that you don't need a cast, but more imporantly (2) in a lot of large-scale programming projects, you don't have good specifications up-front. Instead you have a vague idea, and try to knock out a prototype as soon as possible to show to the customer, who will typically then reply "that's not quite what I want instead ..." and you go back to the drawing board and iterate. The specifications and the program coevolve. In prototype stages you don't actually care if the program needs a cast or not, you just put in the simplest thing that works, and fix/optimise later, probably only after heavy profiling. Who cares if a missing-cast exception is thrown during the protoptye phase? And for large projects the prototyping phase might already involve a team of 50 programmers. Since good specifications are typically only available at the end of a project, when the software is stable, it only really makes sense to pay the (currenly enormous) cost of full verification at the end of the project. With program logic you can easily delay verification until the end of the project (but don't have to), with Curry-Howard based verification you can't. Two, type system researchers promote provably correct programming as the advantage of dependent types. Program logic researchers promote provably correct programming as the advantage of program logic. Anyway, programs can only be provably correct w.r.t. to a specification, but in most programming projects, a meaningful specification is not available in the early stages, so any talk about provable correctness is inapplicable. they generalize a vast swath of different type system features I fully agree with you here, and it's beautiful. But the beauty stands in the way of type inference, and that makes full dependent types extremely costly for most (but not all) forms of software engineering. As B. Pierce says: the Hindley-Milner polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference and simplicity. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. I'm not totally sure I can' follow you here. How does this get around the totality issue?

by mafribe 11y ago

jules 11y ago

Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependently typed languages doesn't mean that you must. It is perfectly possible to program in them like you would in a normal language. That's what I was trying to get at: dependent types are also more expressive, not just more constraining. Now that I know about dependent types I regularly run into situations where I think "gosh, if I had dependent types I wouldn't have had to put in these type casts or handle these error cases that I know for sure cannot happen". So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above: > Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying reverse : Vec n a -> Vec n a or reverse : (xs : List a) -> {ys : List a | length xs == length ys} you can do reverse : List a -> List a and a lemma reverse_preserves_length : forall xs. length (reverse xs) == length xs It's just not the only option you have. What's this forall you say? A dependent function type of course!

mafribe 11y ago
Thanks your your reply. Idris has ... is that not satisfactory? I'm not an expert in Idris, but I think effects are encapsulated / encoded somehow in Idris. I don't think full Idris a logic, only the pure sublanguage (please correct me if I'm wrong), so you loose the coincident between programs and proofs. That probably means that there is some "encoding tax" when reasoning about stateful computation. The more complicated the effects the higher the encoding tax. Just imagine you'd have to reduce full concurrency (e.g. pi-calculus) to lambda-calculus. That would be painful. It is perfectly possible to program in them like you would in a normal language. I don't think that's true with current systems. For a start you have to prove termination, even when you use simple types. (Which leads to another shortcoming of the Curry-Howard approach to verification, non-termination.) I regularly run into situations where I think "gosh, if I had dependent types Sure, and I often think the same. But that doesn't address the key point: (1) you can always do the same with program logic, prove that you don't need a cast, but more imporantly (2) in a lot of large-scale programming projects, you don't have good specifications up-front. Instead you have a vague idea, and try to knock out a prototype as soon as possible to show to the customer, who will typically then reply "that's not quite what I want instead ..." and you go back to the drawing board and iterate. The specifications and the program coevolve. In prototype stages you don't actually care if the program needs a cast or not, you just put in the simplest thing that works, and fix/optimise later, probably only after heavy profiling. Who cares if a missing-cast exception is thrown during the protoptye phase? And for large projects the prototyping phase might already involve a team of 50 programmers. Since good specifications are typically only available at the end of a project, when the software is stable, it only really makes sense to pay the (currenly enormous) cost of full verification at the end of the project. With program logic you can easily delay verification until the end of the project (but don't have to), with Curry-Howard based verification you can't. Two, type system researchers promote provably correct programming as the advantage of dependent types. Program logic researchers promote provably correct programming as the advantage of program logic. Anyway, programs can only be provably correct w.r.t. to a specification, but in most programming projects, a meaningful specification is not available in the early stages, so any talk about provable correctness is inapplicable. they generalize a vast swath of different type system features I fully agree with you here, and it's beautiful. But the beauty stands in the way of type inference, and that makes full dependent types extremely costly for most (but not all) forms of software engineering. As B. Pierce says: the Hindley-Milner polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference and simplicity. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. I'm not totally sure I can' follow you here. How does this get around the totality issue?