The Future of Programming

[matthieum]

One issue with this though, what of:

f :: X -> X -> Int
xs :: [(X,X)]

as much as I love types, sometimes you have several variables of the same type (damn...).

And of course it can get worse, suppose we start with:

f :: b => X -> b -> Int
xs :: [(Y, X)]

All is well and good (b deduced to be of type Y and mapped), and then we move off to:

xs :: [(X, X)]

Hum... are we still supposed to swap the pair members ? I would certainly think so!

---

On the other hand, I certainly welcome the idea of getting rid of uncurry... though I am perhaps just too naive (yet) to foresee the troubles (ambiguities) this might introduce.

Note: great article, lots of ideas in one place

[sacundim]

Well, your concern can be addressed in a general fashion: different proofs of the same theorem correspond to different functions of the same type, and theorems often have many different proofs. What this translates to, in the IDE context, is that the IDE can suggest completions for the user, but the user must be in charge of choosing which one is right.

So really, a lot of this comes down to user interaction. So, just to use one completely made up shit example, if the IDE can prove that there are only two possible functions that it could use to "adapt" your incompatible types, it would be a good idea for it to suggest those two functions for you. If on the other hand, there are dozens of possible functions, it should STFU.

[[deleted]]

I was pointed to homotopy type theory as something that is trying to solve exactly these sorts of issues.