4 ms·
Why do you use the phrasing "heavy-duty (dependant) type system"? Are you of the opinion that dependant typing is overkill for general programming? What is you
by codygman 12y ago
Why do you use the phrasing "heavy-duty (dependant) type system"? Are you of the opinion that dependant typing is overkill for general programming?
What is your opinion of Idris?
- tel 12y agoDT is definitely heavy-duty. There are massive unsolved problems about how to make, say, proof management... basically even possible. This is part of what makes HoTT exciting, I believe, as it provides a formalized way of passing proofs and operations around over different types so long as there's a suitable homotopy. So while Idris is a very exciting research direction, it's completely fair to state that they have a hefty set of barriers to overcome before they truly demonstrate the value of DT in some larger variety of usecases besides just theorem proving.