The Little Typer

If the project had no existing dependent types at all, couldn't you just perform a runtime check before calling the library? The check would return evidence that [i: i%2 == 0] for the particular i, or fail at runtime. If it succeeded, then you could invoke the library using the new evidence.

One appealing aspect of dependent types is that they let you decouple validation of inputs from the function calls themselves, while still disallowing passing wrong inputs to the function by mistake.

I learned a bit of Idris on the book you link, but I gave up after trying to implement Quicksort (the classical Haskell one-liner) in Idris vectors. You need to manually write a page of theorems for Idris to accept it. It's crazy.

So many assumptions are embedded in your comment. Firstly, it's not proven that piracy affects sales. Quite the opposite: it usually raises popularity for an item, because – if it's good – people sing its praises, which leads to more sales.

You didn't respond to my actual comment. Again, it is victimless because no one would've bought the overpriced book except for those who have $40 to throw away on a lark.

If we focus on making a quality product at a reasonable price, sales follow. The fact that technology has reduced this price to near $0 is unfortunate but is merely a consequence of computers.

I get that technology is often upsetting, but why take it out on users? The way to win is to pay attention to trends and adapt, not wish the world were different.

Riddle me this: Why did people write books before there was an economic incentive for them to? The crux of our disagreement appears to be this: it wouldn't hurt the world for us to return to those times. And technology seems to make this inevitable.

I wish I could get paid to write programming languages all day, but many people wish they could be paid for many things that are not feasible. Are you so sure your book would have maid those thousands of dollars in an era before it was possible to widely distribute it? Who would buy it? And moreover, who would hear about it and how?

https://www.gnu.org/philosophy/right-to-read.en.html

Of course, Lissa did not necessarily intend to read his books. She might want the computer only to write her midterm. But Dan knew she came from a middle-class family and could hardly afford the tuition, let alone her reading fees. Reading his books might be the only way she could graduate.

It's always interesting to watch Stallman's writings become reality.

In fact, this is so prescient as to be worth quoting in full:

Programmers still needed debugging tools, of course, but debugger vendors in 2047 distributed numbered copies only, and only to officially licensed and bonded programmers. The debugger Dan used in software class was kept behind a special firewall so that it could be used only for class exercises.

It was also possible to bypass the copyright monitors by installing a modified system kernel. Dan would eventually find out about the free kernels, even entire free operating systems, that had existed around the turn of the century. But not only were they illegal, like debuggers—you could not install one if you had one, without knowing your computer's root password. And neither the FBI nor Microsoft Support would tell you that.

Substitute "Microsoft Support" for "Apple". We even have officially-licensed and bonded programmers now: The $100 developer ransom.

Lissa did not report Dan to the SPA. His decision to help her led to their marriage, and also led them to question what they had been taught about piracy as children. The couple began reading about the history of copyright, about the Soviet Union and its restrictions on copying, and even the original United States Constitution. They moved to Luna, where they found others who had likewise gravitated away from the long arm of the SPA. When the Tycho Uprising began in 2062, the universal right to read soon became one of its central aims.

You claim you are a victim. Yet you refuse to acknowledge that there are people who can't afford your work who would otherwise be enriched by it. Of the two victims, it's hard to say which is worse. Especially given that people will continue writing books even when there is no incentive to.

Try to write the classic Haskell Quicksort in Idris:

    qsort :: Ord a => [a] -> [a]
    qsort [] = []
    qsort (p:xs) = qsort (filter (= p) xs)

and let me know how it goes, if you will. That's when I gave up on Idris.

Don't get me wrong - CT is a super handy thing to learn, and it pops up a ton when thinking about any software, including type checkers and compilers, but the OP was specifically asking about type theory and programming language implementation. Yes, you can express lots of category theory in terms of type theory (the dream is to implement all of it in terms of TT so that we can mechanise it), but it won't be the best use of your time if you want to build a type system.