scala类型系统:柯里-霍华德同构

通过柯里-霍华德同构实现联合类型

在这个系列之前的这篇blog scala类型系统:10) 交集类型与联合类型 里曾提到过实现union类型的另一种方式是柯里-霍华德同构

这段代码是从这里看到的:

type ¬[A] = A => Nothing
type ∨[T, U] = ¬[¬[T] with ¬[U]]
type ¬¬[A] = ¬[¬[A]]
type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }

def size[T : (Int |∨| String)#λ](t : T) = t match {
    case i : Int => i
    case s : String => s.length
}

scala> size(3)
res0: Int = 3

scala> size("three")
res1: Int = 5

要理解这段类型证明,先要了解复合类型,结构类型,函数类型的逆变,类型投影,以及type-lambda等,这些点可以从之前的blog里参考。

对于普通的class来说,A with B复合类型是类型AB的子类型:

scala> import scala.reflect.runtime.universe._

scala> class A; class B;

scala> typeOf[A with B] <:< typeOf[A]
res0: Boolean = true

但对于函数类型,因为其参数类型是逆变的,所以情况正好反过来:

scala> typeOf[ A=>Nothing ] <:< typeOf[ (A with B)=>Nothing ]
res1: Boolean = true

用图来看:

 __________               _________________________ 
|          |             |                         |
|     A    |             |  (A with B) => Nothing  |
|__________|             |_________________________|
      ^                               ^ 
      |                               | 
 __________               _________________________ 
|          |             |                         |
| A with B |             |        A => Nothing     |
|__________|             |_________________________|  

所以,我们把上文中定义的:¬[¬[A]]¬[¬[T] with ¬[U]] 两个表达式展开的话,会发现这两个函数类型是有继承关系的(如果参数类型A与T或U相同的话):

//¬[¬[A]]
scala> type T1 = (A=>Nothing) => Nothing  

//¬[¬[T] with ¬[U]]
scala> type T2 = ((A=>Nothing) with (B=>Nothing)) => Nothing  

scala> typeOf[T1] <:< typeOf[T2]
res3: Boolean = true

然后定义了一个结构类型:

type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }

这个结构类型里的λ是一个类型工厂,当传入给它某个类型参数时,它会构造出一个新的类型 ¬¬[X] <:< (T ∨ U) ,这个是中缀写法,还原成普通类型写法是: <:<[¬¬[X], (T ∨ U)] 关于 <:< 这个类型是用于约束两个类型关系的,它是在Predef里定义的:

sealed abstract class <:<[-From, +To] extends (From => To) with Serializable

它要求 ¬¬[X] 是类型 T v U (即v[T,U])的子类型。

而这个要求,我们前边证明 ¬[¬[X]]¬[¬[T] with ¬[U]] 的关系时已经论证过了,当类型参数X与T或U一致时即:

// 只有当
X =:= T //或 
X =:= U 

//下面的约束才成立
¬¬[X] <:< (T ∨ U) 

那么现在来单独用λ这个类型构造器,它的表达方式为 (T |v| U)#λ,这是一段type-lambda,它描述的是一个构造器类型,它可以由类型参数X,构造出一个复杂的约束类型:

<:<[(X=>Nothing)=>Nothing, ((T=>Nothing) with (U=>Nothing))=>Nothing]

这个约束类型能够编译通过的前提如前边所说,需要X等于TU才行。

现在我们把用一个具体的,由IntString类型参数构造的 |∨|[Int, String] 类型中的λ类型构造器用Factory来表示:

type Factory[T] = (Int |∨| String)#λ[T]

这个Factory类型构造器,对于任何类型参数 T,构造出的类型展开后为:

<:<[(T=>Nothing)=>Nothing, ((Int=>Nothing) with (String=>Nothing))=>Nothing]

也就是说T必须是IntString才能满足。最后用隐式参数的方式(context bound)在方法定时时描述这种约束

def size[T: Factory](p: T) = ...

相当于:

def size[T](p: T)(implicit ev: Factory[T]) ...

如果你纳闷这个ev隐式参数是哪里来的,参考一下以前的这篇: scala类型系统:22) 类型约束与特定方法

整个过程只涉及到类型证明,与以前的实现方式对比不需要显式提供任何隐式转换或隐式参数(只用到了语言默认提供的一个隐式参数),也没有创建任何“单例”或“实例对象”,柯里-霍华德同构可以简单理解为类型证明(type-lambda)即程序。

scala类型系统:类型推导

类型推导是一门博大的学问,背后有繁冗的理论,好在非编译器开发者不用太多了解,我看到这方面的文章时立刻就知难而退了。这里蜻蜓点水的带过。

