This short and to the point post about Idris made me want to try it (at first) and then not, after he described his experiences in getting it to work. I wish everyone who tried out a language would put out a post in this format - it’s extremely helpful to folks trying to get a feel for syntax and usability.
Also, as a bonus, I chuckled several times when I read this because of the sly language sniping.
If you just want to understand dependent types without so much syntax-and-usability struggle, you might be interested in this:
https://mitpress.mit.edu/books/little-typer
Should be available in August.
Out of curiosity, as someone that always hated schemes and lisps in general, but seems to have found Haskell and Idris super fun/useful to learn, what strikes you as the issue in Idris?
And have you read that book at all? Is it beta downloadable prior to release like the idris book was? I’m skeptical that my first try at a lisp should be with dependent types but willing to be proven wrong yet again in life.
If you’re already familiar with Haskell syntax, I imagine that Idris should be easy to learn. In any case, it’s much more of a “real” language, unlike this Little Typer thing which is Racket-based and optimized for being simple and learnable for beginners.
If you don’t like Scheme, I doubt that the Little Typer book will do much for you. It’s probably not the best “Little” book in the series to start with! I’m fond of Scheme myself and find the simplicity of the syntax makes it easier to concentrate on the ideas, but of course that’s a matter of taste.
I have a colleague who’s one of the authors. The source is online somewhere, but I doubt it’s very useful without the book. I have glanced through a preprint, but am looking forward to buying my own copy when it comes out. I’m sure I’ll eventually get around to reading the Idris book too!
Yep Idris was cake coming from Haskell syntax wise. The irony that Haskell actually descends from the lisp family is not lost on me however. I’m just a fan of not having to need so many parens.
I’ll add those to the list of things to read, but that list only grows longer. I do use emacs though so perhaps elisp is the source of my “this language is freaking weird”. But I never really got scheme in school either, activated my uncanny valley I suppose, but I agree its all subjective. Thanks for the link though!
would love to know what was causing the efficiency bottleneck in the reading of the csv file, seemed important and I wish the author had spent a bit more time going into it!
The Idris book is one of my favourite programming books. It describes a simple, iterative technique for exploring a problem (the “type-driven development”) and then shows you how to apply that in a number of different settings, while teaching you a set of complex language concepts almost in passing. I’d recommend anyone who enjoyed previous *-driven-development approaches, and who is interested in functional programming and the Haskell family of languages, to take a look at it.
Syntax and usability are more a function of what you’re used to. I can immediately see a bunch of
casethat should just bemapthat makes that example three times as long as it should be, and I’m no Idris expert.So while I appreciate any review, I’m not sure this style is as useful as you’re saying - it might tell you more about the reviewer than about the language.
Idris is an awesome language to dive into dependent types or go beyond Haskell. The book takes you by the hand with great examples. I’m thinking that the reading CSV example couldn’t benefit much from using dependent types.