Skip to content

Instantly share code, notes, and snippets.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module CarrierTest where
import Data.Profunctor
import Data.Profunctor.Composition
import Data.Profunctor.Strong
-- This is isomorphic to Pastro (Exchange a a)
data Carrier a x y where
@mvr
mvr / Test.idr
Last active March 4, 2016 20:22
module Test
data Chain : Nat -> Type where
MkChain : List (String, Nat) -> Chain n
data Map : Nat -> Type where
MkMap : (Chain n -> Chain (n + d)) -> Map d
compose : Map df -> Map dg -> Map (dg + df)
compose (MkMap f) (MkMap g) = MkMap go
@mvr
mvr / Test.idr
Created February 10, 2016 01:40
module Test
import Data.Fin
record AttemptA where
constructor ConstructA
goA : (n : Nat) -> Fin n -> Fin n
record AttemptB where
constructor ConstructB
@mvr
mvr / UnionFind.hs
Last active September 1, 2015 23:16
module Data.Struct.Internal.UnionFind where
import Control.Monad (when)
import Control.Monad.Primitive
import Data.Struct.Internal
-- | Union-Find
-- >>> a <- new
-- >>> b <- new
-- >>> c <- new
Test
> Line 1
>
> Line 2
@mvr
mvr / gist:8081429
Last active November 10, 2023 02:36
A Whirlwind Tour of Combinatorial Games in Haskell
A Whirlwind Tour of Combinatorial Games in Haskell
==================================================
Combinatorial games are an interesting class of games where two
players take turns to make a move, changing the game from one position
to another. In these games, both players have perfect information
about the state of the game and there is no element of chance. In
'normal play', the winner is declared when the other player is unable
to move. A lot of famous strategy games can be analysed as
combinatorial games: chess, go, tic-tac-toe.
module Math.Homology where
import Data.List ((\\), subsequences)
import Data.Maybe (fromMaybe)
import Data.Tuple (swap)
newtype Simplex a = Simplex { getVertices :: [a] } deriving (Show, Eq)
simplexDim :: Simplex a -> Int
simplexDim = (subtract 1) . length . getVertices
module Temporary
include Behaviour
def setup
Timer.in lifetime do
World.remove self
end
end
def lifetime
make all-am
make[3]: Entering directory `/home/mitchell/gnome-shell/source/gnome-shell/src'
CCLD test-theme
/home/mitchell/gnome-shell/install/lib/libgio-2.0.so: undefined reference to `g_source_get_time'
/home/mitchell/gnome-shell/install/lib/libgio-2.0.so: undefined reference to `g_main_context_invoke'
/home/mitchell/gnome-shell/install/lib/libclutter-glx-1.0.so: undefined reference to `g_object_class_install_properties'
/home/mitchell/gnome-shell/install/lib/libgio-2.0.so: undefined reference to `g_get_environ'
/home/mitchell/gnome-shell/install/lib/libgio-2.0.so: undefined reference to `g_signal_accumulator_first_wins'
/home/mitchell/gnome-shell/install/lib/libgio-2.0.so: undefined reference to `g_get_monotonic_time'
collect2: ld returned 1 exit status
def create
@number = Number.find_or_create_by_value(:value => params[:value])
if not @number.valid?
@fact = Fact.new(params[:fact])
@intended_value = @number.value
render 'facts/new' and return
end
@fact = @number.facts.new(params[:fact])