4 ms·

If it is indeed already outputting multiple code snippets... it would be awesome if you just write the function stub and a couple test cases and it returns only

• still_grokking 5y ago
  You don't need the tests. You need only the types. And especially you don't need "artificial dumbness", which does not understand code, and therefore won't produce correct results, but just an advanced programming language. Say hello to Idris! :-) https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU
  • chriswarbo 5y ago
    If you're completely specifying the behaviour then you're writing a program "manually"; that's what programming is. Using a dependent type system to specify that behaviour is essentially a form of declarative/logic programming, similar to Prolog. Deriving an implementation of those types automatically (e.g. by having the elaborator perform a proof search) is equivalent to compiling your pseudo-Prolog ahead-of-time. It's certainly interesting that such a "compiler" can be guided (e.g. via elaborator reflection), but that's more useful for optimisation rather than implementation. (Note that in some cases, such 'optimisation' might be required for the proof search to finish before the heat death of the universe!)
• qq4 5y ago
  Ooh, you need to see Barliman. https://youtu.be/er_lLvkklsk https://youtu.be/er_lLvkklsk