hirrolot

Don't use Vim

Don't do the crime, if you can't do the time.

-- Anthony Vincenzo "Tony" Baretta

Vim is an amazing text editor. I love it. Really, I wouldn't [organize][organize] a Vim advent calendar if I didn't. But, as amazing as it is, Vim is not for everyone. It can't solve all your problems, or be a TUI version of your favorite IDE, or make you a better programmer, or land you that dream job in the Bay Area. But Vim can help you be more mindful, focused, and efficient, as long as you approach it with the right mindset.

Don't get me wrong, I certainly welcome you to try Vim, but I'm not a proselyte. I don't thrive on newbies. I just want you to use the right tool for the job and not waste your—and anyone's—time on a fruitless quest.

Method for Emulating Higher-Kinded Types in Rust

Intro

I've been fiddling about with an idea lately, looking at how higher-kinded types can be represented in such a way that we can reason with them in Rust here and now, without having to wait a couple years for what would be a significant change to the language and compiler.

There have been multiple discussions on introducing higher-ranked polymorphism into Rust, using Haskell-style Higher-Kinded Types (HKTs) or Scala-looking Generalised Associated Types (GATs). The benefit of higher-ranked polymorphism is to allow higher-level, richer abstractions and pattern expression than just the rank-1 polymorphism we have today.

As an example, currently we can express this type:

ANSI Escape Sequences

Standard escape codes are prefixed with Escape:

Ctrl-Key: ^[
Octal: \033
Unicode: \u001b
Hexadecimal: \x1B
Decimal: 27

Here's a list of mildly interesting things about the C language that I learned mostly by consuming Clang's ASTs. Although surprises are getting sparser, I might continue to update this document over time.

There are many more mildly interesting features of C++, but the language is literally known for being weird, whereas C is usually considered smaller and simpler, so this is (almost) only about C.

1. Combined type and variable/field declaration, inside a struct scope [https://godbolt.org/g/Rh94Go]

struct foo {
   struct bar {
 int x;

	{-
	At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

	"A simple and efficient implementation of strong call by need by an abstract machine"
	https://dl.acm.org/doi/10.1145/3549822

	This is right up my alley since I've implemented strong call-by-need evaluation
	quite a few times (without ever doing more formal analysis of it) and I'm also
	interested in performance improvements. Such evaluation is required in
	conversion checking in dependently typed languages.

	(* The syntax of our calculus. Notice that types are represented in the same way
	as terms, which is the essence of CoC. *)
	type term =
	\| Var of string
	\| Appl of term * term
	\| Binder of binder * string * term * term
	\| Star
	\| Box

	and binder = Lam \| Pi

	data Fmt = FArg Fmt \| FChar Char Fmt \| FEnd

	toFmt : (fmt : List Char) -> Fmt
	toFmt ('*' :: xs) = FArg (toFmt xs)
	toFmt ( x :: xs) = FChar x (toFmt xs)
	toFmt [] = FEnd

	PrintfType : (fmt : Fmt) -> Type
	PrintfType (FArg fmt) = ({ty : Type} -> Show ty => (obj : ty) -> PrintfType fmt)
	PrintfType (FChar _ fmt) = PrintfType fmt

	-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
	import Data.List (delete, union)
	{- HLINT ignore "Eta reduce" -}

	-- File mnemonics:
	-- env = typing environment
	-- vid = variable identifier in Bind or Var
	-- br = binder variant (Lambda or Pi)
	-- xyzTyp = type of xyz
	-- body = body of Lambda or Pi abstraction

	const static struct _0 {} _0;
	const static struct _1 {} _1;


	#define G7_SPLICE(expr) __typeof__(expr)

	#define G7_STRUCT(...) (struct { __VA_ARGS__ } ){}


	#define G7_NAND(a, b) \

	{-# language Strict, BangPatterns #-}

	data Tm = Var Int \| App Tm Tm \| Lam Tm \| Fix Tm deriving (Show, Eq)
	data Val = VVar Int \| VApp Val Val \| VLam [Val] Tm \| VFix [Val] Tm

	isCanonical :: Val -> Bool
	isCanonical VLam{} = True
	isCanonical _ = False

	eval :: [Val] -> Tm -> Val