Skip to content

Instantly share code, notes, and snippets.

@co-dan
co-dan / Automata.hs
Last active December 12, 2015 00:09
module Automata where
import Prelude hiding (or, foldl)
import Control.Monad
import Data.Foldable hiding (elem)
import Control.Monad.Identity
data Automata q s m = A { states :: [q]
, trans :: (q, s) -> m q
{-# LANGUAGE OverloadedStrings, DeriveDataTypeable, ScopedTypeVariables #-}
import Database.PostgreSQL.Simple
import Database.PostgreSQL.Simple.FromRow
import Database.PostgreSQL.Simple.FromField
import Data.Typeable
import Control.Applicative
> showReadIso :: Expr -> Bool
> showReadIso e = parseExpr (show' e) == e
*Tests> quickCheck showReadIso
*** Failed! Falsifiable (after 34 tests):
Prod (Variable "d") (Prod (Variable "b") (Universe 9) (Prod (Variable "a") (Prod (Variable "c") (Var (Variable "a")) (App (Lambda (Variable "c") (Var (Variable "b")) (Universe 8)) (Prod (Variable "a") (Universe 1) (Var (Variable "c"))))) (Prod (Variable "b") (Lambda (Variable "c") (App (Universe 2) (Universe 5)) (Var (Variable "c"))) (App (Var (Variable "b")) (Lambda (Variable "d") (Var (Variable "a")) (Universe 7)))))) (App (Prod (Variable "a") (Lambda (Variable "d") (Universe 9) (Prod (Variable "a") (App (Var (Variable "b")) (Var (Variable "d"))) (App (Var (Variable "a")) (Var (Variable "a"))))) (Prod (Variable "a") (App (Prod (Variable "c") (Var (Variable "b")) (Var (Variable "c"))) (Prod (Variable "d") (Var (Variable "b")) (Universe 10))) (Prod (Variable "d") (Lambda (Variable "a") (Var (Variable "c")) (Var (Variable "d"))) (Prod (Variable "c") (Universe 5) (
@co-dan
co-dan / gist:4358385
Created December 22, 2012 10:37
Generating HTML page from Calibre's catalog
{-# LANGUAGE OverloadedStrings, ScopedTypeVariables #-}
module Main where
import Text.Blaze.Html5
import qualified Text.Blaze.Html5 as H
import Text.Blaze.Html5.Attributes
import qualified Text.Blaze.Html5.Attributes as A
import Text.Blaze.Html.Renderer.Pretty
import Data.Csv
@co-dan
co-dan / MaybeT.hs
Created December 13, 2012 08:38
Maybe monad transformer
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
module MaybeT where
-- Maybe monad transformer
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State
newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }
(* Kevin Sullivan <[email protected]>, writing to the Coq-Club: *)
(* My students presented two solutions to the simple problem of applying a *)
(* function f n times to an argument x (iterated composition). The first says *)
(* apply f to the result of applying f n-1 times to x; the second, apply f n-1 *)
(* times to the result of applying f to x. I challenged one student to prove that *)
(* the programs are equivalent. This ought to be pretty easy based on the *)
(* associativity of composition. Your best solution? *)
Fixpoint ant {X: Type} (f: X->X) (x: X) (n: nat) : X :=
match n with
#!/usr/bin/perl
use Irssi;
use vars qw($VERSION %IRSSI);
use warnings;
use strict;
##use common::sense;
##use Modern::Perl 2012;
Irssi::command_bind smile => \&smile;