Skip to content

Instantly share code, notes, and snippets.

var db = database "links";
var agencies =
table "agencies"
with (oid: Int,
id: Int,
name: String,
based_in: String,
phone: String)
where oid readonly
open function
lemma ideminvoid (A : Type)
(f : A -> A)
(f_idem : forall x, f (f x) = f x)
(f_invo : forall x, f (f x) = x)
: forall x, f x = id x :=
take x, calc f x = f (f x) : f_idem
... = x : f_invo
... = id x : rfl
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
@fehrenbach
fehrenbach / shredding.hs
Created December 4, 2014 16:35
Query shredding queries in Database-supported Haskell
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
@fehrenbach
fehrenbach / hbtf.hs
Last active August 29, 2015 14:10
Example query from Haskell boards the Ferry, George Giorgidze et al., IFL 2010
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
#Colorful prompt, shows current git branch
PS1='\[\033[01;32m\]\u\[\033[00m\]@\[\033[01;32m\]\h\[\033[00m\]:\[\033[01;34m\]\w\[\033[00m\]\[\033[0;36m\]`git branch 2>/dev/null|cut -f2 -d\* -s`\[\033[00m\]\$ '
user=> (do (defn foo [bar] (inc bar))
(prn (foo 1))
(time (defn foo [bar] (dec bar)))
(foo 1))
2
"Elapsed time: 0.189684 msecs"
0
import XMonad
import XMonad.Actions.UpdatePointer
import XMonad.Config.Desktop
import XMonad.Hooks.DynamicLog
import XMonad.Hooks.ManageDocks
import XMonad.Hooks.ManageHelpers
import XMonad.Hooks.EwmhDesktops
import XMonad.Hooks.SetWMName
import XMonad.Layout.PerWorkspace
import XMonad.Layout.Reflect
import XMonad
import XMonad.Actions.UpdatePointer
import XMonad.Config.Desktop
import XMonad.Hooks.DynamicLog
import XMonad.Hooks.ManageDocks
import XMonad.Hooks.ManageHelpers
import XMonad.Hooks.EwmhDesktops
import XMonad.Hooks.SetWMName
import XMonad.Layout.PerWorkspace
import XMonad.Layout.Reflect
#!/usr/bin/env xdg-open
[Desktop Entry]
Version=1.0
Name=Google+
Exec=chromium --app=https://plus.google.com/
Terminal=false
Icon=chrome-https___plus.google.com_
Type=Application
Categories=GTK;Network;WebBrowser;
StartupWMClass=plus.google.com