Skip to content

Instantly share code, notes, and snippets.

View davidpeklak's full-sized avatar

David Peklak davidpeklak

  • Winterthur, Switzerland
View GitHub Profile
import java.sql.{Connection, PreparedStatement}
object SqlInterpolation {
case class StatementPreparation(string: String, effect: PreparedStatement => Unit) {
override def toString: String = s"""StatementPreparation("$string", $effect)"""
}
implicit class ConnectionOps(val connection: Connection) extends AnyVal {
def prepareStatement(sp: StatementPreparation): PreparedStatement = {
@davidpeklak
davidpeklak / EffectReturn.idr
Created April 13, 2015 19:30
'return' in idris effects
module Main
import Effects
import Effect.StdIO
FOO : Type -> EFFECT
FOO t = ?FOO
------------- This works -----------
import java.util.concurrent.{TimeUnit, Executors}
import scala.annotation.tailrec
import scalaz.{\/-, -\/, \/}
import java.util.concurrent.atomic.AtomicReference
object TM {
case class Baseline[A](baseline: A)
case class Transaction[A](baseline: Baseline[A], update: A)
@davidpeklak
davidpeklak / gist:a72892ae8c67feb8af4a
Created September 10, 2014 05:38
Idris Vect shrinking
module Main
data ElemMV : (f : Fin (S n)) -> a -> Vect n a -> Type where
NotThereMV : ElemMV fZ x xs
HereMV : ElemMV f x xs -> ElemMV (fS f) x (x :: xs)
ThereMV : ElemMV f x xs -> ElemMV (weaken f) x (y :: xs)
elemMV : DecEq a => (x : a) -> (xs : Vect n a) -> (f ** (ElemMV f x xs))
elemMV x [] = (fZ ** NotThereMV)
elemMV x (y :: xs) with (decEq x y)
@davidpeklak
davidpeklak / KleisliCombineDep.scala
Last active August 29, 2015 14:01
KleisliCombineDep
package smt.util
import scalaz.{Monad, Bind, Kleisli}
import scalaz.syntax.Ops
import scalaz.Kleisli._
import scalaz.Scalaz._
trait KleisliCombineDep {
type Logger
@davidpeklak
davidpeklak / EitherTKleisli.scala
Last active August 29, 2015 14:01
EitherTKleisli
package smt.util
import scalaz.syntax.Ops
import scalaz._
import Kleisli._
object EitherTKleisli {
type EitherTKleisli[M[+ _], D, E, A] = EitherT[({type λ[+α] = Kleisli[M, D, α]})#λ, E, A]
@davidpeklak
davidpeklak / KleisliTest
Last active August 29, 2015 14:00
KleisliTest
package smt
import scalaz.concurrent.Future
import scalaz.Scalaz._
import org.scalatest.FunSuite
import scalaz._
class KleisliTest extends FunSuite {
lazy val s: List[Int] = List.fill(1000000)(1)
@davidpeklak
davidpeklak / WE.scala
Created March 17, 2014 21:01
EitherTWriterT
import scalaz._
object WE {
type EA[+A] = (String \/ A)
type WT[+A] = WriterT[EA, Seq[Any], A]
def replace(j: Int)(i: Int): (String \/ Int) = {
if (j > 9) -\/("Failed with " + j.toString)
@davidpeklak
davidpeklak / LazyTraverseFold.scala
Last active August 29, 2015 13:57
Lazy Traverse Fold
type M[_] is a monad
def f(as: List[A])(m: A => M[B](c0: C)(g: (C, B) => C)(implicit MM: Monad[M]): M[C] = {
def go(c: C, ras: List[A]): M[C] = ras match {
case Nil => MM.point(c)
case head :: tail => m(head).flatMap(b => go(g(c, b), tail))
}
go(c0, as)
@davidpeklak
davidpeklak / OrType.scala
Last active August 29, 2015 13:57
OrType
object Type {
class |:|[A, B]
implicit def orTypeA[A, B](implicit a: A): |:|[A, B] = new |:|[A, B]
implicit def orTypeB[A, B](implicit b: B): |:|[A, B] = new |:|[A, B]
type \:/[T, U] = {type λ[X] = (X <:< T) |:| (X <:< U)}