it's nice for the haskell folks that they'll be getting some sort of dependent types, but suffice it to say that they will be of a very different sort than the Idris ones.
Not to mention, there is hope of giving a semantics to Idris since it is based on a fairly routine variant of type theory, whereas I don't think there is any hope at all of understanding "which" type theory the Haskell folks shall have implemented.
I think it will be a while, if ever, before we're able to handle passing types around as values, in Haskell, the way we do in Idris and Agda. Dependent typing isn't just some feature. It touches a whole other way of thinking about things.
If you go all the way with Agda, you have significantly constrained recursion to the point that the language isn't turing-complete anymore, but in return you get termination checking and other nice things. As it turns out, most of the code we write doesn't need unbounded recursion. Seriously, can you think of the last time you wrote something like that?
And I think that'll be a hard pill for people to swallow, much like how it was really hard to sell memory safety to C/C++ guys back in the day.
Comments
Great article and really interesting language!
I wonder how Idris is going to be affected when Dependent types come to Haskell as well (announced at last ICFP)
it's nice for the haskell folks that they'll be getting some sort of dependent types, but suffice it to say that they will be of a very different sort than the Idris ones.
Not to mention, there is hope of giving a semantics to Idris since it is based on a fairly routine variant of type theory, whereas I don't think there is any hope at all of understanding "which" type theory the Haskell folks shall have implemented.
I think it will be a while, if ever, before we're able to handle passing types around as values, in Haskell, the way we do in Idris and Agda. Dependent typing isn't just some feature. It touches a whole other way of thinking about things.
If you go all the way with Agda, you have significantly constrained recursion to the point that the language isn't turing-complete anymore, but in return you get termination checking and other nice things. As it turns out, most of the code we write doesn't need unbounded recursion. Seriously, can you think of the last time you wrote something like that?
And I think that'll be a hard pill for people to swallow, much like how it was really hard to sell memory safety to C/C++ guys back in the day.