re: Agda 

@ionchy warning this may break your code and i will not explain why

re: Agda 

@ionchy --experiemental-lossy-unification

@agdakx Make it so only people outside the agda-community org can submit PRs and everyone inside gets told "go take a break. touch grass. enjoy life"

No working on Agda on the weekends no working on Agda on the weekends stop thinking about metavariables and simplifying interval expressions

@asaj @pigworker Something I've considered for Agda is deferring type errors.

We already have metavariables which are blocked on a deferred type-checking problem (e.g. checking the arguments to something whose type we don't know is a Pi), so we could have metavariables blocked on an abandoned type-checking problem. These would be the values of definitions whose RHS had a type error.

Then any type error caused by one of these values would be suppressed. As long as your definition has a type-correct type, it could be used by parts of the program that don't depend on its value

@asaj Right - depending on how radically this is implemented, you could in theory type-check a module where unused dependencies don't even scope check

Really the thing is making it lazy. It should be possible to request only the exported names by a module (in a fast way!), and then when the names are needed, block on the decoding/checking of the definitions in that module. Really I'm thinking of github.com/ollef/rock

Show thread

Once again plagued by thoughts of how to make Agda parallel

re: abstract nonsense 

@jonmsterling @JacquesC2 and yet not close enough that I can get away with ignoring the difference 😉😅

tomorrow i want to do maths instead of debugging agda. something nice and relaxing

Spent 6 hours tracking down a computation bug and I'm no closer to fixing it :/

traverse is the solution to all problems so when you have a nested problem, traverse (traverse f)

Show thread

Hi friends! @agdakx and I built a beautiful new bike shed over AIMXXXI, but predictably there have been complaints about what colour to paint it.

PR: github.com/agda/agda/pull/6354

Short version: We'd like if it were possible for consumers of a module to, in their own abstract blocks, selectively "look through" abstract definitions which they have imported. This is inspired by Gratzer et. al.'s recent "Controlling unfolding in type theory", so we call it "abstract unfolding"

If you use Agda, and you use abstract blocks — or maybe especially if you've tried but gave up on abstract blocks — please weigh in on the linked issue. Thank you! ♥️🐔

@agdakx
@ionchy This sounds interesting — I'll have to think about it! Though I'm not sure how exactly it differs from a tactic implicit, from a user's POV?

@JacquesC2 @gallais I was surprised yesterday, after writing a much "lazier" (not in the technical sense) serialisation scheme, thinking I'd trade space for time — as a flag! — that while it was faster, serialisation got slower, and everything else sped up a bit instead...

@JacquesC2 @gallais Oh I'm of the totally opposite opinion. We should be putting more shit into the agdai files so we have to compute less downstream. The time spending reading them is negligible compared to the time writing them

re: apt search 

@ionchy oh not the package manager

I can't discard this difference being just from random variance, lol. I was expecting this to be much faster than the old serialiser, not.. basically the same thing

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.