Structuring Arrays with Algebraic Shapes [video]

Comments (1)

thesz · 2h 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.

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

Perl Versioning Scheme and Gentoo (wiki.gentoo.org)

The Daily Life of a Medieval King (medievalists.net)

Quadratic Forms Beyond Arithmetic (ams.org)

Staying cool without refrigerants: Next-generation Peltier cooling (news.samsung.com)

Log by time, not by count (johnscolaro.xyz)

The sumerian game early computer game (spillhistorie.no)

Extend (YC W23) is hiring engineers to build SOTA document processing (jobs.ashbyhq.com)

ESP32-Faikin: ESP32 based module to control Daikin aircon units (github.com)

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

XMLUI (blog.jonudell.net)

Show HN: X11 desktop widget that shows location of your network peers on a map (github.com)

XSLT: A Precision Tool for the Future of Structured Transformation (xml.com)

Agents built from alloys (xbow.com)

Debugging Bash Like a Sire (2023) (blog.brujordet.no)

Super-resolution microscopes reveal new details of cells and disease (knowablemagazine.org)

Simulating hand-drawn motion with SVG filters (camillovisini.com)

Ryanair may increase commission to staff identifying oversized cabin bags (rte.ie)

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

Structuring Arrays with Algebraic Shapes [video] (youtube.com)

Stdio(3) change: FILE is now opaque (undeadly.org)

Using the Matrix Cores of AMD RDNA 4 architecture GPUs (gpuopen.com)

Show HN: Conductor, a Mac app that lets you run a bunch of Claude Codes at once (conductor.build)

How to handle people dismissing io_uring as insecure? (2024) (github.com)

Hexanitrogen Energies (science.org)

AI is killing the web – can anything save it? (economist.com)

Speeding up my ZSH shell (scottspence.com)

What my mother didn’t talk about (2020) (buzzfeednews.com)

IPv6 Based Canvas (canvas.openbased.org)

How slow motion became cinema’s dominant special effect (newrepublic.com)

SIOF (Scheme in One File) – A Minimal R7RS Scheme System (github.com)

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

Subreply – An open source text-only social network (github.com)

Digital vassals? French Government ‘exposes citizens’ data to US' (brusselssignal.eu)

JOVE – Jonathan’s Own Version of Emacs (github.com)

A Tour of Microsoft's Mac Lab (2006) (davidweiss.blogspot.com)

Insights on Teufel’s first open-source speaker (blog.teufelaudio.com)

We benchmarked Cyberpunk 2077 on Mac M1 to M4 – the numbers don't lie (tomsguide.com)

Tell me again about neurons now (science.org)

Async I/O on Linux in databases (blog.canoozie.net)

Logical implication is a comparison operator (btdmaster.bearblog.dev)

The Minecraft game score unexpectedly became big business for its composer (billboard.com)

Hacking a Toniebox (schafe-sind-bessere-rasenmaeher.de)

Peep Show is the most realistic portrayal of evil I have seen (2020) (mattlakeman.org)

The old Caveman Chemistry website (1996-2000) (cavemanchemistry.com)

Java was not underhyped in 1997 (2021) (dylanbeattie.net)

Why not to use iframes for embedded dashboards (embeddable.com)

What birdsong and back ends can teach us about magic (digitalseams.com)

A human metaphor for evaluating AI capability (mathstodon.xyz)

The Genius Device That Rocked F1 (youtube.com)

Structuring Arrays with Algebraic Shapes [video]

Comments (1)