Toots for isAdisplayName@mathstodon.xyz account

Written by Raymond on 2025-01-15 at 00:34

"hey, popl is in Denver. That's right nearby, why don't I try going."

• looks at prices*

"wtf"

=> More informations about this toot | View the thread

Written by Raymond on 2024-11-28 at 20:09

two questions about agda libraries:

(i) does anybody know of existing agda libraries that build out the basic infrastructure of codata, solely using coinductive record types? Or maybe even some libraries that go further and set up IO in terms of coinductive record types?

(ii) what about active parsing agda libraries? I know there is agdarsec by @gallais , but it looks like its still on agda 2.6.2. Any such libraries that have infrastructure for working with streams of data, using coinductive records?

=> More informations about this toot | View the thread

Written by Raymond on 2024-11-11 at 01:14

Using haskell as my main language at work is pretty great, except for one thing. Having learned agda first, I got really used to having dependent types at my disposal. Now I often find myself naturally thinking of a solution that makes use of dependent types, then having to translate this solution into haskell. Of course, there is always a translation. But the translation may obfuscate what the code is doing, making it harder for future programmers to understand it and maintain it.

The work I do has no relation to formal verification, nor is it "mission critical" that the code is correct. But I still find my self wishing I could use dependent types, just because they make writing programs and capturing business logic both faster and easier. A language with dependent types requires a less severe translation from the programmers ideas to a compiling program.

=> More informations about this toot | View the thread

Written by Raymond on 2024-09-30 at 02:43

odd. Its called JavaScript but it feels much more like JavaImprov

=> More informations about this toot | View the thread

Written by Raymond on 2024-09-29 at 18:53

when ever I end up need some basic lemma, and its not already in agda-unimath, I have to stop and think, has it simply been the case that no one else has needed this lemma before, or have I messed up four hours ago and no one should need this lemma?

=> More informations about this toot | View the thread

Written by Raymond on 2024-09-14 at 22:47

man, univalent group theory is so nice. Everything just... works, and in such a straight forwards and simple way. The things that you normally need to create equivalence classes to equate in classical group theory are just straight up equal in some obvious structure in univalent group theory. Good stuff

=> More informations about this toot | View the thread

Written by Raymond on 2024-08-24 at 20:19

Lenses are coalgebras for the costate comonad. Prisms are...? What?

=> More informations about this toot | View the thread

=> This profile with reblog | Go to isAdisplayName@mathstodon.xyz account