harveywi

29 ms·

271.
by harveywi 11y ago
To my knowledge, intuitionistic type theory (ITT) considers type of higher order (called higher-kinded types), so homotopy type theory (HoTT) isn't exactly relevant here - especially since it has, to my knowledge, not cross-pollinate
272.
by harveywi 11y ago
There could be some fishiness to it. However... One of the things I noticed right away is that the therapeutic programs prescribed to the patients patients in the study combined autophagy/ketosis (fasting 12 hours at night), low-glyce
273.
by harveywi 11y ago
Personally, I believe Zuckerberg is sincere in wanting to connect everyone in the world with each other. I feel sure he doesn't think of it as a land grab Does anyone recall what Zuckerberg said about the people who "trust him
274.
by harveywi 11y ago
Idris ( http://www.idris-lang.org/ ). Edwin Brady is working on a book that you can access via the Manning Publications MEAP program ( https://www.manning.com/books/type-driven-development-with-i... ).
275.
by harveywi 11y ago
You can already compile BLAS/LAPACK/etc. to JavaScript, but you have to jump through some hoops. Proof of concept: https://github.com/harveywi/arpack-js
276.
by harveywi 11y ago
> these aren't programming languages, they're data languages. Sounds like a job for free applicative functors, which are strictly less powerful than free monads (which you can imagine as the set of interpretable languages).
277.
by harveywi 11y ago
Lawrence H. Dunn III from FSU put together a really nice honors thesis that provides a gentle overview of HoTT. The author was an undergrad math student, so there might be a couple mistakes here and there, but the text was quite accessible
278.
by harveywi 11y ago
The introduction and chapter 1 of the (free) homotopy type theory book ( http://homotopytypetheory.org/book/ ) provide a great overview of type theory and the Curry-Howard correspondence which, for me, was the moment whe
279.
by harveywi 11y ago
You can do it in Scala too (cf. https://github.com/milessabin/shapeless/wiki/Feature-overvie... ).
280.
by harveywi 11y ago
From the article: "In the case of the spinal cord injury data, Ayasdi’s TDA-driven approach mostly confirmed what researchers already knew: The drugs didn’t work." How this "Ayasdi" company's analysis probably works
281.
by harveywi 11y ago
Have you actually been in a PhD program before? Calling it "freedom" could not be farther from the truth. You don't get to work on whatever you want unless you want to pay your own way. Stray a little bit out of your adviso
282.
Leon: An automated system for verifying Scala code, now with support for Isabelle(groups.google.com)
9 points by harveywi 11y ago|0 comments
283.
Java Code Generator for Idris(github.com)
34 points by harveywi 11y ago|3 comments
284.
by harveywi 12y ago
Location: Columbus, OH Remote: Yes Willing to relocate: Maybe Technologies: Scala, Shapeless, Scalaz, Akka, Slick, C#, C#, Haskell, C, C++, Python SQL, MATLAB, LISP, Bash, Coq, Play! Framework, ASP.NET CV: http://www.aylasoftware
285.
by harveywi 12y ago
I've been through it all - from qualifying exams, to candidacy, to defense, to postdoc. To me, these sorts of articles are comparable to "join the army and see the world" propaganda. You never hear about legs blown off, bra
286.
by harveywi 12y ago
It's great that people see the value in having these kinds of functional tools! I also put together a library that looks very similar to this, and it sure has been handy. I used it as a foundation to build some solid algebraic APIs (
287.
by harveywi 13y ago
SEEKING WORK - Remote or Columbus, OH area - Eleven years of professional experience in scientific software development, including application development, requirements definition, testing, profiling, optimization, performance tuning, refac