tonymorris

import Control.Lens
import Data.Monoid

newtype Compose f g a =
  Compose (f (g a))

instance (Foldable f, Foldable g) => Foldable (Compose f g) where
  foldr f z (Compose x) =
    foldr (\a b -> foldr f b a) z x

tonymorris

abstract class IntOrString {
  private IntOrString() {}

  public static class IsInt extends IntOrString {
    private final int i;

    public IsInt(int i) {
      this.i = i;
    }

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March 2015

open import Agda.Primitive using (_⊔_)

postulate
  String : Set

{-# BUILTIN STRING String #-}

mbrcknl

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Definition rev_spec (X: Type) (rev: list X -> list X) :=
  (forall x, rev [x] = [x]) /\ (forall xs ys, rev (xs ++ ys) = rev ys ++ rev xs).

Lemma app_eq_nil: forall (X: Type) (xs ys: list X), xs ++ ys = xs -> ys = [].
  induction xs; simpl; inversion 1; auto.

aaronlevin

{-# LANGUAGE OverloadedStrings #-}

module SimpleThings where

import Control.Applicative ((<$>), (<*>))
import Control.Monad (mzero)
import Data.Aeson
import qualified Data.Aeson as A

-- | sum type containing all possible payloads

nkpart

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# OPTIONS_GHC -fwarn-missing-methods #-}
module Err where

import Control.Lens
import Control.Monad.Error
import Control.Monad.Error.Lens

-- Here is a fairly typical situation, where we have low level errors in certain

mbrcknl

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Fixpoint reverse (X: Type) (xs: list X): list X :=
  match xs with
    | [] => []
    | x :: xs' => reverse xs' ++ [x]
  end.

nkpart

{-# LANGUAGE GADTs #-}
module Yolo where

import System.IO.Unsafe

class Yolo f where
  yolo :: f a -> a

instance Yolo Maybe where
  yolo (Just x) = x

mbbx6spp

Gerrit vs Github: for code review and codebase management

Sure, Github wins on the UI. Hands down. But, despite my initial annoyance with Gerrit when I first started using it almost a year ago, I am now a convert. Fully. Let me tell you why.

Note: This is an opinionated (on purpose) piece. I assume your preferences are like mine on certain ideas, such as:

• Fast-forward submits to the target branch are better than allowing merge commits to the target branch. The reason I personally prefer this is that, even if a non-conflicting merge to the target branch is possible, the fact that the review/pull request is not up to date with the latest on the target branch means feature branch test suite runs in the CI pipeline reporting on the review/PR may not be accurate. Another minor point is that forced merge commits are annoying as fuck (opinion) and clutter up Git log histories unnecessarily and I prefer clean histories.
• Atomic/related changes all in one commit is something worth striving for. Having your dev

mbrcknl

-- Is Set.union better than O(n+m) in some cases?

import Criterion.Main (Benchmark, bench, bgroup, defaultMain, env, whnf)
import Data.Set (Set, fromList, union)

main :: IO ()
main = defaultMain [ bgroup "union" $ map benchUnion sizes ]

-- Grow Set size exponentially, under the hypothesis that
-- Set.union will be O(log n) in this special case.