1,588 karma · joined October 12, 2016
Researcher at https://www.sift.net/
Email is concat ["me@", username, ".com"]
It's not surprising that Google doesn't turn these up, the golden era of this complaining was pre-WWW.
[0]: https://www.ee.torontomu.ca/~elf/hack/realmen.html [1]: https://melsloop.com/
function f<T>(x: T) { return x; }
function g(x: number) { return { a: f(x), b: f(x.toString()) }; }
in sat?if that's easy, how about length and f in:
function append<T>(xs: list<T>, ys: list<T>) {
return match xs {
Nil() -> ys,
Cons(hd, tl) -> Cons(hd, append(tl, ys)),
};
}
function flatten<T>(xs: list<list<T>>) {
return match xs {
Nil() -> Nil(),
Cons(hd, tl) -> append(hd, flatten(xs)),
};
}
function map<T, U>(f: (T) => U, xs: list<T>) {
return match xs {
Nil() -> Nil(),
Cons(hd, tl) -> Cons(f(hd), tl),
};
}
function sum(xs: list<number>) {
return match xs {
Nil() -> 0,
Cons(hd, tl) -> hd + length(tl),
};
}
function length<T>(xs: list<T>) { return sum(map((_) -> 1, xs)); }
function f<T>(xs: list<list<T>>) {
return length(flatten(xs)) === sum(map(length, xs));
}
hm-style inference handles polymorphism and type application without a complicated sat encodinghttps://costsofwar.watson.brown.edu/sites/default/files/pape...
I'm interested in implementing a safe low-level language with less static information around than C has (e.g. no static pointer-int distinction), but I'd rather keep around the ability to restrict capabilities to only refer to subobjects than have the same compatibility guarantees Invisicaps provide, so I was hoping to look into Monocaps (or maybe another design, if there's one that might fit better).
Formal model: https://github.com/riscv/sail-riscv
That's far more true in a language like JavaScript or Scheme than in an "everything is an object" language like Python; the only reason why you would need a variant type for PyObject is to avoid the circular data structures the actual implementation uses.
If you allow the circular data structures, your dynamic types instead are "merely" a relatively complicated codata type, but it's far less obvious that this is actually what anyone considers to be "merely."
RISC-V is specified as a RISC (and allows very space-/power-efficient lower-end designs with the classic RISC design), but designed with macro-op fusion in mind, which gets you closer to a CISC decoder and EUs.
It's a nice place to be in tooling-wise, but it seems too early to say definitively what extensions will need to be added to get 12900K/9950X/M4 -tier performance-per-core.
In either case though, a bunch of the tricks that make modern CPUs fast are ISA-independent; stuff like branch prediction or [0] don't depend on the ISA, and can "work around" needing more instructions to do certain tasks, for one side or the other.
function parse(x: Foo): Bar { ... }
const y = parse(x);
and function validate(x: Foo): void { ... }
validate(x);
const y = x as Bar;
Zod has a parser API, not a validator API.The human-labor cost of working around Anubis is unlikely to be paid unless it affects enough data to be worth dedicating time to, and the data they're trying to scrape can typically be obtained "respectfully" in those cases -- instead of hitting the git blame route on every file of every commit of every repo, just clone the repos and run it locally, etc.
This _is_ the problem Anubis is intended to solve -- forges like Codeberg or Forgejo, where many routes perform expensive Git operations (e.g. git blame), and scrapers do not respect the robots.txt asking them not to hit those routes.
kbuild handles this on top of Make by having each target depend on a dummy file that gets updated when e.g. the CFLAGS change. It also treats Make a lot more like Ninja (e.g. avoiding putting the entire build graph into every Make process) -- I'd be interested to see how it compares.
The attention mechanism that transformers use to find information in the context is, in its simplest form, O(n^2); for each token position, the model considers whether relevant information has been produced at the position of every other token.
To preserve performance when really long contexts are used, current-generation LLMs use various ways to consider fewer positions in the context; for example, they might only consider the 4096 "most likely" places to matter (de-emphasizing large numbers of "subtle hints" that something isn't correct), or they might have some way of combining multiple tokens worth of information into a single value (losing some fine detail).
This isn't actually right, is it? APX hasn't been released, to my knowledge.
Formal reasoning about imperative programs in terms of their (e.g. axiomatic) semantics is only in a grad-level course, and the programs you can reason about are really, really limited compared to the functional ones. (The last time I TA'd the FP class, one of the homeworks involved proving a simple compiler correct. When I took the grad course, I think the most complicated program we proved correct was selection sort.)
I think "reasoning about programs" is more computer-science than "writing programs," and choosing an imperative language signals that you're not emphasizing the former.