burakemir

7 ms·

31.
by burakemir 1y ago
No. A phantom type is a type whose only use is to communicate a constraint on a type variable, without having a runtime value that corresponds to it. Typestate is a bit closer: it communicates some property where an operation (typically a m
32.
by burakemir 1y ago
The paper "Linearity and Uniqueness: an entente cordiale" by Marshall,Vollmer,Orchard offers a good discussion and explanation of the "opposite convention" you describe. There is a dual nature of linearity and uniqueness
33.
by burakemir 1y ago
A definition of memory safety without data race freedom may be more precise but arguably less complete. It is correct that data races in a garbage collected language are difficult to turn into exploits. The problem is that data races in C a
34.
by burakemir 1y ago
Two big differences: - it is typed, and - multi-stage programming can also describe runtime-code generation.
35.
by burakemir 1y ago
Enjoyed this, but looking at these from manager decision scenario is of course going to bias towards the more subjective. For a different scenario, imagine you operate a large distributed system and have been paged at 3 am because there is
36.
by burakemir 1y ago
I made some progress porting mangle datalog to Rust https://github.com/google/mangle/tree/main/rust - it is in the same repo as the golang implementation. It is slow going, partly since it is not a prior
37.
by burakemir 1y ago
Common Table Expression, a SQL concept that enables more expressive programming with SQL queries. They are introduced using WITH ...
38.
by burakemir 1y ago
One angle (no static types) is racket, which knows multiple stages for its macros. Maybe the most developed actually working "new tradition". Researchers have also looked into multistage programming, which is enabled by representi
39.
by burakemir 1y ago
https://blog.rust-lang.org/2025/04/04/c-abi-changes-for-wasm...
40.
by burakemir 2y ago
It is consistent with the way the Rust community uses "safe": as "passes static checks and thus protects from many runtime errors." This regularly drives C++ programmers mad: the statement "C++ is all unsafe" i
41.
by burakemir 2y ago
In an attempt to get a more general version of a debt metaphor, let's look at ingredients: - there is a time interval - we have a utility function, or at least desire one or want to pretend we have one - there is a decision - there is
42.
by burakemir 2y ago
Hi Steven, I will check it out. What I like about Cardelli's handbook article is how he lays down type systems in programming languages as its own thing. This is inspired by logic but definitely not the same - just as mathematical logi
43.
by burakemir 2y ago
From a quick glance at the article, this looks like an interesting linguistic exploration into terminology around "type". It is questionable that such an approach is ultimately effective at getting us closer to a standard meaning,
44.
by burakemir 2y ago
Dependent types typically refers to type systems where a type can depend on a term. The canonical example is "Vector n" where n is some expression that evaluates to a natural number. Refinement types typically(1) refers to a type
45.
by burakemir 2y ago
Agreed. The large and passionate community may have multiple factors but "things actually work" is probably a factor. It is hard to get a full picture of how academic research influenced Rust and vice versa. Two examples: - The us
46.
by burakemir 2y ago
In other words: you encode them. That is likely also the reason why many programming languages did not have sums. You have something else that can be used similarly. A sum type is a disjoint union so a straightforward encoding of A+B would
47.
by burakemir 2y ago
Not bad, an article aiming to popularize product and sum types. I am not the target audience, but wished there was a way to get the masses to understand that elementary type theory and logic are at the heart of these programming concepts th
48.
by burakemir 2y ago
Generics are a powerful mechanism, and there is a spectrum. The act of retrofitting generics on go without generics certainly meant that some points in the design space were not available. On the other hand, when making a language change as
49.
by burakemir 2y ago
The Mangle repo has the beginnings of a Rust implementation but it will take some time before it is usable. The go implementation is also still being improved, but I think real DB work with persistent data will happen only in Rust. Bindings
50.
by burakemir 2y ago
Here is a proof that you can translate non-recursive datalog into relational algebra and vice versa: https://github.com/google/mangle/blob/main/docs/spec_explain... Since Logica is translated to SQL
51.
by burakemir 2y ago
"In summary, it is highly misleading to suggest that Microsoft (or ICOMP) initiated or in any way controlled Foundem’s European complaint or any of Foundem’s other initiatives." Source: http://www.searchneutrality.org&#
52.
by burakemir 2y ago
I am sure Clojure is great but it really shows the need for an "overview of datalog" that is not embedded in the context of a programming language with it's own syntactic choices. My own humble attempt is here https:/&
53.
by burakemir 2y ago
In addition to labelled property graphs and triples, a list of approaches to knowledge graph should consider facts(tuples) that are connected via common values as a form of graph, with datalog queries to query them. This is a lot more flexi
54.
by burakemir 2y ago
For the subproblem of being able to unify and query various data sources in different formats, I would suggest to take a look at Datalog and specifically Mangle, my implementation of it. I don't want to plug the project here but more d
55.
by burakemir 2y ago
Interesting! IIUC this is done using source-to-source translation? It is a bit hard to understand from the docs what technical approach is. The docs are clearly aimed at users and I find them impressive, well done. I'd be interested in
56.
by burakemir 2y ago
Really appreciate the bits in the article about identifying what is fundamental and correcting misevaluations. Making an outline is also important for writing. However doing research also has its place. See this here https://cse.
57.
by burakemir 2y ago
Let's define a mapping F to act as a "signature-step" of an algebraic data type with operations op as a map (functor) from X to Sum_op X^arity(op). This involves a sum of products (or coproduct of products). See "Recurs
58.
by burakemir 2y ago
Mangle is a language that includes "textbook datalog" as a subset https://github.com/google/mangle ; like any real-world datalog language, it extends datalog with various facilities to make it practical. It w
59.
by burakemir 2y ago
Negation is not all that well understood even in formal settings. When PROLOG introduced negation-as-failure, many logicians (Girard) were repulsed: how can failure to find a proof for a proposition P be considered a proof of the negation (
60.
by burakemir 2y ago
There are people who argue that after the horrible events of the 20th century, the time has come to stop pretending that science could be an "objective" universal pursuit of truth and accept that it's results can at any point

More ›