Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.

Administered by:

Server stats:

8.1K
active users

mastodon.world: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.3

#agda

5 posts4 participants0 posts today
José A. Alonso<p>Readings shared August 25, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/26-readings_shared_08-25-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/08/26-readings_shared_08-25-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RustLang</span></a> <a href="https://mathstodon.xyz/tags/Waterproof" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Waterproof</span></a></p>
José A. Alonso<p>Big-stop semantics: A simple way to get the benefits of small-step semantics in a big-step judgment. ~ David M Kahn, Jan Hoffmann, Runming Li. <a href="https://arxiv.org/abs/2508.15157v1" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2508.15157v1</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared August 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/24-readings_shared_08-23-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/08/24-readings_shared_08-23-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Decidable equality for indexed data types, take 2. ~ Brent Yorgey. <a href="https://byorgey.github.io/blog/posts/2025/08/22/OneLevelTypesIndexed2.lagda.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">byorgey.github.io/blog/posts/2</span><span class="invisible">025/08/22/OneLevelTypesIndexed2.lagda.html</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a></p>
José A. Alonso<p>Readings shared August 22, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/23-readings_shared_08-22-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/08/23-readings_shared_08-22-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Continuous and algebraic domains in univalent foundations. ~ Tom de Jong, Martín Hötzel Escardó. <a href="https://arxiv.org/abs/2407.06956" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2407.06956</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
Tom de Jong<p>My paper "Continuous and algebraic domains in univalent foundations" with <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>MartinEscardo</span></a></span> was accepted for publication by the Journal of Pure and Applied Algebra! 🎉 <br><a href="https://arxiv.org/abs/2407.06956" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2407.06956</span><span class="invisible"></span></a></p><p>This paper has its origin in my very first paper with Martín (and my second paper overall) "Domain Theory in Constructive and Predicative Univalent Foundations" which appeared at Computer Science Logic (CSL) back in 2021.</p><p>Since then I wrote my PhD thesis on this topic (and worked on other things in type theory after) and the present paper is a revision of both the CLS'21 paper and my PhD thesis (which I completed in 2022).</p><p>Everything in the paper has been formalized and an HTML rendering of the Agda file that directly links the code to the paper can be found here: <a href="https://cs.bham.ac.uk/~mhe/TypeTopology/DomainTheory.Continuous-and-algebraic-domains.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cs.bham.ac.uk/~mhe/TypeTopolog</span><span class="invisible">y/DomainTheory.Continuous-and-algebraic-domains.html</span></a></p><p><a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>typetheory</span></a> <a href="https://mathstodon.xyz/tags/agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>agda</span></a> <a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>logic</span></a> <a href="https://mathstodon.xyz/tags/math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>math</span></a> <a href="https://mathstodon.xyz/tags/computerscience" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>computerscience</span></a></p>
Roger Sen<p>This makes an interesting reading for the afternoon:</p><p>Policy as Code, Policy as Type</p><p><a href="https://mastodon.social/tags/Policies" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Policies</span></a> are designed to distinguish between correct and incorrect actions; they are types. We demonstrate how even the most complex ABAC policies can be expressed as types in dependently typed languages such as <a href="https://mastodon.social/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> and <a href="https://mastodon.social/tags/Lean" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean</span></a>, providing a single framework to express, analyze, and implement policies.</p><p><a href="https://arxiv.org/abs/2506.01446" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.01446</span><span class="invisible"></span></a></p><p>I mean, it makes completely sense, but someone had to write the paper.</p>
José A. Alonso<p>Readings shared August 18, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/19-readings_shared_08-18-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/08/19-readings_shared_08-18-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RustLang</span></a></p>
José A. Alonso<p>Formal correctness proofs for efficient CHAD. ~ Benjamin Meijs. <a href="https://studenttheses.uu.nl/bitstream/handle/20.500.12932/49742/ThesisBenjamin.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">studenttheses.uu.nl/bitstream/</span><span class="invisible">handle/20.500.12932/49742/ThesisBenjamin.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared August 17, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/18-readings_shared_08-17-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/08/18-readings_shared_08-17-25</span></a> <a href="https://mathstodon.xyz/tags/Abella" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Abella</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Counterpart-based quantified temporal logics. ~ Fabio Gadducci, Andrea Laretto, Davide Trotta. <a href="https://www.sciencedirect.com/science/article/abs/pii/S2352220825000483" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">sciencedirect.com/science/arti</span><span class="invisible">cle/abs/pii/S2352220825000483</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared August 10, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/11-readings_shared_08-10-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/08/11-readings_shared_08-10-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CoqProver</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/OCaml" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>OCaml</span></a></p>
José A. Alonso<p>Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. <a href="https://www.cambridge.org/core/journals/journal-of-functional-programming/article/binary-searchthink-positive/1F974DF9C6475D19B32E18C93A2DCC1C" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">cambridge.org/core/journals/jo</span><span class="invisible">urnal-of-functional-programming/article/binary-searchthink-positive/1F974DF9C6475D19B32E18C93A2DCC1C</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a></p>
amen zwa, esq.<p><a href="https://mathstodon.xyz/tags/Stump" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Stump</span></a>'s "Verified Functional Programming in <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a>" is a CS undergrad-accessible text on software verification and a decent Agda tutorial, both of which are rather intricate subjects.</p><p>As software complexity increases and the software use expands ever deeper into life-critical domains, the reliance on <a href="https://mathstodon.xyz/tags/verified" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>verified</span></a> <a href="https://mathstodon.xyz/tags/programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>programming</span></a> must commensurately rise. Sadly, with <a href="https://mathstodon.xyz/tags/IT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IT</span></a> practitioners surrendering, in droves, to LLM code generators, the concept of "reliable software" has become yet another victim of AI.</p><p><a href="https://www.amazon.com/Verified-Functional-Programming-Agda-Books/dp/1970001240" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">amazon.com/Verified-Functional</span><span class="invisible">-Programming-Agda-Books/dp/1970001240</span></a></p>
José A. Alonso<p>Readings shared July 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/28-readings_shared_07-27-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/07/28-readings_shared_07-27-25</span></a> <a href="https://mathstodon.xyz/tags/AI4Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI4Math</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistants</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Rocq</span></a></p>
José A. Alonso<p>Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. <a href="https://repository.tudelft.nl/file/File_56e70e9e-4f41-429c-a383-20c1bf61c16a" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">repository.tudelft.nl/file/Fil</span><span class="invisible">e_56e70e9e-4f41-429c-a383-20c1bf61c16a</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistant" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. <a href="https://repository.tudelft.nl/file/File_6466eb89-91b7-4561-9933-236ae3f9e15b" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">repository.tudelft.nl/file/Fil</span><span class="invisible">e_6466eb89-91b7-4561-9933-236ae3f9e15b</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistant" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a></p>
lxsameer<p>I owe a lot to a few programming languages that taught me how to design a language, both from an engineering standpoint and computer science. </p><p><a href="https://mastodon.social/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</span></a> &amp; <a href="https://mastodon.social/tags/haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>haskell</span></a> for what a good programming language might look like. </p><p><a href="https://mastodon.social/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a>, <a href="https://mastodon.social/tags/Idris2" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Idris2</span></a>, <a href="https://mastodon.social/tags/lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lean4</span></a> to show me how useful dependent types are.</p><p><a href="https://mastodon.social/tags/C" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>C</span></a>++, to teach me what to avoid</p><p><a href="https://mastodon.social/tags/python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>python</span></a>, <a href="https://mastodon.social/tags/javascript" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>javascript</span></a> to be such giant examples of shitty languages and give me hope that I can do better. 😂</p>
HoldMyType<p>Impredicativity and existential quantifiers : r/haskell<br><a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> had first-class forall a long time ago, without any special effort expended on type inference support. Assuming bidirectional checking, which AFAIK GHC follows, forall and exist are both trivial to handle when checking types are known. Issues arise only when checking types are metavariables (i.e. unknown or perhaps partially known). In slightly older versions of Agda, in these problematic cases we simply had to write some lambdas by hand (most recent Agda employs some extra magic which I don't yet fully grasp). For example, instead of the equivalent of the following pseudo-GHC code</p>
TrendingLive feeds
About