I can't tell if my question is off-topic or not, but..
Can anyone recommend a book (or whatever) that introduces the aspects of type theory relevant to a would-be language designer?
The Little Typer
41–50 of 138 posts
Re: The Little Typer
#42I can't tell if my question is off-topic or not, but.. Can anyone recommend a book (or whatever) that introduces the aspects of type theory relevant to a would-be language designer?
Strongly recommend Types and Programming Languages [1]. I think it's the most useful + accessible book on type theory out there.
[1] https://www.amazon.com/Types-Programming-Languages-MIT-Press...
Re: The Little Typer
#43I'm glad I checked HN today because this sounds like a fantastic read. I went ahead and picked up a copy of it for myself!
Re: The Little Typer
#44Is there a reason dependent types are not more common?
They can make libraries a pain. Like imagine if someone write a library in C#2025 with dependent types where functions took parameters like [i: i%2 == 0] or whatever. And your big project has no existing dependent types. There's no way to adopt this library unless you pull dependent types all the way in. Or even if you did, but your types were [i: i%4 == 0] or [i: (i+1)%2 == 1] or whatever, you'd have to write proofs…
Maybe some form of gradual typing like TypeScript is somehow possible? And also like TypeScript, a repository for declarations for popular libraries.
Re: The Little Typer
#45Is there a reason dependent types are not more common?
Imagine having to prove a Coq theorem for every function call.
No, it's not really that bad. But almost. I really suggest you play with Idris some; what you can do with it is brilliant, for simple tasks. For complicated tasks, like the fully general propositions you need for library functions, it can get much more complicated than the code itself.
Re: The Little Typer
#46Is there a reason dependent types are not more common?
They're very difficult to use and they make code more complicated.
Re: The Little Typer
#47Earlier quoted context omitted.
nobody ever writes the book about a language/paradigm's downsides Indeed. One can argue that books like "optimizing X" or "secure X" are about ways to easily write slow or insecure code in X, but this is somewhat narrow. Is there never enough demand for a broader book on downsides of X?
Bertrand Meyer's book on Eiffel was all about the downsides of C++. And then there's the Unix-Hater's Handbook... https://en.wikipedia.org/wiki/The_Unix-Haters_Handbook I wrote a whole chapter about the downsides of X -- do you think there's a need for a broader book? ;) https://medium.com/@donhopkins/the-x-windows-disaster-128d39...
The one where you demonstrated that you don't know the difference between a client and a server? :-)
Re: The Little Typer
#48Sad to say the book isn't on Library Genesis, so you'll have to drop $40 if you want the knowledge. http://libgen.io/search.php?req=little+typer Also Library Genesis is amazing: http://libgen.io/search.php?req=knuth It's everything I dreamed of when I was a kid. I used to spend hours at the local library scouring through crummy "Learn C++ in 24 hours" type books. http://custodians.online/ is worth a read too.
It took a lot of work for the author to draft this. Would it kill you to compensate them for it?
Re: The Little Typer
#49Sad to say the book isn't on Library Genesis, so you'll have to drop $40 if you want the knowledge. http://libgen.io/search.php?req=little+typer Also Library Genesis is amazing: http://libgen.io/search.php?req=knuth It's everything I dreamed of when I was a kid. I used to spend hours at the local library scouring through crummy "Learn C++ in 24 hours" type books. http://custodians.online/ is worth a read too.
I feel like there’s so much to say about this comment, that I don’t even know where to start.
So firstly I agree, $40 seems like a lot. I personally couldn’t justify it at the moment. Particularly when the reproduction cost is nearly zero.
But $40 also doesn’t seem like a lot to pay for a book that will probably not sell more than a few thousand copies. Most likely revenue generated won’t fully cover the time and effort required to create such a book.
But... the author is also a professor at MIT. I feel like if this work wasn’t somewhat publicly funded, it really should have been.
In the end, I’m left morally confused. But it feels like something is wrong in the world when a book like this is available only to a select few, when for the same capital outlay it could be available to everybody.
Re: The Little Typer
#50As an aside, it's great that Duane Bibby is still providing the art for these. Without him, nothing would be the same.