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

Blaisorblade

% (Possible) bug report or confusing behavior.

% The code is in three parts, Part 1 is boring and 3 are boring, the interaction
% between 2 and 3 is confusing. How long is the result of a %solve directive
% supposed to persist?

% I have an Agda background and I've read some papers on Twelf.

% I've seen this bug in Emacs, but I imagine this only requires keeping the
% Twelf server alive throughout.

Blaisorblade

// Also at https://gist.github.com/Blaisorblade/1622b0809effb9a56061
package ilc

/**
 * Incremental lambda calculus - an attempt at a *typed* Scala implementation.
 * Should you want more details on the particular transform, see http://inc-lc.github.io/ and our
 * PLDI paper at http://www.informatik.uni-marburg.de/~pgiarrusso/papers/pldi14-ilc-author-final.pdf
 * — the transform is in Fig. 4(g).
 *
 * However, I **quickly** wrote a minimal introduction here so that you can make sense of the code.

Blaisorblade

/* Based on code from the Scala standard library, hence covered by the Scala license. See https://github.com/scala/scala/blob/2.11.x/doc/LICENSE.md
 * Copyright (c) 2002-2013 EPFL
 * Copyright (c) 2011-2013 Typesafe, Inc.
 */

import scala.collection.Seq
import scala.util.control.NonFatal
import scala.language.implicitConversions

/*

Blaisorblade

// A variant of https://gist.github.com/Blaisorblade/19ef1abb28e20995e187, answering
// 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) }