A followup: in the end I got a working evaluator and normaliser of λ-calculus using my fast free monad and HOAS in the form of
data Lam = Var String | App Lam Lam | Abs (String -> Lam)
In this way, capture-avoiding substitution can still be just reckless substitution as along as we always concretize a binder String -> Lam with free variables. I believe this is also the algorithmic content of Jamie Gabbay's haskell implementation of nominal sets.
The code is still in this gist: https://gist.github.com/yangzhixuan/07c2b3abf676b797cdfa0e77aa7700e8
The code can be improved in a lot of ways, but next I hope I can understand better how it works algorithmically and show that it is asymptotically as efficient as NbE (well, when you bind a closure in the environment in NbE, it is sort of a lazy substitution, right?)
=> More informations about this toot | View the thread
Can I ask a question as an absolutely novice language implementor? Suppose I want to implement a substitution-based evaluator of some language. After parsing a term into a syntax tree, can I just rename binders in the program to make sure no binders use the same variable name, and then
just forget about capture avoidance when substituting?
(As for why I am doing this: I am playing with a representation of free monads that has amortised constant-time-per-variable substitution and constant-time case analysis, so I'd like to see how fast a stupid evaluator can be if the underlying data structure is clever)
=> More informations about this toot | View the thread
The wall looks great with the light from the shiny big house behind it!
=> More informations about this toot | View the thread
Today's KEXP performance by Chinese Football https://www.youtube.com/watch?v=muKlPCWCK4s is the best live performance that I have seen for years. The last part with the melodica and everyone playing the drum together is incredible.
=> More informations about this toot | View the thread
If you're using Mastodon you probably don't have an X account. I still have an anonymous read-only X account to read news censored in China, and I have some news from that platform for you. Good news: someone wants to 'liberate the people of Britain'. Bad news: someone is Musk🤣
=> More informations about this toot | View the thread
The technique introduced in this paper https://arxiv.org/abs/2103.06195
and this blog https://acatalepsie.fr/posts/overloading-lambda.html is really cool! It lets you write an expression in linear/ordinary Haskell and 'desugar' it to any user-defined monoidal/cartesian category.
Very surprisingly to me, everything can be done without any compiler hacking!
=> More informations about this toot | View the thread
TIL: if a governmental web service isn't working, don't try to debug it by sending HTTP requests manually.
My UKVI e-visa account is in a strange state now💀
=> More informations about this toot | View the thread
Today I learnt: Impact Factors of journals are computed simply by the number of total citations divided by the number articles within a year. What a great metric to measure impact of journals!
=> More informations about this toot | View the thread
https://www.imperialcollegeunion.org/activities/a-to-z/imperial-college-communists
"Imperial College Communists" 🤣 I didn't believe it was real when I heard about it. Is it "Communism with British Characteristics"?
=> More informations about this toot | View the thread
So there is not just the University of Bath, but also Bath Spa University. What's next? Bath Spa Skin-care University?
=> More informations about this toot | View the thread
The majority of east Asian countries are dictatorships right now. What a time to live!
=> More informations about this toot | View the thread
My daily job.ac.uk joke: an AI research group is called iBUG. No wonder iOS is getting buggier!
=> More informations about this toot | View the thread
🤣 "Pre-Doctoral Research Fellow". Should I be glad to see this kind of role is now a real job? I do wonder if "competitive salary" means minimum wage + ε though
=> More informations about this toot | View the thread
Cute category theory/functional programming discovery today:
You might know that in the category of sets, free monoids can be constructed as lists. More precisely, for a set A the initial A-cons algebra μX. 1 + A × X can be equipped with a monoid structure <[ ], ++> and it is the free monoid over A. However, the definition of ++ actually uses the fact that Set is cartesian closed, so if we are in a category that is not cartesian closed, the initial A-cons algebra may not be the free monoid.
Indeed, the category Mon of (ordinary) monoids is complete and cocomplete but not cartesian closed. By the Eckmann-Hilton argument (https://ncatlab.org/nlab/show/Eckmann-Hilton+argument), a monoid object in Mon is precisely a commutative monoid, so free monoid over an object M ∈ Mon is quotienting M with commutativity equations.
However, in Mon, the initial M-cons algebra μX. 1 + M × X is different! Explicitly, elements of it are finite sequences <m_1, m_2, ..., m_n> considered up to trailing zeros (by which we mean <m_1, m_2, ..., m_n> and <m_1, ..., m_n, e, e, ..., e> are considered the same where e is the unit element of M). The unit element is the empty sequence <> and the multiplication is levelwise multiplication (after suitable padding with trailing zeros):
<m_1, m_2, ..., m_n> . <m'_1, m'_2, ..., m'_n> = <m_1 m'_1, m_2 m_2', ..., m_n m'_n>.
Therefore in the category Mon, initial cons algebras and free monoids are different. Moreover, if we do this funny-looking initial cons algebra in the category of applicative functors (which are monoids for the Day tensor), it is exactly the phased computation datatype by Jeremy Gibbons, Donnacha Oisín Kidney, Tom Schrijvers & Nicolas Wu
in their paper https://link.springer.com/chapter/10.1007/978-3-031-16912-0_1
=> More informations about this toot | View the thread
Let ρ : C^op × D → Set be a profunctor. The presheaf category over the collage of ρ is precisely the Artin gluing of Pr C and Pr D along the functor (A : Pr C) ↦ (d : Dºᵖ) ↦ Hom(ρ(-, d), A). How could I miss this simple description this long?!
(The collage of ρ is the category whose objects are the disjoint sum of ObC and ObD and
Hom(c',c) = C(c',c) Hom(d, d') = D(d, d'),
Hom(c,d) = ρ(c,d) Hom(d, c) = ∅.)
=> More informations about this toot | View the thread
In the UK sometimes you can find used books that are in almost perfect condition except that there's a "DAMAGED" stamp on the copyright page, for example, I recently bought such a copy of Continuous Lattices and Domains for "only" £40 (new copies are more than £200).
Does anyone know where such "damaged" copies may come from? Why does someone want to put a "DAMAGED" stamp on a perfect hardcover book?
=> More informations about this toot | View the thread
This is the printing quality of a book costing 48 GBP. My dad's home printer 20 years ago is better than this. Academic publishing companies are so good at turning beautifully written books into craps.
=> View attached media | View attached media
=> More informations about this toot | View the thread
Haven't had some proper tea for years!
=> More informations about this toot | View the thread
=> This profile with reblog | Go to zyang@mathstodon.xyz account This content has been proxied by September (ba2dc).Proxy Information
text/gemini