How we should be doing things in PLs:
Of course, untyped languages with great macro systems already do this, routinely. What's missing is how to do this in typed systems.
Obviously the 'secret' is that the steps above contain a very clear phase distinction. Which macros exploit. Our type systems don't give us a good enough language for exploiting phases (most of them don't even let you say anything about them at all.)
=> More informations about this toot | View the thread
Here's an idea that I think is worth pursuing, but that I'm unlikely to have time to do any time soon, so might as well let the world have it:
Finite Model Finding is a language inversion problem. You have a relational specification S (often in FOL) graded by size, and you want to find all models, up to isomorphism, of a certain size. The usual solution restricts itself to the language of assignments for specifying models M. But that isn't really 'required'.
What you really need is to design a language L and an elaborator E so that it is easy to get M from (L, E). Current approaches have E = id, and L = language of assignments. But it doesn't have to be that way!
(Why 'language inversion'? Think of how you'd phrase M as being as being fibered over S. Then what you're looking for is a "change of coordinates" at the intensional level, i.e. at the level of languages, that causes the inversion of S to be expressible in the new language).
=> More informations about this toot | View the thread
Waiting for results from a conference. They were supposed to be out last Thursday. Late Friday, they say it's going to be Monday. It's now late Tuesday...
=> More informations about this toot | View the thread
Well fuck.
I wanted to turn off 'focused inbox' on the mobile version of Outlook on my new phone. So I google how to do that, as one does. First result, AI, of course. Second result is from Microsoft Support - so I click that.
Results?
=> More informations about this toot | View the thread
What a pain. I'm owner of a Discord server that's been inactive for a while - so I wanted to shut it down. Old enough that 2FA was never enabled.
Can I delete it? Nope. Option doesn't even show up.
=> More informations about this toot | View the thread
"model in" and "model with" are rather different. Not enough is made of that.
I can easily model any given algebraic gadget (like a Ring) in most systems. No system lets me model a lattice of algebraic theories as nicely. Sure, I can do abstract modeling, but the abstract level and the concrete level don't cooperate. At all.
No, "data types a la carte" style is not a solution, it is a massive tease that a solution should be possible.
=> More informations about this toot | View the thread
Some questions need much firepower. To figure out what the proper plural of 'papyrus' is, I pulled out both our French and English dictionaries.
Yes, papyri is valid. Just not the only answer.
=> More informations about this toot | View the thread
I wonder if the following question about NbE has been answered already:
Given a language L with a reduction relation R, what properties of (L, R) would
=> More informations about this toot | View the thread
Great way to ensure that I will ignore a "prospective student" email: talk about my expertise in machine learning.
=> More informations about this toot | View the thread
Today's going to be a LONG day. Flight EDI -> LHR very delayed, so missed my connection to YYZ. Rebooked (after much fuss and stress) on 6pm flight, which lands at 9pm local (i.e. 2am my body time). No idea if my luggage will make it.
I'll probably have to wait an hour to find out about that. And then, in theory, I've got an hour's drive to get home. There's a chance I might get a hotel room close to the airport instead.
=> More informations about this toot | View the thread
At the airport, YYZ -> DUB -> EDI.
Talk planned. Slides, on the other hand... not at all ready.
=> More informations about this toot | View the thread
In many PLs "casting" should be called "lying to the compiler".
Sure, sometimes it's a white lie. But why is lying a feature at all?
=> More informations about this toot | View the thread
Sometimes 80s nostalgia can be a lot of fun.
=> More informations about this toot | View the thread
Today's obscure thought:
categorical modelling is the Poincare dual of telescope science
brought to you by Dijkstra's famous quip.
=> More informations about this toot | View the thread
Uncontrollable laughter. Was reading "Designing proof deautomation for Coq. ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Andrew Head, Benjamin C. Pierce. https://jwshii.github.io/deauto.pdf" and when I understood their 'illustrative example' (end of section 3), that's when it really hit:
That "de-automated proof"? That is exactly the shape of an Agda proof, phrased in Coq-lingo (Ltac), all done with right-programming and nothing on the left.
=> More informations about this toot | View the thread
Large thrombosed hemorrhoid: not recommended at all.
=> More informations about this toot | View the thread
Had a morning thought. Yep, 9 hours ago, but posting now - it's been a busy day.
Actually, a superposition of thoughts:
=> More informations about this toot | View the thread
LOL: "business innovations" and "presheaf" in the same abstract.
By serious people, doing it seriously. Because they want to extend local sections to global ones to show consistent feature sets of amalgamated consumer products.
This feels like using infinity category theory when talking about posets.
=> More informations about this toot | View the thread
Structure worship is annoying.
You know you sound like "Consider the symmetry monoid of the circle..." ?
=> More informations about this toot | View the thread
Two weeks of slaving over a stupid grant proposal over. Made the deadline. It could get funded -- thanks to the superb feedback from a colleague. Of course that feedback caused me 2 days of intense work. Just because it was the right thing to do doesn't mean I'm not thoroughly exhausted right now!
=> More informations about this toot | View the thread
=> This profile with reblog | Go to JacquesC2@types.pl account This content has been proxied by September (3851b).Proxy Information
text/gemini