hiker

5 ms·

1.
by hiker 1y ago
Plexes are first mentioned in 1960 https://dl.acm.org/doi/pdf/10.1145/366199.366256 and the paper even starts with a critique of the efficiency of Lisp's approach for representing data with cons pairs (c
2.
by hiker 2y ago
Lean[1] Zulip chat[2] [1] https://leanprover-community.github.io/ [2] https://leanprover.zulipchat.com/
3.
by hiker 2y ago
Liquid Tensor Experiment also comes to mind: https://www.nature.com/articles/d41586-021-01627-2 https://leanprover-community.github.io/blog/posts/lte-final/
4.
by hiker 3y ago
Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment. [1] https://leanprover.zulipchat.com/
5.
by hiker 3y ago
Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Haskell Category".
6.
by hiker 3y ago
There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2] [1] https://github.com/leanprover-community/mathlib4/tree/master... [2]
7.
by hiker 4y ago
It still supports sbrk since it's available on WebAssembly but mmap is not. https://webassembly.org/docs/faq/#what-about-mmap
8.
by hiker 5y ago
> Cool, I have no idea what the fuck this means and how it is useful to me. > Oh wait, I use them every day. Do you really? Do the `functions` you use even fit the above definition? I bet you can think of infinite number of functions
9.
by hiker 5y ago
Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes. [0] https://leanprover.github.io/programming_in_lean/#01_Introdu... [1] h
10.
by hiker 6y ago
If the focus is on finite data structures only and the equivalence relation is "are the types isomorphic", then each type is isomorphic to the ordinary generating functor with some coefficients C : N->N: -- ogf(c,x) = Σ n:ℕ
11.
by hiker 6y ago
Maybe int getint(const char **s) { int res = 0; for (; **s && isspace(**s); (*s)++); for (; **s && isdigit(**s); (*s)++) res = 10 * res + **s - '0'; return res; }
12.
by hiker 7y ago
Integer factorization is also reducible to Knapsack: To factorize integer N invoke a Knapsack solver with knapsack size of log(N) and items of size logarithm of all prime numbers up to sqrt(N): [log 2, log 3, log 5, ...]. If N=pq (say p and
13.
by hiker 8y ago
No suite of tests is complete enough to replace a proof. Unless the domain is finite and the tests exhaust all values in it.
14.
by hiker 8y ago
> Data flow and perhaps control systems (AI scripts and GUIs built around something declarative and event-driven come to mind) indeed seem to be the only commercially successful examples of visual programming thus far. I strongly disagre
15.
by hiker 8y ago
Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types
16.
by hiker 8y ago
"There are only two hard things in Computer Science: cache invalidation and naming things." -- Phil Karlton But I do like "Computability and naming things" better.
17.
by hiker 8y ago
Going further one will need a word for "the kind of a kind", "the kind of a kind of a kind" and so on. One solution is TypeInType, that is the type of a type is another type (not kind or something else). That's wher
18.
by hiker 8y ago
`Void` being the uninhabited type, in the light of the Curry-Howard isomorphism stands for a false proposition. `a -> Void` get interpreted as "not a" or "from a follows contradiction" or equivalently "a is uninh
19.
by hiker 8y ago
> That's just not true. Functional programming does not eliminate state. And yet it says so in the first sentence in the Wikipedia page for functional programming https://en.wikipedia.org/wiki/Functional_program
20.
by hiker 8y ago
Trees, graphs? Of course one can force anything into a relational database. The data analog of "Turing tarpit". Ironically graph databases are way better for describing relations than relational databases.
21.
by hiker 8y ago
Except that functional programming completely eliminates (yet still allows) concern no. 1 in the mentioned order -- state > coupling > complexity > code. Not to mention the better expressive power for describing data structures wit
22.
by hiker 8y ago
I agree with everything besides your stated difficulties with infinities in type theory. Here's one infinity inductive ℕ : Type | zero : ℕ | succ (n : ℕ) : ℕ the type of natural numbers with cardinality ℵ₀. Here' s a bi
23.
by hiker 8y ago
Also set theory vs type theory (in Math) is really just dynamic typing vs static typing (in CS). And we already know how that played out in CS.
24.
by hiker 8y ago
Not really. The boundaries of type theory (say HoTT) are exactly what is possible on a Turing machine (computable). And a step beyond those throws ZFC itself into paradoxes (say Russel's). Moreover ZFC is directly expressible in type t
25.
by hiker 8y ago
https://en.wikipedia.org/wiki/History_of_type_theory Not that much surprised. History of type theory is a history of trying to define precisely computation. That is, try to allow recursion but enforce that all programs
26.
by hiker 8y ago
> So you think the key for understanding constructive logic is to understand some peculiar syntax. It's not only a syntax, it's a functional programming language which turns out to be a computational model for logic.
27.
by hiker 8y ago
It's from https://hott.github.io/book/nightly/hott-online-1174-g29279f...
28.
by hiker 8y ago
The key to understanding logic constructively goes through type theory, not philosophy. I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4f5de2ddc1bd7381...
29.
by hiker 9y ago
Reminds me of the evolution of Lua https://www.lua.org/history.html from a configuration language to a full blown programming language. Awhile ago, we've used this code as data approach in a game development studio for
30.
by hiker 9y ago
Of course you can. The good old {-# LANGUAGE OverlappingInstances #-}.

More ›