Scala采用的局部的(local)、基于流的(flow-based)类型推断;而非像ML,Haskell等语言采用的更加全局化的Hindley-Milner类型推断方式。

在《Programming in Scala》一书中提到基于流的类型推断有它的局限性,但是对于面向对象的分支类型处理比Hindley-Mlner更加优雅。

基于流的类型推导在偏应用函数场景下,不能对参数类型省略,正体现了它的局限性。下面的偏应用函数声明,在Hindley-Milner类型推导(基于全局的)可以正常的推导的,会在scala里报错:

scala> def foo(a:Int, b:String) = a+b

scala> val f = foo(200, _)
<console>:8: error: missing parameter type for expanded function ((x$1) => foo(200, x$1))
   val f = foo(200, _)
                    ^

上面第二个参数占位符缺乏类型。需要显式的声明变量f的类型

scala> val f: String=>String = foo(200, _)
f: String => String = <function1>

或者显式的声明占位符参数类型

scala> val f = foo(200, _:String)
f: String => String = <function1>

不过这里有一个细节是eta-expansion的情况下可以省略参数类型,比如:

scala> def foo(a:Int, b:String) = a+b

scala> val f = foo _
f: (Int, String) => String = <function2>

scala> val f = foo(_,_)
f: (Int, String) => String = <function2>

上面两种写法占位符都是对全部参数,foo _foo(_,_) 在编译过程会编译器会进行eta-expansioneta扩展会把这个表达式转换为与foo方法类型一致的函数对象。这是在规范里定义的。

而最开始的写法 foo(200, _)并不是eta-expansion(原因见之前的这篇)。这种情况下类型推导并不会从方法体的上下文去推断参数的类型。所以需要显式的声明参数类型。

另外,对于泛型方法的情况,类型推导也需要注意泛型参数,参考这篇

java可以创建多少个线程

记得以前在jvm的群里讨论过,与系统环境设置有关,我在mac os上试验的。

% sysctl kern.num_taskthreads  
kern.num_taskthreads: 2048

用repl来模拟一下,在启动repl后线程大概有20个左右,现在看看还可以启动多少个线程:

scala> import java.util.concurrent.atomic.AtomicInteger

scala> val n = new AtomicInteger(0)

scala> val run = new Runnable(){
        override def run() { n.incrementAndGet ;Thread.sleep(1000000) }}

scala> try{ while(true){ val t = new Thread(run); t.start } } catch{
            case e:Throwable => println("count: " + n.get) 
        }
count: 2025

运行过程中jvm可能还有其他线程也会启动,总的线程数加起来正好2048(或者接近).

如果系统参数设置一个很大的值,那java可创建的线程数就只与内存相关了。

如果指定的-Xss越大,java进程在non-heap区域为每个线程分配的初始也越大。栈空间分配的初始值通常比Xss设定的要小,VM并不会一上来就分配与之对等的内存。

另外一点有趣的是,如果你分配给jvm的堆空间(heap size)太大,系统中如果没有足够多的剩余空间的话,non-heap可分配的就越小,可创建的线程数也反而少了。也就是说heap与non-heap是竞争关系。参考这里

scala类型系统:case class与代数数据类型

ADT(algebraic data type) 是很多函数式编程语言中支持的一种类型。不清楚最初是否来自haskell。

《Programming in Scala》中文版,在术语表中有提到ADT:

通过提供若干个含有独立构造器的备选项(alternative)来定义的类型。通常可以辅助于通过模式匹配解构类型的方式。这个概念可以在规约语言和函数式语言中发现。代数数据类型在Scala中可以用样本类(case class)模拟。

参考wiki:http://en.wikipedia.org/wiki/Algebraic_data_type

在计算机编程、特别是函数式编程与类型理论中,代数数据类型(ADT)是一种组合类型(composite type).例如,一个类型由其它类型组合而成。两个常见的代数类型是product(乘积)类型(比如tuplesrecords)和sum类型,它也被称为”tagged unions”或”variant type”

ADT最大的价值是用于“模式匹配”,即解构一个对象。

我们看看Scala怎么用case class模拟ADT,比如一副扑克按花色来分类:

sealed abstract class Suit
case class Heart(value: Int) extends Suit
case class Diamond(value: Int) extends Suit
case class Spade(value: Int) extends Suit
case class Club(value: Int) extends Suit

当然case class的构造参数并没有限制,比如下面这个描述一棵树的节点和叶子:

sealed abstract class Tree
case class Node(left: Tree, right: Tree) extends Tree
case class Leaf[A](value: A) extends Tree
case object EmptyLeaf extends Tree

关于case class更多细节请参考模式匹配系列blog。