This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 } } | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%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" | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Foo | |
class Blah a where | |
fuzz : String | |
instance Blah Int where | |
fuzz = "Int" | |
instance Blah String where | |
fuzz = "String" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
html do | |
head do | |
title "Stuff" | |
body do | |
p1 "Hello" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* | |
* 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 |
OlderNewer