april cyberglot

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

I had a fun refactoring example in Haskell today I wanted to share. So, I've got a structure with a nested Maybe inside, which looked like this:

Maybe (Vector.Vector (Maybe (Direction, [Departure])))

I wanted to get that second-level Maybe folded into the first as it didn't provide any semantic meaning. So I start by writing the type definition:

This document has moved!

It's now here, in The Programmer's Compendium. The content is the same as before, but being part of the compendium means that it's actively maintained.

This is unmaintained, please visit Ben-PH/spacemacs-cheatsheet

Useful Spacemacs commands

SPC q q - quit
SPC w / - split window vertically
SPC w - - split window horizontally
SPC 1 - switch to window 1
SPC 2 - switch to window 2
SPC w c - delete current window

These links no longer work. Springer have pulled the free plug.

Graduate texts in mathematics

duplicates = multiple editions

A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen

Pulp Flycheck

Defines a Flycheck checker for running the PureScript compiler through Pulp. Based on Bodil's Stokke's: https://github.com/bodil/ohai-emacs/blob/master/modules/ohai-purescript.el#L43

Supports:

Standard compiler error messages
psc: deprecation messages
Syntax errors

	/*:

	This is an implementation of Algorithm W, as found in [Principal Types for functional programs](http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf).

	We'll start by defining literals and expressions:
	*/

	enum Literal {
	case string(String)
	case int(Int)

	module Main where

	import Prelude
	import Data.List
	import Data.Either (Either(..))
	import Data.Maybe (Maybe(..))
	import Data.Newtype (class Newtype, unwrap)
	import Data.Tuple (Tuple(..), fst, snd)

	import Unsafe.Coerce (unsafeCoerce)

	{-# LANGUAGE GeneralizedNewtypeDeriving #-}

	import Control.Monad.IO.Class
	import Control.Monad.Trans.Class
	import Prelude hiding (log)

	--------------------------------------------------------------------------------
	-- The API for cloud files.
	class Monad m => MonadCloud m where
	saveFile :: Path -> Bytes -> m ()