Joey Eremondi boosted
James Wood

#lazyweb: Is there any way to make Firefox “open” a downloaded file using a custom command (in a GNU/Linux system)? For example, when I download a .zip file, I want to be able to click “Open with...” and then type in something like `unzip -d ~/some/where $FILE`, rather than either saving the file under a fresh name in /tmp and then repeating that name in the terminal, or keeping a specialised graphical unzipping program just for open-with. I notice that PCManFM-qt (the LXQt file manager) implements this.

0
Joey Eremondi boosted
David Thrane Christiansen

_Functional Programming in Lean_ is now done and out the door!

It's a free online book that describes using the interactive theorem prover Lean 4 as a programming language, without assuming any background in functional programming. You don't need to already know Haskell, OCaml, Rust, Scala, or Racket to read this book.

You can read it at leanprover.github.io/functiona .

Thank you to everyone who's carefully read prereleases - it's much, much better than it otherwise would have been. The Lean Zulip is a great place to hang out.

Also, thanks to MSR for supporting this project, and to Leonardo de Moura for initiating it. It's been a lot of fun!

1+
Joey Eremondi boosted
Honkability Index

meta, anti-feature 

Did you know that if you post on a hashtag, people following that hashtag can see your posts *even if you'd blocked them*? Now you know!! #FediTips #GodDammit

1+
Joey Eremondi boosted
Kendra Albert

Are you just catching up on the bonkers story about the lawyer using ChatGPT for federal court filings? This is a thread for you.

1+
Joey Eremondi boosted
Steve Dunham

US lawyer used ChatGPT and filed a brief citing a bunch of hallucinated court decisions: nytimes.com/2023/05/27/nyregio

0
Joey Eremondi boosted
Amélia Liao

New little Agda feature I'm cooking on the side (actually a second attempt...) got done enough in a day that I feel comfortable sharing the prototype:
github.com/agda/agda/pull/6669

1
Joey Eremondi boosted
Conor Mc Bride

@dysfun It's a spectator sport. It's hard to learn Agda from finished programs. You need to learn the moves.

1
Joey Eremondi boosted
Emily M. Bender (she/her)

I've seen a lot of folks responding to my recent Medium post "Thought experiment in the National Library of Thailand" by trying to draw analogies between language models and disabled people (specifically blind, deaf or deafblind people).

Please don't do that. It's dehumanizing and inappropriate. To learn more:

medium.com/@emilymenonbender/n

1+
Joey Eremondi boosted
chris martens (they/them)

@maxsnew @ionchy
like i'm fully willing to believe i just have "the way i learned it" bias, but operational semantics have always just felt good to me in that un-mysterious "pushing symbols around on a page" way that (what i've seen of) denotational semantics has not

0
Joey Eremondi boosted
Amélia Liao

nothing can stop me from making extremely unfunny jokes about how the inductive-inductive version of [something] is called [something]-[something].

1
Joey Eremondi boosted
*
Liang-Ting Chen

me: I am so excited to try a new feature in Agda.

(5 min later)

me: (writing a bug report)

1
Joey Eremondi boosted
Andre Videla

@asaj @amy I'm very interested in those cases and I would love to develop a theory of "adaptable changes" where the compiler fix also provides a migration tool for users affected by the change

This is not only useful for compilers but also for breaking changes in libraries

1
Joey Eremondi boosted
Foone🏳️‍⚧️

ugh. It's annoying when you search "how do I do X with Y?" and the first and only relevant result is on the official Y github and it's a ticket saying "adding X would be good". No comments added. Issue is still open.
Created date: four years ago.

1+
Joey Eremondi

Vectors are an instance of this too, with the underlying monoid being Nat

Show thread
0
Joey Eremondi

Algebra/CT question: lists are to monoids as heterogeneous lists are to ??????

i.e. some kind of indexed monoid

A heterogeneous list is a list of elements over a list of types, and concatenating elements from (HList L1) and (HList L2) gives you something from (HList (L1 ++ L2))

Is there a generalized version of this that's analogous to a monoid? i.e. you have some underlying monoid (M, 0M, *M), and then something indexed over that (N, 0N, *N) where 0N is in N(0M), and *N : (m1 : M) -> (m2 : M) -> N(m1) -> N(m2) -> N(m1 *M m2)

1+
Joey Eremondi

Alright, question for me who is I'm still clueless at Mastodon.

There's been talk about how some main servers are blacklisted on types.pl. I'm not here to disagree.

The question is if I want to see content from those servers (the poor moderation ones, not the like fascist ones), what's the best way to do it without jumping ship on types?

1. Is there a way to unblacklist it for myself at types.pl?

2. If not, If I make another account on e.g. mathstodon or something, is there a way to continually "sync" it with my types one, so I can still post from types, but see content from math, and so my following list is always the same for the two?

3. Does any of this work with Tusky?

1+
Joey Eremondi boosted
Colin

I suspect everyone involved already knows this, but any publication venue that asks reviewers for a thorough review in 10 days, or returns reviews in less than a month, or posts papers showing acceptance less then a week after submission, is a junk venue that does not meaningfully review papers, and cannot legitimately be described as peer reviewed.

This PSA brought to you by the latest review requests from such a journal, asking me for a 10-day turnaround on reviewing a paper that is basically a PR puff piece on a commercial AI system 🙄

0
Joey Eremondi boosted
Max S. New ⚜️

I'm completely drunk with power after learning that Agda's variable generalization works works with nested generalization. Now the code is significantly shorter than the on-paper version of the same language/logic

0
Joey Eremondi boosted
Joachim Breitner

From the GHC release announcement:

> The GHC developers are happy to announce the availability of GHC 9.6.2. This release is primarily a bug-fix release addressing a few issues
found in 9.6.2.

We have found a fixpoint! Finally the knot is tied! #haskell

1+
Joey Eremondi

Interesting discovery with Justus at the office today: constructors in Agda don't have types. E.g.

```
data Eq (A : Set) (y : A) : A -> Set where
Refl : Eq A y y
```

The type of Refl is *not* polymorphic, it just has metavariables in it:
```
Eq _A_8 _y_9 _y_9
```

You can use it polymorphically because of unification, but when you actually pattern match on something those variables are not bound at all

1+
Show older
types.pl

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

Resources

Developers

What is Mastodon?

types.pl

More…

v3.5.5+types · Privacy policy