Blaisorblade

object api { class Universe { class Tree { type U = Universe.this.type; def toUTree(u: U): u.Tree = this } } }
def q(tree: api.Universe#Tree)(implicit u: tree.U): u.Tree = tree.toUTree(u)
def sameU(u: api.Universe)(t1: u.Tree, t2: u.Tree) = (t1, t2)
def sameU2(t1: api.Universe#Tree, t2: api.Universe#Tree)(implicit u: t1.U with t2.U): (u.Tree, u.Tree) = (t1.toUTree(u), t2.toUTree(u))

val (u1, u2) = (new api.Universe, new api.Universe)
val (t1, t2) = (new u1.Tree, new u2.Tree)
implicit val iu1: u1.type = u1
implicit val iu2: u2.type = u2

Blaisorblade

scalaVersion := "2.10.2"

//scalacOptions := Seq("-deprecation", "-feature", "-Xlint")

//For Scaladoc, requires SBT 0.13. However, automatic mapping does not work for the standard library - for me at least.
autoAPIMappings := true

Blaisorblade

object JMMBarriers {
  @volatile private var volatile: Int = 0
  /** Enforce a write barrier.
    *
    * Writes before this will not be reordered after this barrier, and will be
    * visible from any other thread which performs a read barrier.
    */
  def writeBarrier() { volatile = 1 }
  /** Enforce a read barrier.
    *

Blaisorblade

Having trouble installing the latest stable version of tmux?

Save yourself some time and run this little fellow!

Prerequisities

• gcc
• wget

Blaisorblade

package bugreport

object BugReport {
  /* A simple universe of types */
  sealed trait Type {
    type Eval
    type DT <: Type
  }
  
  sealed trait BaseType[BaseT] extends Type {

Blaisorblade

class A extends DelayedInit {
  def delayedInit(body: => Unit) {
    println("delayedInit START")
    body
    println("delayedInit END")
  }
  println("A's constructor!")
}
class B extends A {
  println("B's constructor!")

Blaisorblade

// http://stackoverflow.com/a/23019436/53974

trait ORD {
  type T
  def leq(a: T, b: T): Boolean
}

// The most direct attempt runs into limitations of refinements.
//def F(X : ORD) = new { def eq(x : X.T, y : X.T) = X.leq(x, y) && X.leq(y, x) }

Blaisorblade

jvm_opts='-Xms2048M -Xmx2048M -Xss1M -XX:MaxPermSize=256M -XX:+CMSClassUnloadingEnabled -XX:ReservedCodeCacheSize=64m -XX:+TieredCompilation -XX:+UseNUMA -XX:+UseParallelGC'
export ZINC_OPTS="$jvm_opts"
export ANT_OPTS="$jvm_opts -Dpartest.java_opts='-Xmx256M -Xms32M -XX:MaxPermSize=128M'"
unset jvm_opts

Blaisorblade

-- Here I relate problem with unrealizable contexts in μDOT with known problems
-- in dependent type theory. I use Agda for illustration.
--
-- I also discuss the viewpoint given by denotational semantics.

module SoundnessOpenTermsXiRule where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Bool

Blaisorblade

-- Let's try to use the result of xs++[]=xs as an equality.
-- This problem was posted by Fuuzetsu on the #agda IRC channel.

module VectorEqualityExtras (A : Set) where

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; ≡-to-≅)

open import Function