The bloggings of Wren
Flat/Non-higher-order construction of ANF via mutable holes This post will describe an algorithm for constructing an ANF/similar IR from a functional-like base language with no closure usage, and with no related excess space requirements. This algorithm is as far as I know not new, and has apparently been known in imperative compilation for a while. However, I admittedly have no source…
It is well known that most software has bugs [Citation needed] . It is also well known that interpreters are mostly software 1 . One issue that one might run into in an interpreter is type safety : It may very well be possible for your typed language's interpreter to nevertheless end up in a state where it is asked to evaluate 1 + "hi!" . What can we do about that? GADTs: Generalized ADTs 2…
Preface Happy new years! Notation ∀ may be used in place of a Pi-type in some cases. A nested Π (a b : A). ... (or sim. for Σ ) represents Π (a : A). Π (b : A). ... . J Axiom J is the following: Given: A : Type x y : A P : Π (a b : A). a = b -> Type with P x x refl and eq : x = y we can conclude P x y eq where refl : ∀x. x = x . In short, for any property P , if P is true for x x refl , and we…
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣠⣴⣶⠾⠿⠿⠯⣷⣄⡀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣼⣾⠛⠁⠀⠀⠀⠀⠀⠀⠈⢻⣦⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣠⣾⠿⠁⠀⠀⠀⢀⣤⣾⣟⣛⣛⣶⣬⣿⣆⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣾⠟⠃⠀⠀⠀⠀⠀⣾⣿⠟⠉⠉⠉⠉⠛⠿⠟⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⠀⠀⠀⢀⣴⡟⠋⠀⠀⠀⠀⠀⠀⠀⣿⡏⣤⠀⠀__/\웃_⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⠀⠀⣠⡿⠛⠀⠀⠀⠀⠀⠀⠀⠀⠀⠙⣷⡍⠀⠀\____/⠀⠀⠀⢀⣀⣀⣤⣤⣤⣀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⣠⣼⡏⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠈⠙⠷⣤⣤⣠⣤⣤⡤⡶⣶⢿⠟⠹⠿⠄⣿⣿⠏⠀⣀⣤⡦⠀⠀⠀⠀⣀⡄…
A set. Absolutely not a set. An element of a category. A proposition. A chosen fixed point of a generating function. The initial algebra/final coalgebra of a generating endofunctor over a reasonable base category (say, Set ). A metaphorical representation of bytes. A membership function UNIV → bool . That thing you put after the : to make the computer stop yelling at you :( as any Propaganda…
(From someone who has spent far too much time thinking about the designs of programming languages) This post is split up into a few sections. I would also like to preface this post with: This is a little bit of a rant. I believe it presents some very reasonable points about Zig as a language, but it's not going to be perfect or completely objective. It is an opinion piece, and you're…
The following is adapted from the Isabelle/HOL 2025 tutorial , particularly 5.2 and onwards. It will explain much more thoroughly than I can. I also make no promise that the following is entirely 100% correct. It is ultimately my understanding, but I have run it past several others, and to the best of our knowledge it is correct. Notes These rule methods can be used in many different ways.…
This series is intended to give an interested layperson some idea of what goes on behind-the-scenes in a dependent typechecker, and how they might implement one of their own. I personally hold the belief that dependent languages (or similar) will eventually be the future of programming, so knowing this information seems worthwhile to me. One may also simply be interested for the sake of it, or may…
function r(str) { while (str.charAt(0) == ' ') { str = str.slice(1); } return str; } function get_args(str) { str = r(str); if (str == "") { return ["", []] } else if (str.charAt(0) == '.') { return [str.slice(1), []]; } let [rest, l] = get_args(str.slice(1)); return [rest, [str.charAt(0)].concat(l)]; } function parse_app(str) { str = r(str); if (str == "") { return ["", []]; }…
STOP DOING DEPENDENT TYPES Types were not supposed to be given computation! YEARS of typechecking but NO real world use for going higher than GADTS Wanted to go higher anyway for a laugh? We had a tool for that: It was called RUNTIME VERIFICATION "Yes please give me Id A x x of something. Please give me Vec (m + n) A of it." -- Statements dreamed up by the UTTERLY INSANE Look at what computer…
Preface: Low effort post. The following is an excerpt from a discord conversation about dependent pattern unification. In short, pattern unification is one method for solving unification goals such as the following: id : ( A : Type ) -> A -> A id A x = x id2 : ( B : Type ) -> B -> B id2 B x = id _ x Here, we have that our type argument to id is a hole, so we must solve it. We are working with a de…
hey hey
This is just a little blog i'm doing for the sake of spreading stuff I learn about. Fun, right? There will be mostly math and programming. \(a \to b\) let fac n = if n <= 1 then 1 else n * fac (n - 1 ) $$\forall a. \forall b. (\forall c. c \to c) \to (a, b) \to (a, b)$$