Skip to content

Instantly share code, notes, and snippets.

View larrytheliquid's full-sized avatar

Larry Diehl larrytheliquid

View GitHub Profile
{-# 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
@jozefg
jozefg / PickRandom.hs
Last active August 3, 2017 13:55
A simple trick to pick a random element from a stream in constant memory
{-# 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)
@UlfNorell
UlfNorell / Fulcrum.agda
Created April 27, 2018 11:04
Challenge 3 of the Great Theorem Prover Showdown
-- 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 (_≤?_)
@puffnfresh
puffnfresh / Main.idr
Created October 14, 2016 10:49
Type-safe printf, using runtime provided strings. An extension on https://gist.github.com/puffnfresh/11202637
module Main
%default total
data Format
= FInt -- %d
| FString -- %s
| FOther Char -- [a-zA-Z0-9]
format : List Char -> List Format
@copumpkin
copumpkin / RuntimeTypes.agda
Last active July 24, 2018 19:01
Simulating "type providers" in 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
@eborden
eborden / stack-ghcid.sh
Last active May 16, 2019 14:43
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 . \
@dmalikov
dmalikov / README.markdown
Last active May 31, 2019 06:31
Nix / NixOS links

Various blog posts related to Nix and NixOS


General

@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
@gatlin
gatlin / sat.hs
Created February 6, 2012 23:05
SAT Solver in Haskell
-- This is going to be on Hackage soon! https://github.com/gatlin/surely
{-# LANGUAGE BangPatterns #-}
-- |
-- Module : AI.Surely
-- Copyright : 2012 Gatlin Johnson
-- License : LGPL 3.0
-- Maintainer : rokenrol@gmail.com
-- Stability : experimental