Structuring Arrays with Algebraic Shapes [video]

Comments (2)

thesz · 1d ago

Arithmetic inside the types not necessarily introduces undecidability. One example is telescopes for indices:

  data N where
    Z :: N
    O :: N -> N
  data T (n :: N) where
    TZ :: T (O n)
    TO :: T n -> T (O n)

To safely access an element in array you have to provide a proof that a telescope can be constructed for given index range.

bgavran · 1d ago

Indeed, the author seems to have a misunderstanding about both undecidability and complexity as they pertain to dependent types.

Dependent types do not add complexity to our system, they reveal it.

Case in point: here is a fully dependently-typed tensor processing framework written in Idris, which I believe matches most of the desiderata of his talk, capturing even a generalisation of arrays via Naperian functors that is mentioned at one point.

https://github.com/bgavran/TypeSafe_Tensors

LLM Inevitabilism (tomrenner.com)

Kiro: A new agentic IDE (kiro.dev)

Linux Reaches 5% Desktop Market Share in USA (ostechnix.com)

Valve confirms credit card companies pressured it to delist certain adult games (pcgamer.com)

Hyatt Hotels are using algorithmic Rest “smoking detectors” (twitter.com)

Global hack on Microsoft Sharepoint hits U.S., state agencies, researchers say (washingtonpost.com)

Reflections on OpenAI (calv.info)

ChatGPT agent: bridging research and action (openai.com)

Ukrainian hackers destroyed the IT infrastructure of Russian drone manufacturer (prm.ua)

Mistral Releases Deep Research, Voice, Projects in Le Chat (mistral.ai)

How to Firefox (kau.sh)

XMLUI (blog.jonudell.net)

Show HN: Shoggoth Mini – A soft tentacle robot powered by GPT-4o and RL (matthieulc.com)

My Self-Hosting Setup (codecaptured.com)

TrackWeight: Turn your MacBook's trackpad into a digital weighing scale (github.com)

Coding with LLMs in the summer of 2025 – an update (antirez.com)

Oakland cops gave ICE license plate data; SFPD also illegally shared with feds (sfstandard.com)

Cloudflare 1.1.1.1 Incident on July 14, 2025 (blog.cloudflare.com)

Death by AI (davebarry.substack.com)

New colors without shooting lasers into your eyes (dynomight.net)

Apple's MLX adding CUDA support (github.com)

Data brokers are selling flight information to CBP and ICE (eff.org)

Ask HN: Is it time to fork HN into AI/LLM and "Everything else/other?"

The United States withdraws from UNESCO (state.gov)

UK backing down on Apple encryption backdoor after pressure from US (arstechnica.com)

Nobody knows how to build with AI yet (worksonmymachine.substack.com)

Ex-Waymo engineers launch Bedrock Robotics to automate construction (techcrunch.com)

Gemini with Deep Think achieves gold-medal standard at the IMO (deepmind.google)

AccountingBench: Evaluating LLMs on real long-horizon business tasks (accounting.penrose.com)

Complete silence is always hallucinated as "ترجمة نانسي قنقر" in Arabic (github.com)

Cognition (Devin AI) to Acquire Windsurf (cognition.ai)

A 14kb page can load much faster than a 15kb page (2022) (endtimes.dev)

What went wrong inside recalled Anker PowerCore 10000 power banks? (lumafield.com)

OpenAI claims gold-medal performance at IMO 2025 (twitter.com)

Uv: Running a script with dependencies (docs.astral.sh)

I'm switching to Python and actually liking it (cesarsotovalero.net)

To be a better programmer, write little proofs in your head (the-nerve-blog.ghost.io)

I want an iPhone Mini-sized Android phone (2022) (smallandroidphone.com)

Self-taught engineers often outperform (2024) (michaelbastos.com)

Fully homomorphic encryption and the dawn of a private internet (bozmen.io)

Hand: open-source Robot Hand (github.com)

Fstrings.wtf (fstrings.wtf)

Tell HN: Notion Desktop is monitoring your audio and network

The current hype around autonomous agents, and what actually works in production (utkarshkanwat.com)

“Dynamic programming” is not referring to “computer programming” (vidarholen.net)

LLM architecture comparison (magazine.sebastianraschka.com)

The bewildering phenomenon of declining quality (english.elpais.com)

Anthropic tightens usage limits for Claude Code without telling users (techcrunch.com)

Altermagnets: The first new type of magnet in nearly a century (newscientist.com)

FFmpeg devs boast of another 100x leap thanks to handwritten assembly code (tomshardware.com)

Structuring Arrays with Algebraic Shapes [video]

Comments (2)