hiker

9 ms·

31.
by hiker 9y ago
Cubical https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical type theory https://arxiv.org/abs/1611.02108 ) interpretation of HoTT. Agda a
32.
by hiker 9y ago
Lean is quite nice dependently typed language https://leanprover.github.io/
33.
by hiker 9y ago
The way I see it there's a whole spectrum of methods for checking program correctness. On the one end are "point tests", manually written tests that check correctness in several predetermined cases. That's what most soft
34.
by hiker 10y ago
Not really, it's equivalent to a product type.
35.
by hiker 10y ago
> return :: x -> (a -> x) > return x = \a -> x > > (>>=) :: (a -> x) -> (x -> (a -> y)) -> (a -> y) > m >>= f = \a -> f (m a) a >(Incidentally, these are two of the Łukasi
36.
by hiker 10y ago
Most of the progress in the field came from the pursuit of photorealism and trying to simulate better what actually happens in reality. The path tracing approaches in modern raytracers are actually very similar as computation to Feynman&#x2
37.
Why Types Matter [pdf](github.com)
2 points by hiker 10y ago|0 comments
38.
The MPFR Library: Algorithms and Proofs [pdf](mpfr.org)
1 points by hiker 10y ago|0 comments
39.
by hiker 10y ago
"Physics, Topology, Logic and Computation: A Rosetta Stone"[1] might be a starting point. [1] http://math.ucr.edu/home/baez/rosetta.pdf
40.
by hiker 10y ago
Quoting from Wikipedia: "Because of the possibility of writing non-terminating programs, Turing-complete models of computation (such as languages with arbitrary recursive functions) must be interpreted with care, as naive application o
41.
by hiker 10y ago
What is commonly known as Curry-Howard correspondence (the duality between programs/proofs, computing/math) actually goes way deeper. The reason is that "computation" is very useful concept but it has taken us ages to de
42.
by hiker 11y ago
Monte Carlo integration is what's used by most (all?) offline production renderers. The standard book on the subject is "Physically Based Rendering" [ http://pbrt.org/ ] if you want to learn more.
43.
by hiker 11y ago
WebGL implementations zero out newly allocated buffers for exactly that reason. https://www.khronos.org/registry/webgl/specs/latest/1.0/#4
44.
by hiker 11y ago
The "Analytic Combinatorics"[1] book by Flajolet and Sedgewick is also relevant here. [1] http://algo.inria.fr/flajolet/Publications/book.pdf
45.
by hiker 12y ago
What's wrong to think that types are important? From mathematical point of view, types are interpreted as theorem statements and functions(values) that typecheck are considered proofs of those theorems. Types are fundamental. See Curry
46.
by hiker 12y ago
I think Kolmogorov complexity is spot on comparison, considering programs as proofs, theorems as types in the Curry–Howard isomorphism.
47.
by hiker 12y ago
As an active Emacs user, I can confirm the answer of all of the above is "yes". Heck, it even has a Tetris and a Psychiatrist built in. My .emacs is portable and I use it across Linux, OS X and Windows. Of course it's based o
48.
by hiker 12y ago
> In that sense, determinism might be a small part of indeterminism. I agree. The astonishing thing about quantum mechanics to me is that it describes how deterministic laws emerge from completely non-deterministic processes. For example
49.
by hiker 12y ago
Functional C version for comparison https://github.com/skaslev/catmull-clark/blob/master/obj.c
50.
by hiker 12y ago
https://www.youtube.com/watch?v=eSWWSq714aQ http://news.bbc.co.uk/2/hi/europe/4923342.stm
51.
by hiker 12y ago
See my comment here https://news.ycombinator.com/item?id=7857316
52.
by hiker 12y ago
Here's a Haskell translation of the C++ version. Runtume is around 10x of the original (probably vector vs list cache trashing and vector sort/unique vs list to set/set to list), code reduction is 3x. import qualified Dat
53.
by hiker 12y ago
I don't see how the use of std::array<int,3> and std::count makes the C++ version less functional. Also, the next_forests.reserve doesn't help as much as you state, it's barely measurable when commenting out from my exp
54.
by hiker 12y ago
It shows that, if you need to, you can drop to direct memory access in Haskell. Also note the "unsafe" in the names of the functions. Of course, the majority of Haskell code uses algebraic data types and garbage collection.
55.
by hiker 13y ago
His system of equations is not linear so vanilla Ax=b won't work.
56.
by hiker 13y ago
Imo this would be hard if not impossible. Mathematical equations don't have any meaning taken by themselves; they just express a certain relationship between quantities without stating anything specific about what those quantities are.
57.
by hiker 13y ago
Not to mention, strings are immutable in Python.
58.
by hiker 13y ago
This is a Haskell insider-joke. As is the The International Obfuscated C Code Contest. You wouldn't judge the value of the C language for writing, let's say, a unix kernel based on the code from IOCCC, would you? Don't take i
59.
by hiker 13y ago
Let me hoogle those for you (sic) http://www.haskell.org/hoogle/?hoogle=liftM =-)
60.
by hiker 13y ago
The syntax in Haskell for dealing with side effects is tedious/verbose by design. The intention is to push one in writing pure programs since pure functions and compositions are easier to test, verify and reason about. Good Haskell pro

More ›