Skip to content

Instantly share code, notes, and snippets.

View larrytheliquid's full-sized avatar

Larry Diehl larrytheliquid

View GitHub Profile
@callistabee
callistabee / mergesort.lhs
Last active February 10, 2021 06:39
Haskell Implementation of Mergesort
- Haskell Mergesort
- Copyright (C) 2014 by Kendall Stewart
First we define a couple of helper functions that
will be useful in splitting the list in half:
> fsthalf :: [a] -> [a]
> fsthalf xs = take (length xs `div` 2) xs
@jonsterling
jonsterling / proofs.sml
Last active January 2, 2016 04:48
Constructive proofs in SML's module language
(* It is not possible in Standard ML to construct an identity type (or any other
* indexed type), but that does not stop us from speculating. We can specify with
* a signature equality should mean, and then use a functor to say, "If there
* were a such thing as equality, then we could prove these things with it."
* Likewise, we can use the same trick to define the booleans and their
* induction principle at the type-level, and speculate what proofs we could
* make if we indeed had the booleans and their induction principle.
*
* Functions may be defined by asserting their inputs and outputs as
* propositional equalities in a signature; these "functions" do not compute,
@timjb
timjb / AboutMe.mustache
Created December 1, 2013 15:27
Mustache templating in Idris
Hello, my name ist {{name}} and I am {{age}} years old.
@mwhite
mwhite / git-aliases.md
Last active March 25, 2024 07:26
The Ultimate Git Alias Setup

The Ultimate Git Alias Setup

If you use git on the command-line, you'll eventually find yourself wanting aliases for your most commonly-used commands. It's incredibly useful to be able to explore your repos with only a few keystrokes that eventually get hardcoded into muscle memory.

Some people don't add aliases because they don't want to have to adjust to not having them on a remote server. Personally, I find that having aliases doesn't mean I that forget the underlying commands, and aliases provide such a massive improvement to my workflow that it would be crazy not to have them.

The simplest way to add an alias for a specific git command is to use a standard bash alias.

# .bashrc
@ntc2
ntc2 / LC.hs
Last active December 17, 2015 20:28
Scrap Your Boilerplate (SYB) based normalizer for untyped lambda calculus.
{-# LANGUAGE DeriveDataTypeable , Rank2Types , ViewPatterns #-}
import Control.Applicative
import Control.Arrow
import Control.Monad.Reader
import Control.Monad.Writer
import Data.Generics
import Data.Set (Set)
import qualified Data.Set
----------------------------------------------------------------
@larrytheliquid
larrytheliquid / LocalProps.agda
Last active December 15, 2015 03:09
How does local completeness generalize to eliminators?
{-
How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) generalize to eliminators?
Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.
Caveats:
1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
-}
@larrytheliquid
larrytheliquid / gist:3909860
Last active April 28, 2016 13:42
inductive-recursive universe for dependent types
open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
renaming ( _≟_ to _≟B_ )
open import Data.Nat using ( ℕ ; zero ; suc )
renaming ( _≟_ to _≟ℕ_ )
open import Data.Product using ( Σ ; _,_ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
@copumpkin
copumpkin / State.agda
Last active October 4, 2015 15:18
The State monad
module Categories.Agda.State where
open import Categories.Category
open import Categories.Agda
open import Categories.Agda.Product
open import Categories.Functor hiding (_≡_)
open import Categories.Functor.Product
open import Categories.Functor.Hom
open import Categories.Monad
open import Categories.Adjunction
@copumpkin
copumpkin / Routing.agda
Last active October 2, 2015 07:38
Routing
module Routing where
open import Function hiding (type-signature)
open import Data.Bool hiding (_≟_)
open import Data.Maybe
open import Data.Char hiding (_≟_)
open import Data.String as String
open import Data.List as List hiding ([_])
open import Data.Product hiding (curry; uncurry)