Skip to content

Instantly share code, notes, and snippets.

import java.sql.DriverManager
import scalaz.concurrent.Task
import scalaz.stream.io
import scalaz.stream.Process.End
val url = "jdbc:postgresql://localhost/lwarner"
class Query(query: String) { val connection = DriverManager.getConnection(url, "lwarner", "password"); val statement = connection.createStatement; val resultSet = statement.executeQuery(query); def next = resultSet.next; def getString(i:Int) = resultSet.getString(i); def close { resultSet.close; statement.close; connection.close } }
@LeifW
LeifW / scalaz-stream-jdbc.scala
Last active August 29, 2015 14:01
scalaz-stream + jdbc
import java.sql.DriverManager
import scalaz.concurrent.Task
import scalaz.stream.io
import scalaz.stream.Process.End
class Query(query: String, chunkSize: Int) {
Class forName "org.postgresql.Driver"
val connection = DriverManager.getConnection(url, "username", "password")
val statement = connection.createStatement
// This will cause the postgres driver to create a cursor and give ResultSets of that size
class Monoidy (A : Type) where
empty : A
append : A → A → A
left_neutrality : (x : A) → append empty x = x
right_neutrality : (x : A) → append x empty = x
associativity : (x, y, z : A) → append x (append y z) = append (append x y) z
instance Monoidy Bool where
empty = False
append True b = True
@LeifW
LeifW / postulate.hs
Last active August 29, 2015 14:02
Use of postulate in Idris typeclass law
%default total
class Semigroupy a where
op: a -> a -> a
semigroupOpIsAssociative : (x, y, z : a) -> op x (op y z) = op (op x y) z
instance Semigroupy Int where
op = (+)
semigroupOpIsAssociative x y z = believe_me "sure, yeah, whatever"
%default total
class Functor F => VerifiedFunctor (F : Type -> Type) where
fla : (m : F a) -> map id m = m
flw : (f : b -> c) -> (g : a -> b) -> (m : F a) -> map (f . g) m = ((map f) . (map g)) m
class Applicative F => VerifiedApplicative (F : Type -> Type) where
flaw : (f : a -> b) -> (m : F a) -> map f m = pure f <$> m
--flaw : (fn : a -> b) -> (x : f a) -> map fn x = the (f b) (ap (pure fn) x)
--flaw : (fn : a -> b) -> (x : f a) -> map fn x = the (f b) (ap (pure fn) x)
@LeifW
LeifW / Foo.hs
Created June 27, 2014 23:36
parametricity?
module Foo
class Blah a where
fuzz : String
instance Blah Int where
fuzz = "Int"
instance Blah String where
fuzz = "String"
html do
head do
title "Stuff"
body do
p1 "Hello"
@LeifW
LeifW / machines.hs
Last active August 29, 2015 14:04 — forked from pchiusano/machines.hs
-- Type-aligned sequence catenable queue supporting O(1) append, snoc, uncons
-- Don't need it to be a dequeue (unsnoc not needed)
data TCQueue c a b -- c is the category, a is starting type, b is ending type
type Channel f a b = TCQueue (Transition f) a b
type Process f b = Channel f () b
data Transition f a b where
Bind :: (a -> Process f b) -> Transition f a b
OnHalt :: (Cause -> Process f b) -> Transition f a b
@LeifW
LeifW / natAssoc.idr
Created August 18, 2014 23:31
Trying to translate Idris proof to Scala
total natAssoc : (x, y, z : Nat) → x + (y + z) = (x + y) + z
natAssoc Z y z = refl
natAssoc (S k) y z = cong $ natAssoc k y z
/*
* This is the Towers of Hanoi example from the prolog tutorial [1]
* converted into Scala, using implicits to unfold the algorithm at
* compile-time.
*
* [1] http://www.csupomona.edu/~jrfisher/www/prolog_tutorial/2_3.html
*/
object TowersOfHanoi {
import scala.reflect.Manifest