wen @cyrridven@computerfairi.es
I do believe that establishes the precedent that "omega underline" is pronounced as "with type constructors"
if "system F omega underline" can be a well-established point on the lambda cube, I don't want any more negative feedback on my use of emoji in papers
Little known fact! In Denmark, it takes two days for an email to arrive. Ethnographers theorise this is due to the government's contract with Microsoft, but so far this hasn't been confirmed.
Checking first-order languages like:
check Γ BOOL (forAll body) =
check (BOOL ∷ Γ) BOOL body ∨
check (INT ∷ Γ) BOOL body
my partner banned me from dancing while handling a knife in the kitchen, which... fair, that's probably a good call.
anyway, after spending a good amount of time writing it, turns out i don't really need it 🤷🏻♀️
transphobia
I love English, it's a great language, and there isn't anything fundamentally wrong with the the language or culture or anything like that, nope, nope, nope... oh what's that screenshot doing there, oh well this is awkward😅
me, after writing an O(n³) algorithm for reversing typing environments: "this is fine"
spacemacs is the best editor because it has a secret option to show me a cute text-art kitty on startup
Don't mind me, I'm just learning about the properties of the basic arithmetic units of computers, like, a decade into my career.
(It's actually all bar NaN and -Infinity, but that doesn't sound as neat.)
Floating-point numbers start behaving more and more like Infinity the bigger they get. The bigger x is, the more y there are such that x + y = x. Then x hits Infinity, and we have x + y = x for all bar NaN.
just went to file a GHC bug, only to find that I've been beaten to it by 11 years:
https://gitlab.haskell.org/ghc/ghc/-/issues/3134
in that issue, @simonmar@twitter.com mentions recalling a "very old" ticket about this, 11 years ago!!!
anyway, this bug is still in GHC 8.10.1... 😅
welp this sucks, very disappointed in @Neovim@twitter.com :(
RT @RosaCtrl@twitter.com
The worst part is that the patch was originally submitted to @Neovim@twitter.com, the team asked to send it to upstream (something they usually do to avoid diverging too much) but then it was closed following Bram’s decision 😭 First time Neovim’s devs disappoint me https://twitter.com/ibroadfo/status/1298745527484510209
love me some Designated Social Interaction Time #icfp2020
going down the floating-point rabbit hole, now considering implementing unums for agda
@edwinbrady@twitter.com anyone tried to do floating-point arithmetic in idris2 yet, or is that position still open?
so far, I've been the first to try and actually use floating-point arithmetic in three different proof assistants
senpai noticed me 😍
