Skip to content

Instantly share code, notes, and snippets.

Larry Diehl larrytheliquid

View GitHub Profile
eborden /
Last active May 16, 2019
Run ghcid in a monorepo via stack
project=$(basename "$(pwd)")
# build dependencies
build_deps="stack build $project --fast --pedantic --dependencies-only --interleaved-output"
# restart on changes in other packages
restarts=$(find ../. -maxdepth 1 -type d \
-not -name "$project" \
-not -name .stack-work \
-not -name . \
UlfNorell / Fulcrum.agda
Created Apr 27, 2018
Challenge 3 of the Great Theorem Prover Showdown
View Fulcrum.agda
-- Problem 3 of @Hillelogram's Great Theorem Prover Showdown.
-- Implemented using current stable-2.5 branch of Agda
-- ( and the agda-prelude
-- library (
module Fulcrum where
open import Prelude hiding (_≤?_)
View CoList.agda
{-# OPTIONS --copatterns #-}
module CoList where
{- High-level intuition:
codata CoList (A : Set) : Set where
nil : CoList A
cons : A → CoList A → CoList A
append : ∀{A} → CoList A → CoList A → CoList A
puffnfresh / Main.idr
Created Oct 14, 2016
Type-safe printf, using runtime provided strings. An extension on
View Main.idr
module Main
%default total
data Format
= FInt -- %d
| FString -- %s
| FOther Char -- [a-zA-Z0-9]
format : List Char -> List Format
jozefg / PickRandom.hs
Last active Aug 3, 2017
A simple trick to pick a random element from a stream in constant memory
View PickRandom.hs
{-# LANGUAGE FlexibleContexts #-}
module PickRandom where
import Data.List (group, sort)
import Control.Monad
import Control.Monad.Random (MonadRandom, getRandomR)
import qualified Control.Foldl as F
-- Pick a value uniformly from a fold
pickRandom :: MonadRandom m => a -> F.FoldM m a a
pickRandom a = F.FoldM choose (return (a, 0 :: Int)) (return . fst)
edwinb / fakechar.idr
Created Aug 10, 2015
Faked overloaded strings
View fakechar.idr
data FakeChar = A | B | C
data ValidMyString : List Char -> Type where
VA : ValidMyString xs -> ValidMyString ('a' :: xs)
VB : ValidMyString xs -> ValidMyString ('b' :: xs)
VC : ValidMyString xs -> ValidMyString ('c' :: xs)
VNil : ValidMyString []
implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)}
-> List FakeChar
dmalikov / README.markdown
Last active May 31, 2019
Nix / NixOS links
View README.markdown

Various blog posts related to Nix and NixOS


copumpkin / RuntimeTypes.agda
Last active Jul 24, 2018
Simulating "type providers" in Agda
View RuntimeTypes.agda
module RuntimeTypes where
open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All
callistabee / mergesort.lhs
Last active Mar 21, 2019
Haskell Implementation of Mergesort
View mergesort.lhs
- 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 / proofs.sml
Last active Jan 2, 2016
Constructive proofs in SML's module language
View proofs.sml
(* 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,
You can’t perform that action at this time.