Joomy Korkut joom

fpco decided to do their own thing instead of contributing to that effort.

Your timeline is way off. The initial announcement for what would become Stackage was posted in 2012, a full three years before the post you linked was authored (and a year before Cabal got sandboxes!). The proposal blog post doesn't even mention diverging from cabal at all, and the official way to use stackage was through cabal sandboxes. The first public beta of stack was announced in June 2015, and according to the blog post, FPCo had been working on stack internally for about a year before that. If these timelines are to be believed, then stack was six months into internal produ

A Self-Taught Course in Automated Reasoning using Haskell

Variables, Terms, and Syntactic Unification

Resources

[Introduction to Unification Theory Lecture 1][itut-1]
Sections 8.1 and 8.2 of [The Handbook of Automated Reasoning][hoar]

Exercises

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;

	{-# LANGUAGE
	DataKinds
	, TypeApplications
	, TypeFamilies
	, TypeOperators
	, TypeInType
	, KindSignatures
	, ExistentialQuantification
	, InstanceSigs
	, ScopedTypeVariables

	--Roughly based on https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs by Gabriel Gonzalez et al.

	data Expr = Star \| Box \| Var Int \| Lam Int Expr Expr \| Pi Int Expr Expr \| App Expr Expr deriving (Show, Eq)

	subst v e (Var v') \| v == v' = e
	subst v e (Lam v' ta b ) \| v == v' = Lam v' (subst v e ta) b
	subst v e (Lam v' ta b ) = Lam v' (subst v e ta) (subst v e b )
	subst v e (Pi v' ta tb) \| v == v' = Pi v' (subst v e ta) tb
	subst v e (Pi v' ta tb) = Pi v' (subst v e ta) (subst v e tb)
	subst v e (App f a ) = App (subst v e f ) (subst v e a )

	-- A simply-typed lambda calculus, and a definition of normalisation by
	-- evaluation for it.
	--
	-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
	-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
	--
	-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
	-- consider open terms with the environments left implicit/untyped). This was a
	-- pain in the ass to figure out.

	interface Group a where
	(<*>) : a -> a -> a
	inv : a -> a
	e : a
	lAssoc : (x <> y) <> z = x <> (y <> z)
	rAssoc : x <> (y <> z) = (x <> y) <> z
	lId : e <*> x = x
	rId : x <*> e = x
	lInv : inv x <*> x = e
	rInv : x <*> inv x = e

	module HillelVerificationProblems where

	open import Data.Nat
	open import Data.Nat.Properties.Simple using (+-right-identity; +-comm)
	open import Data.List
	open import Data.List.All
	open import Data.List.Properties
	open import Relation.Binary.PropositionalEquality

	-- NB. (a ∸ b) is saturating subtraction and (a ⊔ b) is max(a,b).

	Require Import Lists.List.
	Require Import Arith.Arith.

	Require Import Omega.

	Set Implicit Arguments.

	Fixpoint replicate A (n : nat) (x : A) : list A :=
	match n with
	\| O => nil

	-- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris
	import Data.Vect

	-- `minus` is saturating subtraction, so this works like we want it to
	eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
	eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
	eq_max Z (S _) = Refl
	eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

	-- The type here says "the result is" padded to (maximum k n), and is padding plus the original