Elektrine
Log in Register
Paige Chat Timeline Gallery Friends Email Drive DNS Private DNS Domains VPN Kairo Nerve
Remote

Lane

@lne@social.praxis.nyc
mastodon 4.7.3
  • Open on social.praxis.nyc

interested in next generation type theories, braided monoidal categories, and graphical computation frameworks, based in san francisco

33 Followers
123 Following
10 Posts
Joined August 10, 2023
interests:
type theory, category theory, graphical models of computation, compiler design and implementation
gh:
https://github.com/lane-core/kitcat
Open post
Lane @lne@social.praxis.nyc
· 1mo ago

It's rare to see this level of clarity from economic papers on politics, but refreshing nonetheless:

"We consider a model of automation embedded in a political environment where workers can undertake a revolt ... we show that, starting in a democracy, capital accumulation and thus greater automation encourages the capitalists to support a coup against democracy and set up a repressive system."

https://www.nber.org/papers/w35336

Automation and Repression
NBER

Automation and Repression

Founded in 1920, the NBER is a private, non-profit, non-partisan organization dedicated to conducting economic research and to disseminating research findings among academics, public policy makers, and business professionals.

3
1
1
0
Open post
Lane @lne@social.praxis.nyc
· 2mo ago

A suitable statement of my wager for so-called Virtual Graph Theory:
"Ordinarily one first defines a category, equips it with monoidal structure, and only thereafter introduces braidings, dualities, twists, and the other phenomena of tortile geometry as additional structure. We proceed in essentially the opposite direction. We take the geometry underlying tortile structure as fundamental, and recover ordinary categorical composition and coherence as a degeneration of it."

1
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 6mo ago
Replying to
@mralancooper i imagine that we are confronted again and again with the principle that an interface is defined by what it enables just as much as by what it constrains
3
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 6mo ago

What if the core insight of Duff's rc shell (Plan 9, Bell Labs), taking the sequence instead of strings as the primitive object, can be interpreted with virtual double categories as the semantic frame and sequent calculus as the type theory of its morphisms? I'm not entirely sure yet, but I am optimistic about what may lie in this interpretation for the shell, an often maligned setting of computation.

0
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 6mo ago

what if the system shell was a tool that always suffered from not knowing its semantics were best described by sequent calculus?

0
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 6mo ago

If we lived in a society that used automation to free everyone from material needs, we might be able to appreciate that having a reproducible example of a god awful/irresponsible coder/user would help us foresee the worst possible mistakes to make in systems engineering. Such could only before be discovered before at considerable expense, or when code was actually being used in live production where mistakes come at a much higher price. Claude Code ironically demonstrates this last anti-pattern

0
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 6mo ago

When designing a program that is a dependency for other programs, one must take a lot of care in how much of the overall plan for implementation is realized before it is recommended for public use. Even if further revisions are additive, the kinds of programs that people will make utilizing a system existing at one stage of implementation will vary from what they might make using the more realized system. If your system has two phases P1 and P2: Prog(P1 + P2) != Prog(P1) + Prog(P2) in general

0
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 2mo ago

@MartinEscardo@mathstodon.xyz There is nothing magical about language here. I think that if next-token-prediction is successful it is because there is some structure inherent to the ways in which one must proceed in any given situation, which tends to be preserved in the description of scenarios narrated by various sorts of discourses; in particular the ones that make sensible the lived experiences of historic actors in various disciplines, which they rely upon when confronted by various decisions.

0
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 2mo ago

its pretty wild (no pun intended) that one cool trick (representability predicates) allows you to derive the pentagon and triangle coherences in untruncated hom types in higher #category-theory in #hott. its even nicer that this trick straightforwardly generalizes to monoidal categories and allows you define both levels of monoidal structure, braided structures, and even goes on to derive the hexagon coherence. all proven in cubical agda.

0
0
0
0
Open post
Lane @lne@social.praxis.nyc
· 3mo ago

From Girard. The difficulty arises from conceiving of the coherent action of connectives "and" and "or" -- but what if the problem is a matter of a lacking expressiveness by having these connectives perform double duty? It's no coincidence these orderings are precisely what's at stake in Yang-Baxter, which gives a pleasing geometric angle that Girard almost begins to consider: we might consider what happens when an A entangled with a B then becomes entangled with C, or the alternative.

0
1
0
0
Back
313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

I2P eepsite

j6b6cyk6gjmepjih7jjadxgxvvf3lzzujljuu2v4biemzpg3naya.b32.i2p

Platform

  • Email
  • Chat
  • Timeline
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ
  • Lite (no JS)

Legal

  • Terms of Service
  • Privacy Policy
  • Transparency Report
  • Report Abuse
  • Warrant Canary
  • VPN Policy

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 10:29:50 UTC