shuhung shhyou

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

How the J Script Works

Going line by line:

b =: >: i. 9 9 9

This generates a 9 by 9 by 9 array with all values from 1 to 729. We can choose what each axis represents: I decided that each table is all of the boolean variables for one number, and the rows and columns map to sudoku rows and columns. For example:

Racket tips and tricks

These are extracted from discussions I triggered on the Racket Slack. Thanks to everyone who participated in the discussion threads! :-)

Conversion to boolean

Use (and value #t) to convert a value to its boolean equivalent.

Entering a module in the Racket REPL

On hiring Haskellers

Recently I noticed the number of the same two questions being asked again and again on different Haskell resources. The questions were “How to get a Haskell job” and “Why is it so hard to find Haskellers?” Although these two are coming from the opposite sides of the hiring process, the answer is really just one. There is a single reason, a single core problem that causes difficulties of hiring and being hired in the Haskell community, and we should clearly articulate this problem if we want to increase the Haskell adoption.

We all know that there are many people wishing to get a Haskell job. And a visible increase of Haskell jobs looks like there should be a high demand for Haskellers. The Haskell community has also grown like crazy past years. But still, why is it so difficult to hire and to be hired? Why can’t companies just hire any single person who demonstrates a deep knowledge of Haskell in blog posts, in chats, on forums, and in talks? And why do Haskell companies avoid hirin

With scoped effects, handlers must be a part of the program

It is seductive to imagine that effect handlers in an algebraic effect system are not part of the program itself but metalanguage-level folds over the program tree. And in traditional free-like formulations, this is in fact the case. The Eff monad represents the program tree, which has only two cases:

data Eff effs a where
  Pure :: a -> Eff effs a
  Op :: Op effs a -> (a -> Eff effs b) -> Eff effs b

data Op effs a where

	open import Level
	open import Relation.Binary
	open import Data.Product
	open import Data.Unit
	open import Agda.Builtin.Sigma
	open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
	open import Relation.Binary.PropositionalEquality.Properties
	open import Function.Equality hiding (setoid)

	module Epimorphism where

	open import Data.Nat
	open import Data.Maybe
	open import Data.Product

	-- An implementation of infinite queues fashioned after the von Neuman ordinals

	module Queue where

	infixl 5 _⊕_

	{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.
	Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}

	open import Data.Empty using (⊥)
	open import Data.Unit using (⊤; tt)
	open import Data.Nat using (ℕ; zero; suc)
	open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax)
	open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)

	infix 3 _-→_ _-↛_

	{-# LANGUAGE RecordWildCards #-}
	{-# LANGUAGE DuplicateRecordFields #-}
	{-# LANGUAGE NamedFieldPuns#-}

	data C = C { c::[Int] } deriving Show
	data B = B { b::Bool, c::C } deriving Show
	data A = A { a::String, b::B } deriving Show

	mkA = A "hello world" (B True (C [1,2,3]))

	module Prims where
	primitive
	primLockUniv : Set₁

	open Prims renaming (primLockUniv to LockU) public

	postulate
	Cl : Set
	k0 : Cl
	Tick : Cl → LockU