Pinned toot

As a corollary, if I ever toot anything political, please don't assume that the people whom I follow or who follow me agree with me.

Pinned toot

I'm so angry! This guy claimed that Cantor's diagonalization argument is invalid under intuitionalism and spread the myth that intuitionalists reject proofs that derive a contradiction, then went on to argue with everyone on the comments section who pointed out his error! He was acting really condescending based on his incorrect idea of intuitionalism and acting as if we were all crackpots who were out to disprove classical results!

PLT Redex is amazing! I can prototype languages without having to rigorously prove everything like in Agda! Why didn't I discover this tool before? #Racket

I'm trying to write a proof about the lambda calculus in Agda, but I'm stuck on the strangest type error and I am absolutely fed up.

The typed hole says that I need a proof that ¬ v ≡ v'.

There is a variable neq : ¬ v ≡ v'.

When I try to fill the hole, Agda won't let me because the expression (neq x) of type Data.Empty.⊥ is not definitionally equal to some complicated term!

Agda never listed any equality constraints when I focused on the hole. I don't understand why there is an equality constraint; I'm simply applying a function to an argument (the typed hole is the argument). Besides, Data.Empty.⊥ is uninhabited, so all equalities are vacuously true and it shouldn't even matter!

What???

I was lucky enough to be accepted to Maryland, Northeastern, and Purdue for college.

Northeastern is probably the college that I am most excited about. However, the family friends who helped me with college applications are now recommending me to go to one of the other schools instead! Their ranking is Purdue > UMD > NEU, with the concern that NEU is not as well-known and respected as Purdue and UMD, which are both recognized as having great CS programs. They said that I should pursue a general CS education in undergrad and specialize in PL in grad school.

I intentionally only applied to schools that had some sort of PL department.

From the looks of it, UMD has the smallest PL department, and the projects they do seem to be more "applied": https://www.cs.umd.edu/projects/PL/ It's stuff like static analysis of C, Java, JavaScript, Ruby, etc. I know that Michael Hicks is the guy in charge of the SIGPLAN PL Perspectives blog.

Northeastern's PRL (http://prl.ccs.neu.edu/) seems to have an emphasis that I prefer. It isn't as theoretical as my ideal (CMU was my dream school because it does hardcore TT/CT/constructive math, but they rejected me), but NEU does have a lot of type theory stuff. A lot of academics I've heard about came from NEU (e.g. Gasche, who is involved in the OCaml community and is now at INRIA, or David Van Horn, who is now at UMD).

The only person at PurPL (https://purpl.cs.purdue.edu/) whose name I recognize is Tiark Rompf, who researched Scala stuff. Purdue's course offerings (https://www.cs.purdue.edu/academic-programs/courses/index.html) seem to be mainstream CS stuff, not the FP and PL culture that NEU has.

My heart is probably set on Northeastern, but other people are making me second-guess. Purdue was honestly an acceptance that I was not expecting.

But, I disagree with the premise that NEU is not well-known. It may not be as famous to an outsider, but within PL theory, it seems to have a lot of influence. e.g. Brown is culturally influenced by Racket with its Pyret language. I believe that with PL, everyone will probably have heard of NEU and its Racket crowd.

Which college should I attend?

cc @iitalics How was NEU for you?

I'm reading the article "Natural language processing with SNAP!" by Ken Hahn. Very interesting! I had never heard the term "word embedding" until now. https://helloworld.raspberrypi.org/issues/12

With Covid19 going around, I'm lucky that I did not apply to foreign universities.

How do Northeastern and Purdue compare for programming language theory and for CS in general? NEU has tons of PL people. Purdue has a PL department called PurPL, but the only member I recognize is Tiark Rompf, who worked on Scala. Purdue is higher ranked than NEU in CS.

"Note that the partial element `u`

does not have to specify all the sides of the open box, giving more sides simply gives you more control on the result of `hcomp`

. For example if we omit the `(i = i0) → x`

side in the definition of `compPath`

we still get a valid term of type `A`

. However, that term would reduce to `hcomp (\ j → \ { () }) x`

when `i = i0`

and so that definition would not build a path that starts from `x`

."

Why the heck is this allowed? Aren't all expressions supposed to compute? In what way is that a value?

AP Calc reading:

"One thing that is important to realize about Theorem 4.1 is that it is an existence theorem. It tells us that there must be some number z with the property expressed in Equation (4.2), but it does not tell us how to find that number. In the vast majority of cases, in fact, we will be completely unable to find the magic z. In other words, Theorem 4.1 is all but useless for computation."

ABSOLUTELY NONCONSTRUCTIVE

Page 52 of this paper answers my question about the feasibility of a simplicial type theory: https://www.cs.cmu.edu/~rwh/theses/angiuli.pdf

the higher morphism is mapping other things: https://ncatlab.org/nlab/show/2-morphism What is going on?

How can I learn about the math behind homotopy type theory? I know what groupoids, n-cubes and simplices are. I see the terms "Quillen model category" and "Kan complexes" thrown around, but I don't understand their definitions. One thing that's a little weird to me is that to my understanding, higher category theory generalizes morphisms mapping objects as k-morphisms mapping (k-1)-morphisms, with objects being 0-morphisms. However, it seems like there are different "shapes," in which