amutake

Set Implicit Arguments.
Unset Strict Implicit.

(** Type Definitions *)

Inductive IndexedContsT (W M : Type -> Type) (R O A : Type) : Type :=
| mkIndexedContsT : (W (A -> M O) -> M R) -> IndexedContsT W M R O A.

Definition runIndexedContsT W M R O A (c : IndexedContsT W M R O A) : W (A -> M O) -> M R :=
  match c with

Blaisorblade

{- I suggested that higher-order pattern unification (as in Agda) might be a viable improvement over Haskell-style unification
for higher-kinded types.

This snippet demonstrates it is not. To this end, I tried to encode something similar similar to this snippet

```
def f[F[_], A](fa: F[A]) = ???
f[type lambda here, ...](Good("winning"): String Or Int)
```
That's taken 

djspiewak

Explaining Miles's Magic

Miles Sabin recently opened a pull request fixing the infamous SI-2712. First off, this is remarkable and, if merged, will make everyone's life enormously easier. This is a bug that a lot of people hit often without even realizing it, and they just assume that either they did something wrong or the compiler is broken in some weird way. It is especially common for users of scalaz or cats.

But that's not what I wanted to write about. What I want to write about is the exact semantics of Miles's fix, because it does impose some very specific assumptions about the way that type constructors work, and understanding those assumptions is the key to getting the most of it his fix.

For starters, here is the sort of thing that SI-2712 affects:

def foo[F[_], A](fa: F[A]): String = fa.toString

JoshRosen

Serialization of Scala closures that contain local defs

Several Apache Spark APIs rely on the ability to serialize Scala closures. Closures may reference non-Serializable objects, preventing them from being serialized. In some cases (SI-1419 and others), however, these references are unnecessary and can be nulled out, allowing otherwise-unserializable closures to be serialized (in Spark, this nulling is performed by the ClosureCleaner).

Scala 2.12's use of Java 8 lambdas for implementing closures appears to have broken our ability to serialize closures which contain local defs. If we cannot resolve this problem, Spark will be unable to support Scala 2.12 and will be stuck on 2.10 and 2.11 forever.

As an example which illustrates this problem, the following closure has a nested localDef and is defined inside of a non-serializable class:

``

travisbrown

import cats.{ Applicative, Traverse }
import cats.std.list._
import java.util.concurrent.TimeUnit
import org.openjdk.jmh.annotations._

trait DefaultApApplicative[F[_]] extends Applicative[F] {
  def ap[A, B](ff: F[A => B])(fa: F[A]): F[B] = map(product(ff, fa)) {
    case (f, a) => f(a)
  }
}

gkossakowski

Scala's "type T in class C as seen from a prefix type S" with examples

Introduction

Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples together with explanation how specific set of rules (grouped thematically) is applied. These notes helped me gain confidence that I fully understand Scala's core typechecking algorithm.

As Seen From

Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier reference:

puffnfresh

sealed trait Caster[A, B]
case object CastTo extends Caster[Unit, Unit]
case class Ignored[A, B]() extends Caster[A, B]

def cast[A, B]: A =:= B =
  (Ignored(): Caster[A, B]) match {
    case CastTo | _ => implicitly[B =:= Unit]
  }

cast[String, Int]: String =:= Int

ekmett

{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}

lyricallogical

import scala.language.higherKinds

sealed trait Base[F[_]] { // all compilation is succeeded if F' kind is *
  def a: String
}
case class Ctor[F[_]](a: String) extends Base[F]
abstract class Etor[F[_]] extends Base[F] {
  def f(q: Base[F]): String = q match {
    case Ctor(fa) => fa // NP
    case Etor(fa) => fa // error! why???

ekmett

{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}