Owen Lynch

I've decided to leave twitter by changing my password and then deliberately forgetting it, so that my old tweets remain up but I will no longer have access to my account. You can find me on localcharts.org or @olynch" target="_blank" rel="nofollow noopener">mathstodon.xyz/@olynch.

@arntzenius nix-shell -E 'with import <nixpkgs> {}; mkShell { buildInputs = [(haskellPackages.ghcWithPackages (hpkgs: with hpkgs; [random]))]; }'

I want to generate random numbers in Haskell for some exploratory programming. There's a `random` package to do this. Is there a way to use it without needing to create a goddam "project" with "dependencies"?

Today I learned about the HTML <q> element, which is used for inline quotations and has the neat property that when you nest, it can change from double quotes to single quotes! developer.mozilla.org/en-US/docs/Web…

I wrote about the philosophy that underlies Topos Institute modeling software: topos.site/blog/2024-10-3…. Also, it's a job ad; see the end for details!

@kmett @joseph_h_garvin Oh yeah, definitely the getter/setter life is not fun. I mainly was thinking about newtypes like newtype Positive = MkPositive Int toInt :: Positive -> Int fromInt :: Int -> Maybe Positive

I agree about making most things immutable where it makes sense is helpful for concurrency, but I endeavor to leave everything internal wide open regardless, because maintaining private internals in c or java is usually a path to 3x-7x as many lines of code for every thought you go to think when you factor the cost to build getter/setter pairs, etc. in exchange for _very_ limited refactoring gain, all paid fully in advance all based on the hypothesis users won't #define private public In C++ you also lose a lot of the benefits you get from having the structure be trivially constructible plain-old-data by loading down the constructor. (This calculus changes for types used for RAII, etc. though.) In general I'd rather fit more code on my screen and pretend private was a post-Smalltalk fever-dream delusion about how such encapsulation was desirable in practice and without cost. Your complex number type isn't going to refactor cleanly between polar coordinates and linear coordinates, the behavior at 0 will show through. Make two types, make a common concept so you can pass them to code that doesn't care, define interconversions, go about your day. If you have invariants by all means capture them as static_asserts or requires clauses whenever possible, though.

"Make illegal states unrepresentable" I do when I can but almost all language support for this is incredibly weak. Can you lang express that a struct with two sum type fields can never both be the same value? Can you express one integer field must always be greater than another?

@alicemazzy My nixos setup has every folder that is not explicitly marked in my config to back up deleted on every boot (because my / is a tmpfs). So every reboot is the new install experience. NixOS is the way.

guys if I want to complete the transition from "I have a server and vpn" to "my laptops are functionally disposable because I can reprovision new ones at will" should I start using nixos or just learn ansible

@joseph_h_garvin @mattecapu Look, once ATS Xanadu github.com/githwxi/ATS-Xa… or CFTT andraskovacs.github.io/pdfs/2ltt_icfp… become real, I'll be as happy as the next guy. But I'm not holding my breath.

@u_map_prop @mattecapu Slower to write or slower to run? I personally like when runtime checks are elided

@mattecapu @joseph_h_garvin When I want to write 10x as much code and go 100x slower, sure!

@u_map_prop @joseph_h_garvin or embrace a rich dependent type system

@Ayegill The framework is pretty good!

Send me your linux laptop recommendations

@arntzenius @tangled_zans @jhemann I'm not 100% confident, but I do know that there's a lot of cool coinductive type stuff going on there. It's definitely not production-ready though.

@u_map_prop @tangled_zans @jhemann No, you mean github.com/mikeshulman/na…? I hadn’t heard of it before. Are you confident this would work there? Otherwise I’ll probably not try given how experimental it looks - I don’t like writing code and discovering it’s no longer working a year later :P.

Most lazy stream implementations are synchronous: one delay between each element, eg: data Stream a = Nil | Cons a (Delay (Stream a)) where Delay x = () -> x, for instance. But miniKanren instead uses *asynchronous* streams, with arbitrary delays between elements. [1/n]

@arntzenius @tangled_zans @jhemann Have you tried narya?

@tangled_zans @jhemann How does Idris do coinduction? In Agda the coinductive stuff isn't powerful enough out of the box and I had to use --guarded, which is a bit underdocumented & experimental: docs: agda.readthedocs.io/en/v2.7.0/lang… my implementation of the mukanren search strategy: gist.github.com/rntz/c2996e063…

This specific feature, the graph-rewriting, is enabled by the local mode that Yaron is talking about: it ensures that no reference to the graph escapes into the runtime of your app, so the graph can't be mutated after the startup of your app.

So far, the only UI library I know that explicitly support Mealy machines, and that does a graph-rewriting pass to optimize how state propagates through your app.

And you can play around with the new Cont-based bonsai interface! Some really cool design here: github.com/janestreet/bon…, github.com/janestreet/bon….

@mattecapu @obsdmd Alright, this will be my impetus to make silviculture good

@u_map_prop @obsdmd sorry but obsidian's ecosystem is so alluring 🥺

switching to @obsdmd for my research notes (was able to export from Notion seamlessly), any plugins/architectures reccomendations?

My “Scoped Propagators” submission to LIVE got accepted! Thank you to the reviewers for the incredibly thoughtful and useful feedback!

@jtcbrule @krismicinski I mean, maybe "mainstream programming languages" have copied all the good stuff from... lisp 40 years ago. But there are tons of modern lisp dialects that have new stuff! Like correct handling of lexical scope for macros in Racket youtube.com/watch?v=ABWLve…

@krismicinski @u_map_prop Lisp is... weird. The Lisp hackers were right that their language was superior, more "mainstream" programming languages spent the next 40 years copying the good stuff from Lisp and now, finally, Lisp isn't really that special.

This is a common misunderstanding. Zig's comptime features are quite *different* than macros, despite both nominally running at compile time. 🧵

@krismicinski Not true! I'm a lisp fan and I don't think this!