3 ms·

> Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative t

> Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative tool for writing logic where "you're not entirely sure how" it works. You might be surprised to learn that this is not only possible but something research is definitely working towards. In a language like Agda, for example, when there is enough type information available the compiler can fill in the holes for you with the obviously correct implementation. The idea behind program synthesis drives this even further. Using type level specifications we can automatically derive the programs that meet those specifications. This is useful because the language of types is much more concise than the language of terms. For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! It's still early on for this kind of technology but projects like Synquid[0] are making good headway. Dependent-type theory also forms the basis of interactive theorem proving in Coq and Lean[1]. We use something like holes as the basis of proofs. Haskell's typed holes are quite a bit more loose but to me it feels very similar to working with such a system. I propose to Haskell there there exists an expression that satisfies a particular type and then I use the typed holes to fill in my obligations to provide a proof. The hole is my goal and the available objects in scope are my terms. It is a very effective tool for solving hard problems. [0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-types https://www.csail.mit.edu/research/synquid-synthesis-liquid-... [1] https://leanprover.github.io/ https://leanprover.github.io/ update: Links

_bxg1 7y ago
> For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! Yet the humans must still fully consider the higher-level specification. I know that what you describe isn't a compiler per se, but from the perspective of programmer experience it seems analogous. You're not enabling the programmer to "not think", just to think on a more abstracted level. I think the gist of my point still stands; maybe not the final paragraph.
simiones 7y ago
I do wonder whether there is any reason to believe that generating code from types would ever be easier than writing the code directly. More specifically, I wonder if this: > This is useful because the language of types is much more concise than the language of terms. actually holds with sufficiently complex types. For example, would the fully-specified type for quicksort actually be shorter than quicksort? I don't know that there is any reason to believe so. The best we may be able to hope for is that we'll have less work to do for formal verification, since instead of writing both the proofs and the code, we may be able to only write the proofs and have the code for free. However, given that writing the proofs is, at least currently, much, much harder than writing just the code, I'm not sure this type of development would make more than a dent in the software engineering world.
- hopia 7y ago
  In my experience it's much easier. A lot of my API relies on this. I even produce clients in other languages purely based on the API types which act as a form of specification. Haskell's compiler will generate all the logic for serialization and deserialization, leaving me to only implement the actual business logic.
  - simiones 7y ago
    Serialization and deserialization are probably the lowest hanging fruit for this. Java has them, and it can even serialize objects with behavior. I think you're thinking of a very shallow kind of auto-generation of code, which doesn't include any kind of behavior beyond calling your API. The GP though was talking about generating the behavior based on the type specification, which is also doable in principle. For example, you could provide a complex type specification for a sorting function, and have the compiler infer the implementation. For example, you could declare a function which takes a list of `Ord a` and returns a list of `Ord a` such that the second list is a permutation of the first list and each element in the second list is <= to the next element (you of course need dependent types for this). With this type signature, the system could generate the code for a function which achieves this purpose. However, I do not believe that it will be easier to write that type signature (especially if you want to add properties like stability or time and space constraints) than it would be to write the actual sorting function yourself and sticking with `Ord a => [a] -> [a]`. I also don't think we will see anything like this in the near future that doesn't rely on a large set of pre-defined functions that the system simply fills in.
nikofeyn 7y ago
at least with what i have seen of program synthesis, you end up having to write such a specific specification that you are basically defining the implementation (i.e., programming). dependently typed languages also seem woefully unprepared for real systems programming. they are probably good in the small but are so difficult in the large that the costs outweigh the benefits.

_bxg1 7y ago

> For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code! Yet the humans must still fully consider the higher-level specification. I know that what you describe isn't a compiler per se, but from the perspective of programmer experience it seems analogous. You're not enabling the programmer to "not think", just to think on a more abstracted level. I think the gist of my point still stands; maybe not the final paragraph.

simiones 7y ago

I do wonder whether there is any reason to believe that generating code from types would ever be easier than writing the code directly. More specifically, I wonder if this: > This is useful because the language of types is much more concise than the language of terms. actually holds with sufficiently complex types. For example, would the fully-specified type for quicksort actually be shorter than quicksort? I don't know that there is any reason to believe so. The best we may be able to hope for is that we'll have less work to do for formal verification, since instead of writing both the proofs and the code, we may be able to only write the proofs and have the code for free. However, given that writing the proofs is, at least currently, much, much harder than writing just the code, I'm not sure this type of development would make more than a dent in the software engineering world.

hopia 7y ago
In my experience it's much easier. A lot of my API relies on this. I even produce clients in other languages purely based on the API types which act as a form of specification. Haskell's compiler will generate all the logic for serialization and deserialization, leaving me to only implement the actual business logic.
- simiones 7y ago
  Serialization and deserialization are probably the lowest hanging fruit for this. Java has them, and it can even serialize objects with behavior. I think you're thinking of a very shallow kind of auto-generation of code, which doesn't include any kind of behavior beyond calling your API. The GP though was talking about generating the behavior based on the type specification, which is also doable in principle. For example, you could provide a complex type specification for a sorting function, and have the compiler infer the implementation. For example, you could declare a function which takes a list of `Ord a` and returns a list of `Ord a` such that the second list is a permutation of the first list and each element in the second list is <= to the next element (you of course need dependent types for this). With this type signature, the system could generate the code for a function which achieves this purpose. However, I do not believe that it will be easier to write that type signature (especially if you want to add properties like stability or time and space constraints) than it would be to write the actual sorting function yourself and sticking with `Ord a => [a] -> [a]`. I also don't think we will see anything like this in the near future that doesn't rely on a large set of pre-defined functions that the system simply fills in.

nikofeyn 7y ago

at least with what i have seen of program synthesis, you end up having to write such a specific specification that you are basically defining the implementation (i.e., programming). dependently typed languages also seem woefully unprepared for real systems programming. they are probably good in the small but are so difficult in the large that the costs outweigh the benefits.