|
|
|
|
|
|
by sourceless
1724 days ago
|
|
|
I don't know, some of that is at least starting to happen with Idris 2, though not in the exact way predicted: https://www.youtube.com/watch?v=mOtKD7ml0NU (Type Driven Development with Idris 2) Short summary of linked video: when your type system is powerful enough you can restrict the set of possible implementations to the point that the compiler can make a decent guess as to what the program should be to satisfy the type signature. |
|
|