I found http://adam.chlipala.net/cpdt/html/Hoas.html to be very useful. It looks like it was once a chapter of the book, but was replaced by the final chapter http://adam.chlipala.net/cpdt/html/ProgLang.html

I found the first version much more useful so I'm posting it here for others.

I like the idea of an random number generator that exploits the full precision of the floats. However, the issue with the naive method is loss of accuracy, not bias. When the article states

If k is 64, a natural choice for the source of bits, then because the set {0, 1, ..., 2^53 - 1} is represented exactly, whereas many subsets of {2^53, 2^53 + 1, ..., 2^64 - 1} are rounded to common floating-point numbers, outputs in [0, 2^-11) are underrepresented.

this is very misleading, because the points that are "underrepresented" are closer together. The discrete probability density created by the naive method is a perfectly good approximation to the uniform distribution.

Furthermore, although as the article shows, we can do better, this can, and must, come at a cost. Since the small numbers occur with much lower probability, the only way to generate them (without importance sampling) is by generating much more randomness (1088 bits in the article). Generating random bits is expensive, and this uses 17 times more randomness than the naive method.

EDIT: it would be possible to avoid generating all the extra bits in most cases, and so an efficient average time algorithm should be possible, but the worst case still requires 1088 bits to be generated.

The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite as a GADT:

  data Composite : Nat -> Type where
    factors : (x : Nat) -> (y : Nat) -> Composite ((S (S x)) * (S (S y)))

but there is no analogous construction of a prime type. Luckily most day to day programming looks more like the composite case than the prime case.

As an example, here's how primality is defined in the Agda standard library. It is simply the negation of the property 'has a divisor and is greater than 2'.

http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.ht...

I'm an engineer on the Google team for coLaboratory. In order to have access to Google Drive (which we need for collaborative editing), the app needs access to your Google account.

I looking into using a weaker set of permissions, where you grant access to the app to read/write data only to files that the user opened with the App (see https://github.com/jupyter/colaboratory/pull/82). This is a much weaker set of permissions since that app cannot write to arbitrary files in Google Drive.

The port of IPython is itself open source (in the repo https://code.google.com/p/naclports/ using the build rule ipython-ppapi), so any developer is free to make their own version (e.g. as a regular web app). We are also working with the IPython/Jupyter team to upstream the collaborative features to the IPython/Jupyter notebook (in a manner that is not tied to using Google's realtime API, but could use any realtime collaboration back end).

Thank you! I'll look at trying this out, along with the Jupyter webapp.

Author here. Glad to see so many people interested.

I think people will find this useful as an example is programming in Idris. While there are many other resources around, this fills a niche as a fairly complete, self contained program.

Since I wrote it, I've noticed that my programming style is not very standard, especially my approach to proofs, so I'm still working on it.

Thanks for this - I've bookmarked it to read later. It looks like you've explained everything pretty thoroughly in the readme, and looks like an excellent example for getting started.