It can’t. Your type is too general. Not sure what this specific plugin will do, but it will probably just come up with some expression that will have that type. Possibly the one you want – but probably not. :)
For example of types of functions where the types will only allow one, correct implementation, look up implementations of e.g. length-indexed vectors or red-black trees in dependently typed programming languages. It’s also interesting to look at the interactive modes for languages such as Agda and Idris where you can tell your editor “complete this expression” and it will do that (or tell you that it’s not able to, and what’s missing).
I believe that these tools are not based on parametricity, merely on syntactic proof search (in essence, enumerating possible terms at this type, using techniques from the proof search literature). If you think about it, theorems-for-free does not actually help you generate code at arbitrary types.
Abstract types and parametric polymorphism are a nice language feature that has several consequences. One is the existence of free theorems (technically, a nice denotational semantics in the categoy of relations), another is the possibility of having a restricted enough search space that blind proof search produces sensible/interesting program. Those two consequences are independent, I don’t think that you can claim that one is a “side effect” of the other.
“Theorem for free” is an interesting and thought-provoking and well-written research article, so people will easily share it and think about it. This is great! But it also result in some miscomprehensions (or at least exaggerations) about what the result says, which result in the article sometimes being cited in situations where it is not actually relevant (besides being in the same scientific domain as the work being discussed). I thought you may be interested a slightly more detailed picture of the technical details at play here.
Thanks for the clarification. As you say, this is stuff I know exists, but do not work with it daily so do not understand the full implications and shortcomings.
So this creates the function code from the types? I don’t understand how that works.
If I have
Int -> Int -> Inthow would that know I want the functionfoo bar baz = bar + bazand notfoo bar baz = bar - baz?It can’t. Your type is too general. Not sure what this specific plugin will do, but it will probably just come up with some expression that will have that type. Possibly the one you want – but probably not. :)
For example of types of functions where the types will only allow one, correct implementation, look up implementations of e.g. length-indexed vectors or red-black trees in dependently typed programming languages. It’s also interesting to look at the interactive modes for languages such as Agda and Idris where you can tell your editor “complete this expression” and it will do that (or tell you that it’s not able to, and what’s missing).
I think it is relying on the free theorems guaranteed by parametricity.
See Philip Wadler’s paper Theorems for Free!
I believe that these tools are not based on parametricity, merely on syntactic proof search (in essence, enumerating possible terms at this type, using techniques from the proof search literature). If you think about it, theorems-for-free does not actually help you generate code at arbitrary types.
Ok, thanks.
But I think the fact that this is possible is a side effect of the free theorems granted by parametricity.
Which explains why it is not possible to do this with a concrete type signature, as per the original question.
Abstract types and parametric polymorphism are a nice language feature that has several consequences. One is the existence of free theorems (technically, a nice denotational semantics in the categoy of relations), another is the possibility of having a restricted enough search space that blind proof search produces sensible/interesting program. Those two consequences are independent, I don’t think that you can claim that one is a “side effect” of the other.
“Theorem for free” is an interesting and thought-provoking and well-written research article, so people will easily share it and think about it. This is great! But it also result in some miscomprehensions (or at least exaggerations) about what the result says, which result in the article sometimes being cited in situations where it is not actually relevant (besides being in the same scientific domain as the work being discussed). I thought you may be interested a slightly more detailed picture of the technical details at play here.
Thanks for the clarification. As you say, this is stuff I know exists, but do not work with it daily so do not understand the full implications and shortcomings.