Latest Posts (9 found)

Horrible answers to "What is a type?"

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, ). A metaphorical representation of bytes. A membership function . That thing you put after the to make the computer stop yelling at you :( Propaganda made up by Big Typechecker to make us complacent. The archetype of person that you tend to feel attracted to romantically. A metal plate with a glyph, used for printing ink onto paper.

0 views

Opinion piece: On Zig (and the design choices within)

(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: First, and very much foremost, Zig is not memory safe. This is, in my opinion, the most egregious thing in this post, by a very large margin. Moreso, Zig does not make any attempt to be memory safe - it can catch some things at runtime, with specific allocators, but so can C these days. Indeed, there are some cases, like use-after-realloc, that can catch and Zig cannot. A language in the modern day that does not make an attempt at memory safety is, in my opinion, not reasonable. It has been shown that in some areas, up to 70% of security bugs are due to memory safety issues ( Source ). I subscribe to the idea that the user must be constrained. It is perhaps harsh to say, but for large and complex programs, I believe that there are very few programmers who will write memory-correct code nine times out of ten. When writing code with others, that goes down. I personally do not believe I fit into that category. The fact that Zig allows the user to write faulty software is supported by various somewhat informal, but still useful, statistics. Notably, the following statistic disregard duplicates, and unreported errors. However, general trends are still of note. Here are some: This means that, roughly: Again, this roughly means: Also not great. Again, these statistics are slightly off at best simply due to the nature of their collection, but the trends do not lie. If you're not reading the above: It can be summarized as "Not ideal." At one point, this part of the article contained a runthrough of the , and my opinions on each bullet point. I have decided that that is not a constructive discussion of Zig. It suffices for me to say that I do not believe Zig particularly embodies its own zen. Zig does generics in an odd way. I believe this is the best way of putting it. This post is not meant to be, nor will it contain, a proper explanation of Zig's capabilities, so I refer the reader to the wider internet there. However, doing generics with "normal" code means that there are multiple ways to write the same generic function. There is no standardization between different libraries, different styles of writing code, and different users of Zig. Every person can do generics in their own special way. This obviously has slightly dire effects on readability. In practice, most Zig users are reasonable enough to stick to some "common patterns" of doing generics and similar, but it is widely known that if the user is giving the ability to do something, it will be done. I believe that generics are important enough they should be first class. Arguments can be made that Zig's comptime is also useful for other things, not just generics. Some examples I have been given are conditional compilation, and variadic functions. Beyond these, I am yet to see a convincing motivating example that requires the machinery that Zig provides. Every such example can, in my experience, be solved with less powerful (and hence, for the most part, less confusing) machinery. As a result, I am inclined to believe that Zig's comptime is a very large and all-encompassing feature that ultimately brings very little to the table that smaller features cannot. I am personally a proponent of a good macro system, but I will readily admit people can also go overboard with one of those. Zig's casting is a bit cumbersome. To cast a float to a specific int width, for example, must be done with . Bit of a mouthful. Inference can help here (For example if a variable is already known to be a , the outer cast is not needed), but I would think that with Zig's comptime abilities, this could be made a bit nicer. Luckily, it is common Zig practice to annotate everything if possible, so this does come up slightly less in practice. It is still a bit bulky however. Float to int casting additionally can invoke undefined behavior if the float is outside the integer's range. I personally prefer truncating semantics, with perhaps a specialized method ( ?) for UB semantics. That's more of a personal preference though. Result location semantics are in theory a quite nice idea. Knowing predictably where things are going to be placed in memory is, of course, good for any systems-adjacent language! In practice, there are several choices within RLS that I find counterintuitive. Take the following example, where we attempt to swap two struct members in place: This outputs the following: I will note that the equivalent C can only be written in the former style, and it prints the former. The only difference between the latter and the former is whether the type name is present. This is intended behavior! Indeed, this very example is given in the Zig reference, a fact that I find odd. Why give a warning against something when you could just fix it? Zig does not have move or copy constructors; I do not think there is very much reason for the latter to ever behave the way it does. One extra register is all you ever need, even for an arbitrary parallel move! ( Source .) In its previous form, PRO has been removed from Zig. There was a long period where this would print : As Zig would correctly, per PRO at the time, but incorrectly per common sense, pass as a reference. This is actually mildly unfortunate. It's a very interesting optimization, and being able to guarantee behavior around optimization of parameter passing would also be quite beneficial. Unfortunately, Zig simply does not have the level of control needed to do it. Aliasing is freely allowed, and in order to make PRO work, it cannot be. Rust can, and in many cases does, do this! It's a shame Zig has to miss out. There is current work to make PRO work in the case of pure functions ( Source ), so I remain hopeful that it will return in some form eventually. The Zig compiler is not particularly fast. The LLVM backend even more so; compared to Clang, (which has the home field advantage, but can still be quite slow), and by my measurements, Clang is consistently between 3-10x faster. A new Zig backend has been written to help fix this; by similar measurements, it is consistently faster than Clang by 1.5-2x, and much faster than the Zig LLVM backend. While these numbers are nothing to scoff at, I believe there is more room for improvement, and I would like to see where it goes. Zig is a simpler language than C when comptime is not involved, and I would be excited to see that reflected in the benchmarks. It is also possible that Zig could use LLVM more efficiently, but I cannot comment on this without digging into the internals of the compiler. Of course, all of this is quite reasonable. The Zig compiler has had far, far fewer man-hours put into it, and this of course reflects in aspects of the compiler that simply take a lot of time, such as these. I look forward to seeing what can be done in the future. The Zig build system is a little confusing. It is very neat to be able to write build system code in the language itself, and this is a feature I believe more languages should have. Unfortunately, it is as of current not well documented enough to justify its own complexity. This of course can be improved, and I hope it is. Zig currently does not have a "first class" language server. The "Zig Language Server", or ZLS, is unofficial; It does not have real compiler integration, so it is unfortunately limited in some ways. The creator of Zig apparently does not use a language server while programming, so I do slightly understand why it is not a priority, but I personally believe tools like a good language server are quite essential to wider/popular usage. Here are some quotes I have heard from people who have used it far more than I: Apparently it is very limited when comes into play, and cannot handle compound types like 2D arrays. I cannot offer much firsthand experience however. There are always more errors to be caught. I particularly recently noticed that Zig cannot currently catch use-after-realloc errors, like the following: Address sanitizer with Clang can catch this, so theoretically Zig should be able to catch it (perhaps with a similar system) too. Apparently, it is desired that comparisons with panic. This seems reasonable to me. However, the issue for this has been open for almost ten years , which makes me worry that it might be a while still until it is finished. This panics in and modes, however, so it does at least work in some cases. According to this issue , it is "not a goal of the Zig compiler" to catch issues like the following: This just seems silly to me. Catching something like this, in the simple case, should be just one pass over the AST; why not do it? Zig simply doesn't allow tabs in comments and strings? This issue explains more, but the justification of "it (a tab) is ambiguous (in) how it should be rendered", I do not quite agree with. Strings make some sense; you can still write for a tab, and they do indeed make output ambiguous. However, they're still allowed in indentation! This means that in commenting out code, you can take a program from valid to invalid. does reify tabs into spaces, but if your editor is misconfigured and you're not running constantly? Zig does not have a way to iterate through a slice or similar in any way except one-at-a-time forwards. Anything else? You're using a loop, and you'll enjoy it. Zig blanket bans proposals to change the language, so despite issues like this one , I doubt this will happen any time soon. Zig doesn't have 'em. Everything is an error. In practice, this mostly manifests through reasonably harmless things like "unused variable" notices becoming errors, which is reasonably annoying when just trying to spitball. For the most part, the community is about par for the course for programming language communities; that is to say, quite nice. However, I have had some reasonably negative interactions that I feel are somewhat of a general trend. They usually proceed like the following: This is unpleasant, and while it's not a particularly uncommon thing to see in programming language communities, Zig seems to have a bit of a bad case of it. I suspect it is due to Zig's fairly minimalistic nature; it lacks a lot of features that one would otherwise use to solve problems. Of course, this is the appeal for many, but still. It is made worse when said topic is something one is particularly knowledgeable about, and the people you are conversing with believe they can solve the issue without that knowledge. I do not believe that a few bad apples necessarily spoil the whole barrel here, but they definitely sour it. I find Zig interesting, with an unfortunately negative connotation. I believe the goal of a C-like memory unsafe language "for the modern day", while interesting at first glance, ignores many of the issues that make C a problem in said modern day. Much of Zig seems to me like "wishful thinking"; if every programmer was 150% smarter and more capable, perhaps it would work. Alas, they are not; myself included. I believe that modern concerns of memory safety and correctness require modern solutions; not performing patchwork fixes over the core issue. Existing memory safe languages are not perfect. Rust will be used as an example quite a bit, as from what is currently avaliable, it embodies closer to what I think is reasonable in a programming language. However, there is still much room for improvement in this space. All of the following is ultimately my opinion. If you disagree, you are welcome to find me somewhere on the internet and ask me more. I bear no grudge or ill will against anyone who contributes to, works on, or is otherwise involved in the Zig community. The following are things I have noted about the language, not the people behind it. If you enjoy Zig, go and write it, and make cool stuff - I am not the programming language police. Exception to the above: I have one gripe about the Zig community. This gripe "targets" no one person in particular; rather, larger trends. The Rust compiler has had a lifetime 59,780 issues reported. Of these, 4,158 contain one of "crash", "segmentation fault", or "segfault". The Zig compiler has had a lifetime 13,269 issues reported. Of these, 2,260 contain one of "crash", "segmentation fault", or "segfault". 7% of lifetime issues reported in the Rust compiler are crashes. 17% of lifetime issues reported in the Zig compiler are crashes. The Node/v8 JS runtime, written partially itself in JS and partially in C++, has had a lifetime 19,631 issues reported, 1,710 of which contain one of the above keywords. The Deno JS runtime, written primarily in Rust, has had a lifetime 13,422 issues reported, 552 of which contain one of the above keywords. The Bun JS runtime, written in Zig, has had a lifetime 13,828 issues reported, 3676 of which contain one of the above keywords. 8.7% of lifetime issues reported in Node are crashes. 4.1% of lifetime issues reported in Deno are crashes. 26.5% (!!!) of lifetime issues reported in Bun are crashes. "Deeply horrid" "It is one of the worst LSPs I have ever used" "Don't get me started" I ask a question about solving something in Zig. Often, given my background, it is about adapting my more functional-esque thinking to Zig. Someone chimes in with a half-solution that does not actually address my problem. I attempt to communicate this to them, which often involves explaining the features I would use in <insert other language>. They insist that these features are not needed, but do not elaborate on how one would solve the problem without them.

0 views

Isabelle/HOL: The various rule methods

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. These rule methods can be used in many different ways. While some general principles are mentioned below, if the prerequisits are met, every rule can theoretically be used with every rule method. Many of these various combinations will not be beneficial to proving a given goal, and hence it is useful to know how the rule methods interact with rules and proof states in order to select the correct pairing. In that vein, the same rule will be interpreted differently by these different rule methods. Read more for how they work, and hence why. We use , , and as arbitrary assumptions and goals throughout. Consider the introduction rule : If we have a goal of form , from we can infer that it is sufficent to seperately prove and . Indeed, performing on a goal of this shape will result in two goals: which can be then proven seperately. is for backwards-reasoning; here we can see that as moving "backwards up" the introduction rule (Starting with the bottom, and ending with the top.) It is therefore useful for introduction rules, as demonstrated. is designed to function with elimination rules. Take for example the elimination rule for disjunction: (Informally, to prove something about a disjunction, we must handle both possible cases.) If we have a goal of the form: we can perform to transform this into two goals: where we must handle each possible case of the disjunction. is a bit of both backwards and forwards reasoning. In the above elimination rule, we can see that we need three assumptions to prove --- we already have , so it is sufficient to then only additionally prove and , which are exactly the goals gives us. Notable: deletes the already-held assumption, as it is "rarely useful" (quoting the Isabelle/HOL tutorial). See below's note for more. As mentioned, deliberately deletes the already-held assumptions when using an elimination rule. Above, we could see that was not present in the generated goals, as it was already assumed. By instead using , we can keep the original goal in our assumptions as follows. If we apply the principles from the section to , we would get: i.e., , as expected, replaces the goal R with the goals sufficent to prove it. In this case, however, the first goal is trivial, and in the latter two, holds little worth, as we know either or . This is why automatically discharges the first goal and deletes the already-held assumption. For the sake of example, recall (one of) the conjunction elimination rules: This rule is more specifically called a "destruction" rule, as it takes apart (destroys) the original term (here the conjunction) and concludes with one of its subterms. The in therefore stands for or . Destruction rules are used for forwards-reasoning, as you move "forwards down" the rule. hence replaces an assumption of form with one of , deleting the original assumption. functions the same as , but does not delete the original premise. The stands for , as it is used for forwards-reasoning. For all the above rule methods, can be used to explicitly instantiate them instead of using the family (which is explained below). This instantiates left-to-right by occurence, so with will result in the instantiation , from where the rule will proceed. Notably, does still work with the family, but there is (as far as I know) no reason to use it over 's explicit instantiation. Speaking of: For each of the above, there is a corresponding (standing for tactic): , , etc. These s are slightly more powerful than their less equivalents. Firstly, each allows for the various premises to be explicitly instantiated by name. For example, with the rule, one could explicitly write This allows the rule to refer to meta-forall-bound variables, which most commonly arise when performing induction or similar. For a goal of form: with some mentioned in , performing will generate the goals is a meta-forall bound variable. This functions as expected; during the induction step of an inductive proof, we must prove that for any , . Because it is meta-forall bound, and friends cannot refer to directly using (Although, automatic unification can work). Instead, we must use and friends to refer to it. I am not quite sure why this is, but I presume it is due to internal complexities around the meta-forall. Recall that can be used to explicitly instantiate: These lemmas are otherwise equivalent; only their presentation differs. In general, these methods have the form where is a variable occuring in , and is a locally bound variable or assumption. Any combination of zero or more of the variables occuring in may be used, in any order. The methods have an additional advantage, which is that they can be told to refer to a specific goal. If we have goals of the form and friends will by default refer to the first goal. Using , we can refer to the goal (1-indexed.) When combining this with specifying variables, the goal specifier comes first. (i.e., .) This section is almost entirely copied from the aformentioned Isabelle/HOL tutorial. Given an arbitrary rule R of the form: For elimination rules, is referred to as the "Major premise". This will usually be the object being eliminated. In for example, it is . Method unifies with the current subgoal, and replaces it with the subgoals . Method unifies with the current subgoal, and with the first suitable assumption. The subgoal is then replaced with the subgoals , and the assumption is deleted. Method unifies with the first suitable assumption, which it then deletes. It then adds the subgoals , and the original subgoal gains the assumption . Method is like , but it does not delete . Method unifies with the current subgoal, and replaces it with the subgoals . Method unifies with the current subgoal, and with the first suitable assumption. The subgoal is then replaced with the subgoals , and the assumption is deleted. Method unifies with the first suitable assumption, which it then deletes. It then adds the subgoals , and the original subgoal gains the assumption . Method is like , but it does not delete .

0 views

Crafting a dependent typechecker, part 1

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 be interested in implementing their own dependent language. This series does assume a small base amount of knowledge around dependent programming languages. There are many tutorials out there far better than I could provide, so I will refer the reader to the wider internet if they are curious. (Return here afterwards, though!). Additionally, the code snippets will be in OCaml, although a Haskell or Rust version may be made available at a later date. The technique we will implement in this series can most succinctly be described as "Bidirectional typechecking, utilizing Normalization by Evaluation". I do not expect the reader to understand that sentence for at least a little while ;). All code snippets will be collated at the end of each page, so scroll all the way down if you're only interested in that. The following are resources I highly recommend for exploring this topic on your own. If you have implemented a typechecker before, you may have come to the realization that deciding when two things are the same is a very large component of typechecking. Whether it be simply checking that two arguments to are both integers, or larger problems with polymorphism, the arguable core of typechecking is deciding equality. In a dependent language, our types can (and often do) contain expressions that must be evaluated. Therefore, in order to explore how we check equality in the presence of evaluation, we will first start by considering how we do this for a very simple language - integer arithmetic. Take two expressions: How might we decide whether these are equal? The obvious solution is to evaluate them. Indeed, (sparing the reader the derivation), we can see they both evaluate to , and so they are equal. Let us now introduce a small extension: Variables with a known value, using "let". We will refer to the variables themselves as "bound variables", as they are bound by the "let". In this case, they are additionally bound to a value. Terms containing only bound variables are referred to "closed" terms - this alludes to, for example, closed and open systems in the real world. Getting back to evaluation, we could simply substitute the computed value: And then evaluate. (In this case, our result is 117.) However, what if the variable occurs multiple times? The following is a little bad, but not awful: But what if was the following? Duplicating that would clearly not be ideal! Perhaps we could compute in advance, and then substitute that result in. This is much better: (In fact, there is yet another optimization to do: What if we don't need to compute it at all, say because it's not used? We will explore this possibility later.) A simple OCaml interpretation of the terms of this language may be the following. (sidetrack: A "term" is some element of a language. Above, we have the language of (restricted) integer arithmetic, and our terms are expressions of said. Hence, we call our OCaml interpretation of this language .) We then must make an environment that associates, or "binds", our names to terms. is often called a "binder" because it functions as the source of this binding. We will make our context a list of pairs , and will reimpliement the lookup function for example's sake, although a suitable function is available as . Note: In this series, we will not be considering the possibility that a name is used without being previously defined in some way. This is an error, and can be handled via normals means, e.g. erroring. We now note something curious: Our lookup function need not return a fully computed value! It could return , which we would have to further evaluate before we could do anything with. It would be possible of course to manually insert invariants ensuring that this is not the case, but we could still accidentally violate them. Here we hit one of the most important distinctions in our exploration of dependent typechecking. A "term", as previously seen, is any element of a chosen language. Above, this was (some subset of) integer arithmetic. We could also consider the language of OCaml programs, of which the above examples would be terms. However, two terms are not always easy to compare. We may need to evaluate one, or both, and we don't know whether that will be needed until we start comparing them. Instead, what if we defined another type that was guaranteed to be reduced to some suitable level? For this simple case, we could restrict this to contain only fully evaluated terms (i.e., integers). We prefix these constructors with to ensure they're distinct. Then, we could modify our environment and lookup function to only deal with values: and now we know that will always return something we can handle immediately, with no further processing. In the general case, we call this "suitably-reduced" constraint a "normal form". We can say that contains only elements of in this chosen normal form. Now we can finish our little evaluator. We do a slight hack to perform arithmetic inside values; if our value type contained more than just the constructor , we would have to consider how to handle that case. This is something we will cover soon. In the case, we compute the definition first, then extend our environment with the new name and value before computing the rest of the expression. We then, by returning a , have a guarantee that whatever comes out of is as simple as we want it to be. Comparing for equality is then very simple: We use to evaluate our terms into values, then because our values are in a nice normal form, we can compare them easily guaranteed. So far we have covered: In the next part, we will explore how to take these concepts and apply them to something much closer to a "real" programming language, with expressions and application, which will require the introduction of a "closure". From there, we can explore how to deal with open terms, containing free variables, and onwards to dependent types. András Kovacs' "Elaboration Zoo", found here . It was a primary source of inspiration for this series. "A tutorial implementation of a dependently typed lambda calculus", by Andres Löh, Conor McBride, and Wouter Swierstra; found here . "Checking Dependent Types with Normalization by Evaluation: A Tutorial", by David Christiansen, found here , for the more lisp-minded. Languages and terms. Simple evaluation strategies for let bound variables & closed terms. Values and normal forms.

0 views

Debruijn indexes and levels, and why they're handy

At least a familiarity with the lambda calculus, including how it is evaluated. Some base knowledge of programming languages is also assumed. Let's look at a little imaginary term, in some lambda-calculus-like language. For future note, we call the lambda a "binder", as it binds a variable. There are other types of binders, e.g. , but we will only consider lambdas for the moment. We can perform what's called "beta reduction" on this term — essentially, function application, applying to the lambda. Uh oh. We've accidentally captured a variable! Instead of referring to the outer , now it refers to the inner . This is "the capture problem", and it is quite annoying. Generally to avoid this, we need to rename everything 1 in our "substituted" term to names that are free (do not occur) in the "subsitutee" so nothing is accidentally captured. What if we could introduce a notation that avoids this? De Bruijn indexes are a naming scheme where: Let's rewrite that term above using this system: Here's some ascii art showing what refers to what: Now, how does this help us with our substituion problem? Surely if we naively subtitute we will still have binding issues - and indeed we do: What De Bruijn indexes allow us to do is simply avoid capturing. The rule is simple: Every time we go past a binder when substituting, we increment every free variable 2 in our substituted term by one, to avoid the new binder. Just once, we decrement every free varible in the substitutee, to account for the removal of the binder: Now we're cool! Everything works as expected, and it takes much less work (and is much more predictable!). At the bottom of this post there's a little widget that can convert terms to de Bruijn for you, if you want to play around! De Bruijn levels work similar to De Bruijn indexes, in that we use numbers to refer to binders. However, in De Bruijn levels, the lowest number refers to the least recently bound item. Recall that: Now, with levels: This has the same diagram of what refers to what: (As it should! These two representations represent the same term.) As you might expect, de Bruijn indexes and levels are each beneficial in their own situations. Generally, De Bruijn indexes are "more useful" than De Bruijn levels, as they're "more local". In order to work with levels, you need to know "how deep" you are in a term at all times. De Bruijn indexes give us the advantage that we can freely create new binders without the need for any information about where in a term we are, whereas de Bruijn levels give us the advantage when moving a term under a binder, free variables in said term do not need to be modified. Generally, one has many more free variables in a term than bound ones. Something that can come up quite a lot in various contexts is comparing whether two terms are equal or not. There are many complicated ways to do so, but de Bruijn gives us an advantage in a critical one, called "alpha-equivalence". Consider the following two terms: These terms should clearly be equal, right? They do the exact same thing. In this case, we consider them "alpha-equivalent", meaning they are equal up to the names of variables. Alpha renaming is the process of renaming one term to match the names of another, so that they are "clearly" equal. Let us consider the de Bruijn index representation of both of these terms: Isn't that nice? They've gone from being alpha-equivalent, but not quite equal, to being equal. de Bruijn gives us the ability to compare terms for equality without having to consider alpha-equivalence at all. De Bruijn indexes and levels can also be summed up via the following: if you’re “here” Try it out! Some example terms to try: (sorry, it does over-parenthesize a bit :P) It is worth noting that there are several other methods for gaining the same, or similar, advantages as de Bruijn gives. This post is not intended to explain them, but I will list several here so that the curious reader may read further (tip: when searching, append "lambda calculus" to find the right results quicker): As you can see, there are many approaches! Jesper Cockx has an excellent summary of almost all of these, which can be found here. Notably, many are intended for formalization efforts rather than for computational usage. Technically, this is not actually needed. It is sufficient to keep track of everything and rename only names that would overlap. See here for more. ↩ A free variable is one that is not bound by the expression we are currently considering. For example, in , is free, but is not. ↩ We use natural numbers to refer to lambdas, and Zero refers to the "most recent" lambda; one refers to the second most recent, etc. Using indexes, adding any binders further left doesn’t affect the current binder's variables, or any further right. Using levels, adding any binders further right doesn’t affect the current binder's variables, or any further left. HOAS, or "Higher Order Abstract Syntax" PHOAS, or "Parametric HOAS" Locally nameless Nominal signatures Well-scoped de Bruijn indices Well-scoped names “Nameless, Painless” Abstract scope graphs Abstract Binding Trees Co-de Bruijn indices Technically, this is not actually needed. It is sufficient to keep track of everything and rename only names that would overlap. See here for more. ↩ A free variable is one that is not bound by the expression we are currently considering. For example, in , is free, but is not. ↩

0 views

Dependent types suck actually

STOP DOING DEPENDENT TYPES Look at what computer scientists have been doing, with all the languages and typecheckers we built for them: (This is REAL dependent types, done by REAL computer scientists) "Hello I would like apples please" they have played us for absolute fools Agda credit: 1Lab Lean credit: Mathlib4 Roqc credit: 4 Color Theorem Proof 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 of something. Please give me of it." -- Statements dreamed up by the UTTERLY INSANE Agda credit: 1Lab Lean credit: Mathlib4 Roqc credit: 4 Color Theorem Proof

0 views

A short excerpt on pattern unification

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: Here, we have that our type argument to is a hole, so we must solve it. We are working with a de Brujin representation, so the above actually looks something like: Once we've gotten to the point of writing that hole, what was once is now (Two levels of lambda binders in the way.). As such, performing this solving takes slightly more work, as we can't simply plug in the result of unification - the de Brujin wouldn't line up. In this conversation, we were discussing relative to András Kovács' excellent "elab-zoo", found here . We are discussing and in particular, the former being a formal treatment of what happens after you find a solution, and the latter being an implementation of pattern unification (amongst other things). I think this explanation is somewhat reasonable for what's actually happening. Nothing will replace the original document, of course! Go give that a read (preferably before you read this.) This conversation is only going to make sense if you've had a look at at least the latter linked file above ( ). I recommend also having a look at if you really want to grasp it, though. I also make no concrete warning that the below is 100% correct; while it is to the best of ability, i'm still learning this too! (In reference to ) most of this is what you do after you've "found the solution" finding the "solution" is vaguely your normal unification procedure when you find a hole, you put a meta in it, when you unify something with that meta you "solve" it "Normal unification" here is your fairly traditional unification for typechecking; it is somewhat different in a dependent setting, but not too different. (Look here later for a series on this!) All of the following is then discussing and the concrete implementation of solving a metavariable. This maps somewhat closely from , but can be understood standalone. Andras' puts it better than i could: A small break while I write the following is what elab-zoo calls the thing holding an unsolved metavariable (here or ), and a "spine" , which is a list of everything bound in the context when was created you can then imagine the meta to be, essentially, a function, taking everything bound as arguments (which is what it actually is, in elab zoo) here our normal typechecking would try to unify 's with the actual solving is then handled by : would be our here you need to remember we're working with debrujin, so the solution to our metavariable (which may reference things in the context of where the meta was created, of course) should exist in a different context (a "mostly" empty one, with only the arguments to our meta). , which is in the pattern unification text, creates a renaming from our original context ( ) to the desired new context, with only our meta arguments takes our and uses the renaming to take it to the new context (it takes as an argument because it does an occurs check at the same time, recursive solutions are no good) finally we add the needed lambdas for our function meta (debrujin, remember), evaluate it in the empty context in order to take it into the value domain, and plug it in as the solution so then our final solution is ?m is fully inline though, so which is obviously equal to the "clear solution" and so clearly we've solved it! I don't really have any other comments. There will (hopefully shortly) start appearing a "tutorial" sort of series on writing a dependent language with holes, so some of this will definitely come up in that, and I'll probably write some more comments here after i've gone and written that tutorial. Hope this helps somebody!

0 views

Hi, world.

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\) $$\forall a. \forall b. (\forall c. c \to c) \to (a, b) \to (a, b)$$

0 views