kestert

3 ms·

1. 1.▲
   by kestert 11y ago

   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/ht
2. 2.▲
   by kestert 12y ago

   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
3. 3.▲
   by kestert 12y ago

   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 : Na
4. 4.▲
   by kestert 12y ago

   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, whe
5. 5.▲
   Doing Data Science with coLaboratory(googleresearch.blogspot.com)

   39 points by kestert 12y ago|3 comments
6. 6.▲
   by kestert 12y ago

   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. S