Hacker News: wisnesky

New comment by wisnesky in "Formal Reasoning [pdf]"

wisnesky — Sun, 26 Oct 2025 19:41:19 +0000

That's the approach we're taking to verify LLM-generated SQL code at http://sql.ai.

New comment by wisnesky in "Graphs Are Programs"

wisnesky — Thu, 14 Aug 2025 17:38:15 +0000

Hydra is a programming language that uses mathematical abstraction to model graphs within the language itself. It’s an open-source project spearheaded by Josh Shinavier, co-creator of Apache TinkerPop. In Josh’s own words: “In Hydra, programs are graphs, and graphs are programs.”

Graphs Are Programs

wisnesky — Thu, 14 Aug 2025 17:38:15 +0000

Article URL: https://gdotv.com/blog/introducing-hydra/

Comments URL: https://news.ycombinator.com/item?id=44903324

Points: 4

# Comments: 1

New comment by wisnesky in "Semantic Search of SQL Code"

wisnesky — Thu, 17 Apr 2025 20:12:37 +0000

An open source project to search SQL code 'semantically': up to the meaning of parse trees. For example, searching for 'select from A,B' matches 'select from B,A'.

Sql Semantic Search

wisnesky — Thu, 17 Apr 2025 20:12:37 +0000

Article URL: https://github.com/CategoricalData/SqlSemanticSearch

Comments URL: https://news.ycombinator.com/item?id=43721675

Points: 2

# Comments: 1

New comment by wisnesky in "Code in Database vs. Code in Application"

wisnesky — Thu, 03 Oct 2024 00:45:58 +0000

The code in database vs database in code duality has a long history, and one way to formalize it mathematically uses category theory: the notion of LINQ (language integrated query, such as collection comprehensions) is formally related to the notion of "query-integrated languages" (where data integrity constraints are Turing-complete domain specific languages extending the database vocabulary). https://arxiv.org/pdf/1511.06459

New comment by wisnesky in "GPTs and Hallucination"

wisnesky — Tue, 10 Sep 2024 16:34:03 +0000

There is a partial solution to this problem: use formal methods such as symbolic logic and theorem proving to check the LLM output for correctness. We are launching a semantic validator for LLM-generated SQL code at sql.ai even now. (It checks for things like missing joins.) And others are using logic and math to create LLMs that don't hallucinate or have safety nets for hallucination, such as Symbolica. It is only when the LLM output doesn't have a correct answer that the technical issues become complicated.

New comment by wisnesky in "Ask HN: What is the current state of "logical" AI?"

wisnesky — Tue, 26 Dec 2023 17:07:02 +0000

Yes; categories extend traditional graphs with systems of equations. Hypergraphs extend traditional graphs by allowing edges to be between multiple nodes. Most operations on categories are formally undecidable because of the systems of equations; most operations on graphs/hypergraphs are decidable. This makes working with categorical databases a lot like doing computer algebra in e.g. Mathematica and provides a huge increase in expressive power (you can e.g. encode Turing machines with equations.)

New comment by wisnesky in "Ask HN: What is the current state of "logical" AI?"

wisnesky — Tue, 26 Dec 2023 16:44:21 +0000

At https://www.categoricaldata.net we claim that symbolic AI is also generative, when eg used in data warehousing. Instead of eg new images, the generatively gives you new primary and foreign keys, new ontologies, contradiction detection, etc.

New comment by wisnesky in "Applied Category Theory: Textbook (2019)"

wisnesky — Mon, 06 Nov 2023 15:56:54 +0000

We use it for data integration https://www.categoricaldata.net

New comment by wisnesky in "What do we mean by "the foundations of mathematics"?"

wisnesky — Wed, 01 Nov 2023 19:45:24 +0000

Yes, at least with a strong enough arithmetic (such as Peano's), but that is usually more complicated; for example, you might have to create a Godel numbering or some other "deep embedding" to represent each set as a number. There's also so-called "reverse mathematics", which tries to determine the weakest axiom system capable of establishing a particular result.

New comment by wisnesky in "What do we mean by "the foundations of mathematics"?"

wisnesky — Wed, 01 Nov 2023 19:33:57 +0000

A foundation for mathematics is any formalism sufficient to prove the results typically taken as axioms in practical mathematics. For example, in ZFC you can define numbers as sets in many different ways and prove that 1+1=2 for each of them - other foundations include higher order logic, topos theory, other set theories, etc.

New comment by wisnesky in "The deep link equating math proofs and computer programs"

wisnesky — Wed, 11 Oct 2023 17:31:16 +0000

Yes, although Dijkstra was interested in proving programs correct in general, not just in how lambda calculi correspond to logics correspond to categories (a proof technique for program correctness, among other things).

New comment by wisnesky in "Applied Category Theory Course"

wisnesky — Thu, 28 Sep 2023 20:41:05 +0000

We've used Poly to prove results about functorial data migration.

New comment by wisnesky in "Ask HN: Did studying proof based math topics make you a better programmer?"

wisnesky — Sat, 24 Jun 2023 22:59:50 +0000

Yes, in the sense that "math is programming paper instead of computers", being better at one translates to being better at the other. This intuition can even be made precise via the "Curry-Howard isomorphism", upon which "proof assistants" such as Coq are built.

New comment by wisnesky in "Category Theory Illustrated"

wisnesky — Sat, 18 Mar 2023 16:37:24 +0000

If you have a symmetric system, you can use group theory to make predictions about it. Similarly, if you have a compositional system, you can use category theory to make predictions about it. As for whether those predictions are useful, or non-obvious, or worth it, etc, tends to very a lot depending on the application, and the other techniques available- it's not a matter of being smart enough to get it. FWIW, I think category theory is certainly indispensable in denotational programming language semantics.

New comment by wisnesky in "Hydra: Type-aware transformations for data and programs"

wisnesky — Mon, 05 Dec 2022 21:43:31 +0000

Hydra is a transformation toolkit along the lines of Dragon (Uber), but open source, and with a more advanced type system and other new features. Hydra maps data and schemas between languages in a way which maintains type conformance. It will even map functional programs between selected languages, including parts of its own source code.

Hydra: Type-aware transformations for data and programs

wisnesky — Mon, 05 Dec 2022 21:43:31 +0000

Article URL: https://hackage.haskell.org/package/hydra

Comments URL: https://news.ycombinator.com/item?id=33872320

Points: 5

# Comments: 2

New comment by wisnesky in "Why I am learning category theory"

wisnesky — Thu, 01 Dec 2022 19:43:36 +0000

You might try pages 8-16 of this presentation: https://www.categoricaldata.net/cql/lambdaconf.pdf . The examples are relational to relational and simplistic but they do illustrate running the same transformation both forward and backward, as well as show the "unit" of such a "monad". We implemented everything in public software, so hopefully the software is even better than my word! As for loading SQL to RDF specifically, I'd be happy to share that technique, but it isn't public yet- please ping me at ryan@conexus.com.

New comment by wisnesky in "Why I am learning category theory"

wisnesky — Thu, 01 Dec 2022 10:47:17 +0000

Bi-directional data exchange has many uses. For example, given a set of conjunctive queries Q, because coeval_Q is left adjoint to eval_Q, the composition coeval_Q o eval_Q forms a monad, whose unit can be used to quantify the extent to which the original query Q is "information preserving" on a particular source (so query/data quality). As another example, we use the technique to load data into OWL ontologies from SQL sources, by specifying an OWL to SQL projection query (tends to be easy) and then running it in reverse (tends to be hard). But no doubt more applications await!