icen

This is why `f` is really my workhorse key in vim.

There are a million monad tutorials for Haskell (and, with respect to their use in Haskell, it's probably better to learn them from there). I think that a good one is "You Could Have Invented Monads!".

This[1] is a good paper about monads in functional programming. It reads quite similarly to a monad tutorial, but with a little more formality.

As for actual category theory, I've enjoyed the first few chapters of "Algebra: Chapter 0", by Aluffi.

If you're after more type theory, the usual recommendations are "Types and Programming Languages", by Pierce, and "Software Foundations", also by Pierce.

[1] http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba...

You'd get pretty far just by whitelisting arxiv, .edu, .ac.uk, etc.

In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs.

If you wanted to prove that a list was sorted, you'd write another datatype:

    IsSorted : Ord a => List a -> Type

which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair:

    (l : List a ** IsSorted l)

which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!).

The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.

Nothing; it would return a partially applied function that waits for a proof that `x < y` before continuing. (Trying to use that function as an integer would be a type error).

The key here is that `add` is not a function `Nat -> Nat -> Nat`, it is a function `(a : Nat) -> (b : Nat) -> LT a b -> Nat`. There are just some compiler features that allow you to avoid having to write out the full `LT a b` proof each time you want to add things!

You can just write something like

    foo x = case x of
              pattern1 -> ...

An expressive and ergonomic type system goes a very long way into codifying that intent.

For example, it's quite obvious what the intent of this Idris function is: `f : Vect n (Vect m a) -> Vect m (Vect n a)` (where `Vect` is the type of lists of a given length).

Here is RMS' piece on nonfree javascript:

https://www.gnu.org/philosophy/javascript-trap

For a western analogue, try the BBC's spaghetti plantations.

It's not like that first factorial function is actually any worse than the usual Haskell one:

    fac = \n -> product [1..n]

The recursive one is also much the same as a Haskell one, but Q is hardly built around idiomatic recursion.

This[1] would be the one, right?

http://kparc.com/q4/readme.txt

You should add Screencheat to your list. Amazing fun.

I use `!rustn` because it's more convenient than actually loading my local copy of the rust documentation.

The same reason you have pensions now, despite guaranteed state pensions. Whilst $10K is probably liveable, in some places, if you own a house, it's likely not going to be terribly comfortable.

It just means to bind a variable:

    let x : u32 = 0;

In Haskell, it's used for temporary definitions, or pure definitions in do blocks:

    let f = \x -> x + 1 in f 2

When you go to vote, are you only ever concerned about the mechanical action to place a cross in a box?

There's quite a lot more to politics, and politics in democracy, than just the act of voting.

Munkres is very good. If you're after algebraic topology, Hatcher is also good (and freely available online).