Novel usage of static type systems
刘未鹏(pongba)
然而，类型也可以用于描述一般意义上的"属性"，比如我觉得STM（软件事务内存） Haskell中一个对类型系统的运用就是神作：
Haskell中的do块能够将一组IO动作（带有副作用的语句）捆成一个块：
do {
a1
;a2
;a3
}
但a1，a2，a3的类型必须一样。一个IO动作的类型为"IO( )"。
STM Haskell是Haskell的扩展，引入了新的STM动作，类型为STM a。由于STM的特点，一个STM事务里面是不允许有IO( )动作的，因为IO( )动作可能是不可撤销的，而整个STM事务必须要求能够撤销。
Haskell的类型系统优雅的阻止了这一点：如果a1, a2都是STM动作的话，那么a3就不能是IO( )动作，因为do只分别对IO( )和STM a重载，不允许混杂。（C++里面不区分"有/无"副作用的函数，在编译器眼里所有函数都是具有副作用的）。
这个应用当中，类型的运用不再具有"一集允许的值"这样的含义，而是一个tag，代表着某种语意。
这个例子符合我认为是关于类型系统运用精髓的一句话：
"make illegal states unrepresentable"
类似的还有《C++ Template Metaprogramming》里面第三章的物理单位系统，以及Andrei很久以前写的一篇文章，利用volatile关键字（实际上是类型系统）来避免data-race。
有谁对Hakell, OCamel, F#, ML之类的语言熟悉的，还有更多这方面的例子吗？我觉得这代表类型系统的一个很有意思的应用方向——即为语言结构提供某种语意上的属性，这些属性编译器无法容易的获知，而程序员总是可以容易的获知（比如一个函数究竟是有还是没有副作用的，程序员在写一个函数的时候自然是知道的，这就类似于指定一个类的成员函数为const的一样，另一方面，一旦编译器得到了程序员的指示说"XX函数是无副作用的"，那么就可以放开手去检查程序员到底有没有（无意间）违背自己的承诺了）。当然，有无副作用的这一属性只是其一，正如那句话所说的，关键是：
make illegal states unrepresentable
--
刘未鹏(pongba)|C++的罗浮宫
http://blog.csdn.net/pongba
redsea
利用volatile关键字（实际上是类型系统）来避免data-race。
这个似乎不行吧? volatile 只是让编译器不为了优化而持续使用的已装载到 register 的变量值, 但是不配合 memory
barrier 的话, 无法避免 data-race 的啊.
最近在关心 D 语言.
D 语言准备增加 pure function 类型, 就是无副作用的纯函数. 增加的目的是
1. 更好地支持 fp
2. 为以后支持自动并发处理做铺垫.
D 里面的 typedef 是强 typedef, typedef int myint 之后, 两个类型是不匹配的.
D 里面 enum 和整数是不同的, enum 类型不能接受整数复制, 包括 0 , 但是 enum 类型可以接受 enum 常量的计算结
果.
这些都是在 c++ 的基础上对类型系统的加强了.
刘未鹏(pongba)
我简要的归纳一下他的做法：
struct X
{
void f();
};
template<typename T>
struct LockPtr
{
LockPtr(T* p) : o(p)
{
// 加锁
}
T* operator->() { return const_cast<T*>(o); }
~LockPtr()
{
// 解锁
}
private:
T* o;
};
最后使用一个约定：所有多线程共享的变量都必须声明为volatile的，这样一来：
volatile X x;
要线程不安全的调用x.f()便不可能，因为f是non-volatile的成员函数。
必须使用
LockPtr<X>(&x)->f();
或者，如果要调用多个成员函数的话：
{
LockPtr<X> locked_px(&x);
locked_px->f();
locked_px->g();
}
redsea
开销, 还会通过系统总线影响所有的 core/physical cpu , 比较昂贵.
> --
> 刘未鹏(pongba)|C++的罗浮宫http://blog.csdn.net/pongba
> TopLanguagehttp://groups.google.com/group/pongba- 隐藏被引用文字 -
>
> - 显示引用的文字 -
redsea
> > - 显示引用的文字 -- 隐藏被引用文字 -
>
> - 显示引用的文字 -
lynnboy
型定义同一性关系，多数还要定义一种弱序关系。
严格来说，具有语义的"类"，当被看作是类型时，其"值的集合"并不是传统认为的所有可能成员值的组合，而是其成员所构成的所有有效"状态"的集合。状
态之间的有效转移也构成一个状态空间上的映射，这个映射的集合定义了这个类型的语义范围。
C 中的同一性是由结构同一定义的，意味着同一的类型具有相同的值域。C++ 和多数现代语言的同一性是由指称同一性定义的，因为同样的结构不能保证同
样的状态集合和语义集合。
比如，假定符号 = 表示同一性：
int = int,
struct stat = struct stat,
struct A { int i; char c;} = struct B { int i; char c;} /* C */
class A { int i; char c;} != class B { int i; char c;} // C++
typedef 和 enum 在 C++ 中总被诟病的一个重要原因就是，它们通常被用于定义具有明确语义的类型，但却无法通过指称同一性来区别它
们。
类型系统中的弱序关系来自类型的值域范围。比如，假定符号 < 表示有序：
int < long, float < double, class Derived* < class Base*
这种弱序关系在 C++ 中明显地表示为隐式转换关系。
上述说法并不严格，比如根据Liskov可替换性原则的子类型定义，子类型应该完全保持父类型的语义，而实际上子类型总会具有某些不同之处。另
外，Derived < Base 其实并不意味着 Derived 整个状态空间的值域属于 Base 的状态空间，而是指其中的 Base 部分的
子空间；这其实也是 Liskov原则的另一个说法。
类型cv限定符同样定义了类型弱序关系。加上CV限定符并不会缩减类型的状态集合，但可以缩减状态空间中的状态转换集合
现代多数类型系统中的类型不仅代表"值的集合"，更代表带有语义的"状态空间"，类型就带有语义约束能力了。Andrei 的方法其实就是这种语义约束
能力的一个应用而已，其本质上与用不同的类来区别语义没有太大不同。
On 8月31日, 上午10时47分, "刘未鹏(pongba)" <pon...@gmail.com> wrote:
> 类型的一般定义是"值的集合"，比如int类型允许的值集是所有的整数。字符串类型则是所有的字符串。char类型则是字符集，一般来说不同值集之间的赋值是不允许的也是不该被进行的，类型系统的主要作用就是在编译期禁止这一操作。
>
> 然而，类型也可以用于描述一般意义上的"属性"，比如我觉得STM（软件事务内存） Haskell中一个对类型系统的运用就是神作：
>
> Haskell中的do块能够将一组IO动作（带有副作用的语句）捆成一个块：
>
> do {
> a1
> ;a2
> ;a3
>
> }
>
> 但a1，a2，a3的类型必须一样。一个IO动作的类型为"IO( )"。
>
> STM Haskell是Haskell的扩展，引入了新的STM动作，类型为STM a。由于STM的特点，一个STM事务里面是不允许有IO(
> )动作的，因为IO( )动作可能是不可撤销的，而整个STM事务必须要求能够撤销。
>
> Haskell的类型系统优雅的阻止了这一点：如果a1, a2都是STM动作的话，那么a3就不能是IO( )动作，因为do只分别对IO( )和STM
> a重载，不允许混杂。（C++里面不区分"有/无"副作用的函数，在编译器眼里所有函数都是具有副作用的）。
>
> 这个应用当中，类型的运用不再具有"一集允许的值"这样的含义，而是一个tag，代表着某种语意。
>
> 这个例子符合我认为是关于类型系统运用精髓的一句话：
>
> *"make illegal states unrepresentable"
>
> *类似的还有《C++ Template
> Metaprogramming》里面第三章<http://blog.csdn.net/pongba/archive/2004/09/01/90642.aspx>
> 的物理单位系统，以及Andrei很久以前写的一篇文章 <http://www.ddj.com/cpp/184403766>
> ，利用volatile关键字（实际上是类型系统）来避免data-race。
>
> 有谁对Hakell, OCamel, F#,
> ML之类的语言熟悉的，还有更多这方面的例子吗？我觉得这代表类型系统的一个很有意思的应用方向--即为语言结构提供某种语意上的属性，这些属性编译器无法容易的获知，而程序员总是可以容易的获知（比如一个函数究竟是有还是没有副作用的，程序员在写一个函数的时候自然是知道的，这就类似于指定一个类的成员函数为const的一样，另一方面，一旦编译器得到了程序员的指示说"XX函数是无副作用的"，那么就可以放开手去检查程序员到底有没有（无意间）违背自己的承诺了）。当然，有无副作用的这一属性只是其一，正如那句话所说的，关键是：
>
> *make illegal states unrepresentable
>
> *--
> 刘未鹏(pongba)|C++的罗浮宫http://blog.csdn.net/pongba
刘未鹏(pongba)
lynnboy能否给出更多类似这类例子？即广义的类型系统应用？我个人感觉这才是类型系统真正的潜力所在。
楠公小白（lynnboy）
类型系统最初能够出现，盖因人们无法记住机器表示中的每个字节的目的和用法。比如给 C 加上浮点表示能力的 float 类型出现后就可以让人们不用
记住那个变量其实不是整数。这种"簿记"信息从人的大脑中解放出来，就是类型系统的责任。类型用于记住一个东西是什么（或者可被当作什么）。到现在为
止，无论是编译时有效的静态类型系统，还是虚拟机支撑的运行时类型系统，甚至是经常被称为（没有类型系统）的动态类型系统，其实都要完整这个根本任
务。
类型系统的发展就是不断把需要由人工记住的附加信息变为可以由机器（编译器、虚拟机等）维护的过程。从低级语言向高级语言过渡的过程中人们把数据的表示
和解释方式放在类型中；结构化运动中人们发展出抽象数据类型，把适用于一个特定抽象数据结构的语义的集合交给类型来维护；随即是面向对象革命，又抽象出
了"接口"这个概念，并自然同类型联系起来；再然后就是参数化类型，使我们不必为每种可能性写实现代码；而对参数化类型的参数进行类型检查，只不过是这
个进程的自然推论。
指令式语言有这样的演进过程，而另一方面函数式语言和动态语言也同样经历了类似的类型系统扩张过程。这其中的道理其实只有一个：让机器用一种结构化的方
式记住更多的东西，增加更多抽象层次，[有效降低系统复杂度]，解放我们的大脑。
这个过程的另一个方面，就是随着语言不断演化和创新，如今指令式语言越来越多地增加函数式语言原来独有的能力，而这些能力一部分可能依赖于越来越动态化
的语言运行时，而其最重要的基础原因却是由类型系统增加的更多抽象层次所导致的更高级概念的表达能力不断出现。比如 C++ function<>,
lambda<>, 这样的东西，就源自模板系统在使用点实例化新实体的能力，而这在 C 甚或早期的 C++ 等语言所无法想象的。又如 C#
3.0 新加入的许多函数式特性，大多数都依赖于 C# 语言本身类型系统的丰富的抽象层次。
Andrei 的例子是很好，很优雅，其中的本质是对成员函数的 this 指针的 volatile 限定导致了其作为左值类型的状态空间无法匹配，
简单来说就是对所有以 X 的左值为参数的行为都无法应用到 volatile X 上。但这中间很明显有个毛病，就是 X 不能有任何以右值为参数的
行为。比如基础类型就有一大堆运算符，又如 std::string，它经常是按值传递的。
这个毛病的原因是 volatile 只能把类型状态空间的一半封闭掉。而要封闭整个状态空间，只能用个包装类实现：
template<class T> struct SharedRes {
SharedRes() : o(T()) { }
SharedRes(T& v) : o(v) { }
unique_ptr<T, type_of_unlock> Get() { lock(); return unique_ptr<T,
type_of_unlock>(&o, unlock); }
private:
T& o;
};
SharedRes<X> x;
SharedRes<std::string> sharedStr;
void f(std::string str){...}
void g(){
f(sharedStr);// failure
x.f();//failure
x.Get()->f();//OK
f(*sharedStr.Get());//OK
}
当然，我也不是说 Andrei 的方法不好，其实这个方法许多人都"发现"过，而且只要遵守恰当的设计原则（比如从不用右值操作资源），还是很不错
的。
我对类型系统的想法是：下一步还可以把什么放入其中，获得什么抽象能力，怎样控制系统复杂性呢？
我觉得对于控制系统复杂性来说，AOP 的"关注点分离"概念应当是当前最重要，也可能是最本质的理论方向。而要实现关注点分离能力，就要明白用什么来
建模关注点。在我看来，所谓关注点仍然是分立的语义元素。AOP 的"方面"（Aspect），就是这个语义元素的表述。方面编织（Weaving）能
力，就是语义组合能力，也就是把某个分立的语义插入到系统各个部分中去。AOP 的编成能力，体现在其能够对语义本身进行编程控制的能力。
类型系统本身的发展方向应该就是这种语义级别的抽象。拿 AOP 来说，流行的 AOP 语言给类型系统中加入了 aspect 等元素，它们就是用于
对可编织的语义进行直接建模。
C++ 类型系统新加进了 concept，这个东西本身并不能带来很多新东西，因为它只是对静态接口的绑定，进一步保护语义同实现的一致性，增加类型
安全性而已。然而还有个 concept_map 存在。它的出现虽然本来用于进行静态接口的适配，但同时却意味着把语义从类型中剥离出来的能力。有
了 concept_map，concept 不再只是静态接口，而同时更加可以是对语义的抽象。语义剥离能力，再加上 C++ 类型系统固有的元编程
能力，分明意味着静态 AOP 能力的出现为期不远。
On 9月5日, 下午11时34分, "刘未鹏(pongba)" <pon...@gmail.com> wrote:
> 感谢lynnboy的指教:-)
> lynnboy能否给出更多类似这类例子？即广义的类型系统应用？我个人感觉这才是类型系统真正的潜力所在。
>
pierric
illegal states unrepresentable" 确实点出了精髓所在。
除了STM外，各类Monad应该都是很好的例子，一个do block当中不能随意的混合它们，因为do block本身只是syntax
sugar，最终被转换为bind函数的组合，bind的类型决定了任何试图混合使用的行为都是非法的。如果希望同时获得某些monad们的功能，那么
只能通过monad transformer来做到，monad transformer本身也借助类型系统来保证代码是正确的。
前段时间有看到一个叫House的操作系统项目，在概要里面提到他们构造了一个hardware monad，以保证系统底层级别的动作的合理。此外文
章中还有提到一个叫Oskar的项目──一个微内核操作系统──目的在于借助类型系统，来获得一些key security properties.
库Parserc中，构造了parser monad，生成一系列combinator，这也是Monad最值得称道的一个应用。
还有quickCheck库中，大量运用了type class，自动产生随机数据对任意函数进行测试。
除了举了上面这些例子以外，我还想说说一些个人对haskell的感受。事实上，我觉的haskell和C++挺像的，这里指c++中的范型编程。只是
haskell更加精巧直接的多，而gp更像是一个庞然大物。譬如concept完全就是type class的等价物，haskell中同样也有很多
meta programming的技巧。不过貌似haskell打一开始就要求编程者站在范型的角度来看待所有的东西。
On Aug 31, 10:47 am, "刘未鹏(pongba)" <pon...@gmail.com> wrote:
> 类型的一般定义是"值的集合"，比如int类型允许的值集是所有的整数。字符串类型则是所有的字符串。char类型则是字符集，一般来说不同值集之间的赋值是不允许的也是不该被进行的，类型系统的主要作用就是在编译期禁止这一操作。
>
> 然而，类型也可以用于描述一般意义上的"属性"，比如我觉得STM（软件事务内存） Haskell中一个对类型系统的运用就是神作：
>
> Haskell中的do块能够将一组IO动作（带有副作用的语句）捆成一个块：
>
> do {
> a1
> ;a2
> ;a3
>
> }
>
> 但a1，a2，a3的类型必须一样。一个IO动作的类型为"IO( )"。
>
> STM Haskell是Haskell的扩展，引入了新的STM动作，类型为STM a。由于STM的特点，一个STM事务里面是不允许有IO(
> )动作的，因为IO( )动作可能是不可撤销的，而整个STM事务必须要求能够撤销。
>
> Haskell的类型系统优雅的阻止了这一点：如果a1, a2都是STM动作的话，那么a3就不能是IO( )动作，因为do只分别对IO( )和STM
> a重载，不允许混杂。（C++里面不区分"有/无"副作用的函数，在编译器眼里所有函数都是具有副作用的）。
>
> 这个应用当中，类型的运用不再具有"一集允许的值"这样的含义，而是一个tag，代表着某种语意。
>
> 这个例子符合我认为是关于类型系统运用精髓的一句话：
>
> *"make illegal states unrepresentable"
>
> *类似的还有《C++ Template
> Metaprogramming》里面第三章<http://blog.csdn.net/pongba/archive/2004/09/01/90642.aspx>
> 的物理单位系统，以及Andrei很久以前写的一篇文章 <http://www.ddj.com/cpp/184403766>
> ，利用volatile关键字（实际上是类型系统）来避免data-race。
>
> 有谁对Hakell, OCamel, F#,