timjb

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

timjb

{-# LANGUAGE RankNTypes #-}

module TraversalIso where

import Control.Lens.Traversal
import Control.Monad.State.Lazy
import Data.Traversable (Traversable (..))

{-
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

timjb

import Test.QuickCheck
import Control.Applicative ((<$>))
import Data.List (scanl)

-- To test whether my timsort implementation has the bug described in
-- http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
-- Answer: yes :-(

runLengthInvariantBroken :: (Num i, Ord i) => i -> i -> i -> i -> Bool
runLengthInvariantBroken a b c i = (b - a <= i - b) || (c - b <= i - c)

timjb

Veganes Mousakás

(Rezept von Nina Baumann)

Zutaten

(für eine kleine Auflaufform, 3-4 Personen)

• 200g Sojagranulat
• 1l Gemüsebrühe

timjb

{-# LANGUAGE BangPatterns #-}

module Main (main) where

import Criterion.Main
import Data.Bits

main :: IO ()
main = defaultMain benchmarks
  where

timjb

module SubstIrrelevant where

open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Nullary

-- Irrelevant in ⊥
⊥-elim′ : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
⊥-elim′ ()

timjb

module IrrelevantTest where

open import Relation.Nullary.Core
open import Data.Empty

⊥-elim′ : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
⊥-elim′ ()

test : {A : Set} → .A → Dec A → A
test a (yes p) = p

timjb

-- developed for https://gist.github.com/timjb/e3e85f961781b088e88b

module Main where

import Control.Monad (forM_)
import Data.Monoid ((<>))

data Action = Noop | InsertChar | RetainChar | DeleteChar | InsertTombstone | RetainTombstone
  deriving (Show, Eq, Ord)

timjb

-- this agda module depends on https://github.com/copumpkin/categories

-- inspired by https://gist.github.com/aristidb/1746133

open import Level
open import Categories.Category
open import Categories.Functor.Core
open import Categories.Agda
open import Categories.Product
--open import Categories.Bifunctor

timjb

-- this agda module depends on https://github.com/copumpkin/categories

module Categories.OTCategory (C : Set) where

-- inspired by https://gist.github.com/aristidb/1746133

open import Level
open import Categories.Category
open import Categories.Functor.Core
open import Categories.Agda