Pinned toot

Humanitarian crisis in Bangladesh Show more

skilled, engaged, and passionate the teacher is can make or break the class experience for me. Last year, I had some amazing teachers, so right now, I feel disappointed by some of my teachers in comparison, but *shrugs* it's too early in the year to judge. As a result, my class preferences so far this year are different subjects than last year.

Many times, people like doctors may ask me, "What's your favorite class/subject in school?" I feel like generally, people don't make a distinction between "class" and "subject," but I've noticed that the two words can lead to totally different meanings. As I'm starting the school year, I notice that how much I enjoy a class is based more on the quality of the teacher than the actual subject. I don't really hold any special preference towards English vs chemistry vs history etc, but how (cont.)

Idea: C++, but the template metaprogramming and static introspection are formalized by dependent type theory

Okay, so `:t case \x -> x of { id -> id id id }` fails in GHCi due to the occurs check and `match fun x -> x with id -> id id id` in OCaml has type `'_weak1 -> '_weak1`. So, Haskell doesn't let-generalize in case expressions, but OCaml does??? 😕

Okay, I rewrote my typechecker to work on patterns, not decision trees. However, I'm not sure if I'm supposed to let-generalize the bound variables in the pattern. Considering that I desugar let expressions to case expressions now, I guess that I should.

I currently have two tree representations (AST and core terms); I can afford to add a third one. Alright, I’ll make the core form have desugared patterns that are easy to typecheck, then lower the core form into a format with decision trees!

Oof, I just remembered that I need to append (Lisp-style) lists! What bothers me is that the operation is done for both patterns to create the decision tree and type lists in the typechecker to follow the decision tree evaluation logic, but the typechecker would not need to mirror the pattern match compiler’s actions if I had typechecked from the pattern.

match compiler bugs and also modified the algorithm with enough information to evaluate the decision tree. Previously, I compiled patterns into let-expression terms separately, but I decided to move the name binding logic into the decision tree, and typechecking the tree proves that I have enough information to bind names from the tree.

Hmm. The pattern match compiler has a relatively expensive operation in which it finds a column of a pattern matrix that contains a constructor pattern, then moves it to the front. The action corresponds with a decision tree “swap” instruction. For the typechecker, I need to swap a list / stack of types. This isn’t *that* inefficient, but it would have been more straightforward to walk pattern AST nodes IMO. OTOH, by typechecking the decision tree, I discovered and fixed some pattern (cont.)

Haha yes, I'm so relieved right now! I managed to refactor my code to only compile patterns into decision trees and type infer from the decision tree! The type checker was failing so much and I JUST fixed it. I was afraid that I had totally ruined my code. (Of course, I am using version control, so if I really did mess things up beyond repair, I would still have working code.)

Also yippee, I managed to understand an algorithm (the pattern compilation algorithm) enough to adapt it for my needs.

Hmm, if I annotate the decision tree leaf node and switch node with the variables to bind...

*Sigh* In my WIP compiler, I wish that I type inferred programs before compiling patterns to decision trees. Before, I compiled patterns to decision trees and let-expressions separately and typechecked the let-expressions. However, now I'm refactoring the pattern compilation and need to figure out how to typecheck from the decision tree, or do an even more massive refactor. I hope that the decision tree doesn't lose too much information...

What are your opinions on distinction between capitalized and lowercase identifiers in syntax? (e.g. modules are capitalized, variables are lowercase)

Boy, are you a const? Because you are \x _ -> x.

TAH boosted

Anime Show more

My school-issued Java textbook uses three-space indentation! 😡

I set my user flair on r/programmingcirclejerk to `What part of ∀f ∃g (f (x,y) = (g x) y) did you not understand?`, and I mean it unironically. All it means is that all functions of pairs can be curried.

Yippee, I just finished doing the first chapter of vol 1. in . I was challenged by the exercise about proving that for all Booleans b and c such that b && c = b || c, b = c. I first tried introducing everything, then destructing, but ended up needing to prove the uninhabited, that true = false. Then, I read the comment above the exercise stating that I shouldn't immediately destruct my variables. 🤦‍♂️

I want to get into constructive proofs and ; which language do you recommend: , , , or something else? Idris is cited as the practical one; but I’m less motivated by pragmatics than by theoretical elegance. What are the implications of the languages’ different approaches to universe hierarchies? Of homogeneous vs heterogeneous equality? Is Coq’s Prop vs Set distinction inelegant or good? Should I prefer tactics or the core lambda calculus?

Show more
Functional Café is an instance for people interested in functional programming and languages.