rachel rosen @rachelrosen@types.pl
is this testing whether I'm a lesbian or a replicant mr. deckard?
first year computer witch at chalmers university of technology.
Joined May 2021
Pinned toot
rosen isn't my surname, I just really like the book "do androids dream of electric sheep?" and stole rachel(from the book)'s surname for my username.
realized this is not obvious lol
rachel rosen
boosted
rachel rosen
boosted
I'm trying to get linearity checking working in the new Idris core. This is how it's going so far:
Yaffle> plus (S Z) (S Z)
(S Type) : Nat
It's possible I've messed this up somewhere.
I love when my type theory is crisp, with a real crunch !
I think I finally groked typechecking depdendent types. been playing around with implementing "An algorithm for type-checking dependent types" (Thierry Coquand), as well as looking at some of the SPLV20 tinyidris stuff. neat!
why did the topologist fail their maths class? they only had surface level knowledge.
rachel rosen
boosted
(5/5)
The first email ever sent by a head of state was to announce a programming language! Sent by "HME2" (i.e. Her Majesty, Elizabeth II), it began "This message to all ARPANET users announces the availability on ARPANET of the Coral 66 compiler...."
rachel rosen
boosted
time isn't real, that's why functional programming works
I've been trying to do a first dependent type checker for a while, but I keep writing it in idris and adding a lot of information to the types, which is probably great for a big project, but has ultimately stopped my progress as I get stuck proving stuff in order to get anywhere. I really should just get something that just works before I try to make it fancy...
rosen isn't my surname, I just really like the book "do androids dream of electric sheep?" and stole rachel(from the book)'s surname for my username.
realized this is not obvious lol
rachel rosen
boosted
rachel rosen
boosted
@ionchy reminds me of the classic "If you need to prove a theorem, Yoneda lemma"
rachel rosen
boosted
https://researchseminars.org/talk/ToposInstituteColloquium/57/
We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals. Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.
I have now applied to be a teaching assistant next year, exciting!
rachel rosen
boosted
shoutout to the two guys I called out on being racist for repeatedly failing to missgender me, having to "correct" themselfs. huge confidence boost :)
rachel rosen
boosted
this server is now running on an 8GB Linode due to the generous support of our supporters on Patreon
also we have a Patreon now. it's https://patreon.com/typespl
rachel rosen
boosted
announcement (boosts appreciated)
We're delighted to announce the HoTTEST Summer School, which will take place online everywhere in the world during the months of July and August 2022.
The school will run both synchronously and asynchronously. The lectures will be delivered live (between 2:30-4pm UTC) and paired with various tutorial sessions run by teaching assistants. The course will also feature a discord-based all-hours Q&A and an online archive of all course materials so that participants can follow along on their own schedule.
This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory. Our goal is to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.
Read more: https://groups.google.com/g/homotopytypetheory/c/Ir2joc7imyI
Join the Discord: https://discord.gg/tkhJ9zCGs9
is this testing whether I'm a lesbian or a replicant mr. deckard?
first year computer witch at chalmers university of technology.
Joined May 2021
rachel rosen's choices:
