4 ms·

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

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

jules 11y ago
I don't understand what you mean by encoding tax. Can you give an example? Certainly lots and lots of work to make an actual practical and usable system still needs to happen, but I don't see any fundamental limitations with respect to effects, including non-termination. > For a start you have to prove termination, even when you use simple types. This is not the case. E.g. in Idris you have non-terminating functions. In NuPRL the whole thing is built on potentially non-terminating functions. Of course the functions that you use as proof witnesses have to terminate, but that's true in any system since a non-terminating proof witness means that the proof is bogus ("Theorem: Socrates is a goat. Proof: Socrates is a goat because Socrates is a goat."). The functions in the program that that the specification is saying something about do not have to be proven to terminate. > (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 I don't want to prove that I didn't need the cast or check, I want to not have the cast or check in the program in the first place. This is about types that are expressive enough to model the actual shape of the data, not about proving that a program is correct relative to some specification. By analogy with lacking generics / parametric polymorphism like old versions of Java: if I write a program that uses a List I need to cast to and from Object. With generics I can use a List<T> and do not need the cast. I don't want to write the program with casts and then prove that I didn't need them, I want to write the program with List<T> without casts. For the same reason that you still want generics even if you use a program logic to reason about your programs, you still want dependent types even if you use a program logic to reason about your programs. > 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. Why? You can write the same program without specification as you would in the program logic system, and then prove lemmas about it. > the beauty stands in the way of type inference Type inference is overrated anyway, and with dependent types you don't actually lose type inference. You do lose it for the parts of the programs that use fancy types, but you wouldn't be able to write those at all in a language with full type inference. There is no fundamental reason that a dependently typed language couldn't have the same type inference for non-dependently typed pieces of the program as the language that only supports non-dependent types. By the way, and I admit this is more of a theoretical curiosity, IIRC full type inference for dependent types is decidable if you do not have implicit parameters. That does make sense: you can either infer types, or values, but not both at the same time. Of course in practice you much rather have implicit parameters than type inference. From the proof assistant side of Curry-Howard type inference is also kind of strange: you infer the theorem (the type) from the proof (the program). So it's like writing down a proof, but having it inferred what the proof is actually proving. > the Hindley-Milner polymorphic typing system "has hit a sweetspot" Where sweetspot = local optimum :) Meanwhile, OCaml is getting GADTs ;-)

by mafribe 11y ago

jules 11y ago

I don't understand what you mean by encoding tax. Can you give an example? Certainly lots and lots of work to make an actual practical and usable system still needs to happen, but I don't see any fundamental limitations with respect to effects, including non-termination. > For a start you have to prove termination, even when you use simple types. This is not the case. E.g. in Idris you have non-terminating functions. In NuPRL the whole thing is built on potentially non-terminating functions. Of course the functions that you use as proof witnesses have to terminate, but that's true in any system since a non-terminating proof witness means that the proof is bogus ("Theorem: Socrates is a goat. Proof: Socrates is a goat because Socrates is a goat."). The functions in the program that that the specification is saying something about do not have to be proven to terminate. > (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 I don't want to prove that I didn't need the cast or check, I want to not have the cast or check in the program in the first place. This is about types that are expressive enough to model the actual shape of the data, not about proving that a program is correct relative to some specification. By analogy with lacking generics / parametric polymorphism like old versions of Java: if I write a program that uses a List I need to cast to and from Object. With generics I can use a List<T> and do not need the cast. I don't want to write the program with casts and then prove that I didn't need them, I want to write the program with List<T> without casts. For the same reason that you still want generics even if you use a program logic to reason about your programs, you still want dependent types even if you use a program logic to reason about your programs. > 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. Why? You can write the same program without specification as you would in the program logic system, and then prove lemmas about it. > the beauty stands in the way of type inference Type inference is overrated anyway, and with dependent types you don't actually lose type inference. You do lose it for the parts of the programs that use fancy types, but you wouldn't be able to write those at all in a language with full type inference. There is no fundamental reason that a dependently typed language couldn't have the same type inference for non-dependently typed pieces of the program as the language that only supports non-dependent types. By the way, and I admit this is more of a theoretical curiosity, IIRC full type inference for dependent types is decidable if you do not have implicit parameters. That does make sense: you can either infer types, or values, but not both at the same time. Of course in practice you much rather have implicit parameters than type inference. From the proof assistant side of Curry-Howard type inference is also kind of strange: you infer the theorem (the type) from the proof (the program). So it's like writing down a proof, but having it inferred what the proof is actually proving. > the Hindley-Milner polymorphic typing system "has hit a sweetspot" Where sweetspot = local optimum :) Meanwhile, OCaml is getting GADTs ;-)