Skip to content

Instantly share code, notes, and snippets.

Larry Diehl larrytheliquid

View GitHub Profile
@eborden
eborden / stack-ghcid.sh
Last active May 16, 2019
Run ghcid in a monorepo via stack
View stack-ghcid.sh
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
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.
-- https://www.hillelwayne.com/post/theorem-prover-showdown
--
-- Implemented using current stable-2.5 branch of Agda
-- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude
-- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94).
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
puffnfresh / Main.idr
Created Oct 14, 2016
Type-safe printf, using runtime provided strings. An extension on https://gist.github.com/puffnfresh/11202637
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
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
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
dmalikov / README.markdown
Last active May 31, 2019
Nix / NixOS links
View README.markdown

Various blog posts related to Nix and NixOS


General

@copumpkin
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
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
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.