Skip to content

Instantly share code, notes, and snippets.

View Blaisorblade's full-sized avatar

Paolo G. Giarrusso Blaisorblade

195 followers · 191 following
View GitHub Profile
@Blaisorblade
Blaisorblade / Reduced.elf
Last active August 29, 2015 14:06
I'm confused by the lifetime of variables bound by Twelf's %solve, and documentation does not seem to help.
% (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
Blaisorblade / DeriveV2.scala
Last active August 29, 2015 14:06
Trying to implement a typed tree transform ([T]Exp[T] => Exp[∆[T]]) in Scala, where ∆[_] is a type function, with some successes
// 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
Blaisorblade / TryModule.scala
Last active August 29, 2015 14:08
A customizable implementation of Try (untested)
/* 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
Blaisorblade / SMLModules.scala
Created January 18, 2015 16:16
Try encoding SML functors in Scala, v2
// 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) }
@Blaisorblade
Blaisorblade / 01.configure
Created February 4, 2015 20:29
2015-02-04 21:28:45 +0100
./configure
--disable-debug
--disable-dependency-tracking
--prefix=/usr/local/Cellar/ipmiutil/2.9.5
--enable-sha256
--enable-gpl
ipmiutil version 2.9.5
@Blaisorblade
Blaisorblade / log
Created February 8, 2015 21:54
Partial log
$ cabal build
Building pts-0.1...
Preprocessing library pts-0.1...
[24 of 36] Compiling PTS.Options ( src-lib/PTS/Options.hs, dist/build/PTS/Options.o ) [dist/build/autogen/cabal_macros.h changed]
[29 of 36] Compiling PTS.Statics.Typing ( src-lib/PTS/Statics/Typing.hs, dist/build/PTS/Statics/Typing.o ) [dist/build/autogen/cabal_macros.h changed]
[30 of 36] Compiling PTS.Statics ( src-lib/PTS/Statics.hs, dist/build/PTS/Statics.o ) [PTS.Statics.Typing changed]
[34 of 36] Compiling PTS.Interactive.Runners ( src-lib/PTS/Interactive/Runners.hs, dist/build/PTS/Interactive/Runners.o ) [PTS.Options changed]
[35 of 36] Compiling PTS.Transform ( src-lib/PTS/Transform.hs, dist/build/PTS/Transform.o ) [PTS.Options changed]
[36 of 36] Compiling PTS.Interactive ( src-lib/PTS/Interactive.hs, dist/build/PTS/Interactive.o ) [PTS.Statics.Typing changed]
[24 of 36] Compiling PTS.Options ( src-lib/PTS/Options.hs, dist/build/PTS/Options.p_o ) [dist/build/autogen/cabal_macros.h changed]
@Blaisorblade
Blaisorblade / timestamp
Created March 26, 2015 10:38
My script to generate timestamps
#!/bin/sh
[ "$1" = "-d" ] && date +"%Y-%m-%d" || date +"%Y-%m-%d-%H.%M"
@Blaisorblade
Blaisorblade / ReviewAssignment.scala
Last active August 29, 2015 14:24
// Input param: a set of IDs of participants.
val origChapters = List(6, 7, 5, 11, 8, 9, 15, 17, 24, 21, 31, 22, 27, 23, 25, 29)
val nReviewers = 2
// Output: assign nReviewers reviewer IDs to each submitter ID, so that the two reviewers and the reviewee are all different, and such that everybody does nReviewers reviews.
val chapters = origChapters.sorted
val r = new util.Random
def rndIdx() = r.nextInt(chapters.length)
case class ReviewAssignment(reviewers: List[Int], target: Int)
@Blaisorblade
Blaisorblade / caking.scala
Last active August 29, 2015 14:24
Playing with Scala cakes (?)
trait Cake
/*
trait Slice[T <: Cake] {
val cake: T
import cake._
//... implement slice using methods from cake ...
}
trait CakeSlice extends Cake with Slice[Cake with this.type] {
@Blaisorblade
Blaisorblade / gist:ea72ebc4e3a71e2cfce9
Created July 18, 2015 12:04
What I get on direct logic

Disclaimer: don't read this unless you are already interested in Carl Hewitt's direct logic.

Carl Hewitt's Direct Logic is a strange thing, if it is a thing at all. However, part of the mystery stems only from communication problems. It is hard to understand because it violates the following standard assumptions without sufficient mention or discussion --- though (some of) the violations might have a point in software engineering. However, it's still not clear whether (a) these problems can all be solved satisfactorily (b) .

  • A conventional logic has a syntax in the usual sense, so that the set of judgements is countable. Direct Logic's judgements can refer to an uncountable set of actors. Therefore, Direct Logic's judgements cannot be encoded through Gödel's natural numbers.
  • Conventionally, proof checking is decidable. It's unclear to me how Direct Logic's proof checking can be decidable; but maybe it only looks at a finite part of each actor. But if proof-checking is decidable, why can't you turn an ex