4 ms·

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 n

by 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 ;-)

mafribe 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. Look at the theory of natural numbers. We can reason about them in Peano arithmetic, or in ZFC using one of the well-known ways of encoding natural numbers as sets. Because Peano arithmetic has a model in ZFC, every proof in Peano arithmetic can be converted into a proof in ZFC. But proof search in ZFC is more expensive than proof search in Peano arithmetic, because the latter is less general than the former. ZFC allows you to ask questions like "333 \in \pi", which is perfectly meaningful as a statement about sets, but not meaningful in Peano arithmetic. The "encoding tax" is the increase in proof search space when moving from a specific to a general theory. Let me give you a second example. Most programming languages can be encoded into \pi-calculus, and pi-calculus has a good logic called Hennessy–Milner logic (HML). You can use HML to reason about all \pi-calculus behaviour. Since \pi-calculus is a very expressive model of computing, HML is extremely fine-grained. Now assume you want to reason about ML programs. You do this by translating them into \pi-calculus and then using HML. But due to the fine-grainedness of HML this will be very painful. It's much more efficient to develop a logic for ML itself, and avoid paying the "encoding tax". As I said, I don't know Idris well, but I assume that the proof language does not have state and other effects, so they need to be coded up as pure functions. I expect there to be an "encoding tax" to be paid for this translation of effects into pure functions. This is not the case. E.g. in Idris you have non-terminating functions. Yes, but they are not in your proof language. You can always code up anything. By analogy with lacking generics / parametric polymorphism like old versions of Java: This is not a good analogy, because type-inference can handle parametric polymorphism, whereas general type-dependency on values cannot be dealt in that form. You can write the same program without specification as you would in the program logic system, and then prove lemmas about it. My experiences in Coq and Agda suggest that that's not the case. 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. If it's so simple, then we should have systems that do this. We don't have such systems, hence it's probably not that simple. 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. I don't know what you mean by "implicit parameters". Type inference might be decidable for some weak inexpressive dependently typed systems, but MLTT, CoC, nope? OCaml is getting GADTs ;-) Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still.

by jules 11y ago

mafribe 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. Look at the theory of natural numbers. We can reason about them in Peano arithmetic, or in ZFC using one of the well-known ways of encoding natural numbers as sets. Because Peano arithmetic has a model in ZFC, every proof in Peano arithmetic can be converted into a proof in ZFC. But proof search in ZFC is more expensive than proof search in Peano arithmetic, because the latter is less general than the former. ZFC allows you to ask questions like "333 \in \pi", which is perfectly meaningful as a statement about sets, but not meaningful in Peano arithmetic. The "encoding tax" is the increase in proof search space when moving from a specific to a general theory. Let me give you a second example. Most programming languages can be encoded into \pi-calculus, and pi-calculus has a good logic called Hennessy–Milner logic (HML). You can use HML to reason about all \pi-calculus behaviour. Since \pi-calculus is a very expressive model of computing, HML is extremely fine-grained. Now assume you want to reason about ML programs. You do this by translating them into \pi-calculus and then using HML. But due to the fine-grainedness of HML this will be very painful. It's much more efficient to develop a logic for ML itself, and avoid paying the "encoding tax". As I said, I don't know Idris well, but I assume that the proof language does not have state and other effects, so they need to be coded up as pure functions. I expect there to be an "encoding tax" to be paid for this translation of effects into pure functions. This is not the case. E.g. in Idris you have non-terminating functions. Yes, but they are not in your proof language. You can always code up anything. By analogy with lacking generics / parametric polymorphism like old versions of Java: This is not a good analogy, because type-inference can handle parametric polymorphism, whereas general type-dependency on values cannot be dealt in that form. You can write the same program without specification as you would in the program logic system, and then prove lemmas about it. My experiences in Coq and Agda suggest that that's not the case. 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. If it's so simple, then we should have systems that do this. We don't have such systems, hence it's probably not that simple. 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. I don't know what you mean by "implicit parameters". Type inference might be decidable for some weak inexpressive dependently typed systems, but MLTT, CoC, nope? OCaml is getting GADTs ;-) Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still.