Cool stuff! I used Idris in college and was obsessed with dependent types, (we taught a CS1 course using Idris as a more-friendly Haskell). The students did, uh, not like it and we switched to doing PyGame stuff midway through. It's neat to see how practical linear types can be for modeling resources.
Idris as a *more friendly* haskell! What a concept! I'm not surprised CS1 students didn't like it, but it's cool that dependent types were introduced to students that early. I'm sure at least one person was shown something that changed the course of their career :) Linear types for resources is a really nice idea, but sadly my experience with Idris didn't impress upon me the practicality. I still think it can be made practical, but there is some work to go on that front, in my opinion.
![Megan Thee Stallion - Mamushi (Remix) [feat. TWICE] [Official Audio]](http://i.ytimg.com/vi/5c0_u9PsrsQ/mqdefault.jpg)
Cool stuff! I used Idris in college and was obsessed with dependent types, (we taught a CS1 course using Idris as a more-friendly Haskell). The students did, uh, not like it and we switched to doing PyGame stuff midway through.
It's neat to see how practical linear types can be for modeling resources.
Idris as a *more friendly* haskell! What a concept! I'm not surprised CS1 students didn't like it, but it's cool that dependent types were introduced to students that early. I'm sure at least one person was shown something that changed the course of their career :)
Linear types for resources is a really nice idea, but sadly my experience with Idris didn't impress upon me the practicality. I still think it can be made practical, but there is some work to go on that front, in my opinion.