runarorama

// Finally tagless lambda calculus
object Final {
  def varZ[A,B](env1: A, env2: B): A = env1
  def varS[A,B,T](vp: B => T)(env1: A, env2: B): T = vp(env2)
  def b[E](bv: Boolean)(env: E): Boolean = bv
  def lam[A,E,T](e: (A, E) => T)(env: E): A => T = x => e(x, env)
  def app[A,E,T](e1: E => A => T, e2: E => A)(env: E): T = e1(env)(e2(env))

  def testf1[E,A](env: E): Boolean =
    app(lam[Boolean,E,Boolean](varZ) _, b(true))(env)

lambdageek

Sometimes I want to put an array inside of a mathpartir inferrule.

The straightforward thing doesn't work:

\begin{equation*}
\inferrule{Conclusion}{
  Premiss 1 \and
  \begin{array}{ll}
 1 & 2 \\ % note, this is where the problem happens

OlivierBlanvillain

Revisiting Tagless Final Interpreters

Tageless Final interpreters are an alternative to the traditional Algebraic Data Type (and generalized ADT) based implementation of the interpreter pattern. This document presents the Tageless Final approach with Scala, and shows how Dotty with it's recently added implicits functions makes the approach even more appealing. All examples are direct translations of their Haskell version presented in the Typed Tagless Final Interpreters: Lecture Notes (section 2).

The interpreter pattern has recently received a lot of attention in the Scala community. A lot of efforts have been invested in trying to address the biggest shortcomings of ADT/GADT based solutions: extensibility. One can first look at cats' Inject typeclass for an implementation of [Data Type à la Carte](http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesA

juanca

javascript:
document.querySelectorAll('.load-diff-button').forEach(node => node.click())

sir-wabbit

sealed trait Decidable[+Proof]
final case class Yes[Proof](proof: Proof) extends Decidable[Proof]
final case object No extends Decidable[Nothing]

sealed trait List[+A] {
  def nonEmpty: Decidable[this.type <:< ::[A]]
  def ::[AA >: A](value: AA): ::[AA] = new ::[AA](value, this)
}
final case object Nil extends List[Nothing] {
  def nonEmpty: Decidable[this.type <:< ::[Nothing]] = No

Blaisorblade

If T is a parameterized type, then isInstanceOf[T] must give an erasure warning, even if we have a ClassTag[T] in scope. Alternatively, we could ensure that ClassTag[T] does not exist for parameterized types, but only for their wildcard versions. More alternatives might be desirable, since ClassTag[T] is also used for array creation and that has different requirements.

This code (files below) demonstrates why.

The issue is that we get heap pollution and a ClassCastException without casts or erasure warnings, and that must not happen, as described by Java's guarantees for erasure warnings, which I expect should apply to us too:

https://docs.oracle.com/javase/tutorial/java/generics/nonReifiableVarargsType.html

Googling instanceof classtag unsound finds nothing, but somebody must have noticed? I expect I never did, but this issue is surprisingly easy to trigger. Apparently shapeless's Typeable takes care of avoiding the issue:

twitu

How to architect a query compiler

This paper describes the various techniques that are used to create a query compiler that converts high-level (declarative) logic into low-level optimized (imperative) logic. The paper argues that conventional methods for compiling queries i.e. template expanders have the following weaknesses -

• Everything is compiled in a single big stage which makes the logic complex and difficult to modify/expand
• Combinations cause an explosion of possible cases because each combination has to be checked with all others making it O(n^2)

The paper argues that having multiple stages that gradually lower the query through multiple DSLs each performing a specific type of transformation is a scalable and effective approach. The paper defines the two types of transformations.

• Optimizations - when the transformation occurs at the same level i.e. the construct in a DSL is expressed differently but within the same DSL.