7 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

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

jules 11y ago
> 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. There is general consensus that the best way to handle effects is a pure base language with an effect system on top. Idris takes a good shot at this, but I doubt it's the last word. Eff and Koka and F* seem particularly promising as well. > 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. Why did type inference become the #1 criterion for a type system in this discussion? There are far more important criteria than type inference, such as expressiveness. If your type system is not expressive enough you wouldn't be able to write the program that can't be type inferred at all. Why is that a win? > Yes, but they are not in your proof language. You can always code up anything. No sound system can have non terminating functions as proof witnesses. You can reason about potentially non terminating functions just fine in dependently typed languages. Look in particular at NuPRL, which is build around the concept. > 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. Doing type inference for non HM-typeable parts of programs is theoretically simple. For the parts of the program that do not have type annotations just type infer them with a HM inference algorithm, if it succeeds great if it fails signal a type error. Just like in ML. The reason that it hasn't been done is likely a combination of reasons (1) not publishable (2) a lot of work (3) type inference just isn't that important especially if you're only doing it for the HM-typeable fragment. > My experiences in Coq and Agda suggest that that's not the case. Coq and Agda are not the pinnacle of the possibilities of dependent types. As I said, it's ongoing research. My point is that the style of writing a program and then separately proving lemmas about it is perfectly possible in a dependently typed language. I would also suggest that your experience may not yet have been that extensive if you didn't know about 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? Implicit parameters let you mark function parameters as implicit and they will be inferred at the call site if the compiler can deduce that they must have one particular value in order for the program to type check. It's like the reverse of type inference: instead of inferring the type of an expression, we infer the expression from the type. It's kind of related to type classes, which let the compiler infer type class dictionaries from types. Look at the Sage work for full inference for refinement types. I think the same strategy could work for full dependent types. Of course it's not really what you want in practice, since in a dependent type system the most precise type you infer for a function simply restates what the function computes. That is, if you have the function (\x -> x+2) then the type will simply say "a function that returns its argument +2". Inferring the most precise HM type gives reasonable results precisely because HM is weak, so you don't get a type that's "too precise" ;-) > Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still. Type inference for GADTs is undecidable.

by mafribe 11y ago

jules 11y ago

> 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. There is general consensus that the best way to handle effects is a pure base language with an effect system on top. Idris takes a good shot at this, but I doubt it's the last word. Eff and Koka and F* seem particularly promising as well. > 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. Why did type inference become the #1 criterion for a type system in this discussion? There are far more important criteria than type inference, such as expressiveness. If your type system is not expressive enough you wouldn't be able to write the program that can't be type inferred at all. Why is that a win? > Yes, but they are not in your proof language. You can always code up anything. No sound system can have non terminating functions as proof witnesses. You can reason about potentially non terminating functions just fine in dependently typed languages. Look in particular at NuPRL, which is build around the concept. > 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. Doing type inference for non HM-typeable parts of programs is theoretically simple. For the parts of the program that do not have type annotations just type infer them with a HM inference algorithm, if it succeeds great if it fails signal a type error. Just like in ML. The reason that it hasn't been done is likely a combination of reasons (1) not publishable (2) a lot of work (3) type inference just isn't that important especially if you're only doing it for the HM-typeable fragment. > My experiences in Coq and Agda suggest that that's not the case. Coq and Agda are not the pinnacle of the possibilities of dependent types. As I said, it's ongoing research. My point is that the style of writing a program and then separately proving lemmas about it is perfectly possible in a dependently typed language. I would also suggest that your experience may not yet have been that extensive if you didn't know about 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? Implicit parameters let you mark function parameters as implicit and they will be inferred at the call site if the compiler can deduce that they must have one particular value in order for the program to type check. It's like the reverse of type inference: instead of inferring the type of an expression, we infer the expression from the type. It's kind of related to type classes, which let the compiler infer type class dictionaries from types. Look at the Sage work for full inference for refinement types. I think the same strategy could work for full dependent types. Of course it's not really what you want in practice, since in a dependent type system the most precise type you infer for a function simply restates what the function computes. That is, if you have the function (\x -> x+2) then the type will simply say "a function that returns its argument +2". Inferring the most precise HM type gives reasonable results precisely because HM is weak, so you don't get a type that's "too precise" ;-) > Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still. Type inference for GADTs is undecidable.