序
函数式编程语言有很多种定义,宽泛的认为支持高阶函数(higher-order function)就算函数式语言的话,大多数现代语言都是支持函数式编程的,例如C/C++,java,C#,lua,python,JavaScript,Scala等等。收紧一下定义的话,加入函数式语言要求的模式匹配、无副作用等要求,那么剩下的就是纯函数式语言,比较常见的有Haskell,Clean等。
副作用是什么和为什么有些语言想在设计上避免副作用这个问题,google能搜出好多博文,这里就不多说了。避免副作用可以带来一些实际的好处,比如帮你大量改写代码什么的(误),而且连gcc都有 _ _ attribute _ _((pure/const))的函数扩展嘛~。比如像erlang这种依赖于副作用编程的语言,虽然有着变量不可变这个特性,但是仍然可以读写process携带的全局变量,而且又没有一个好的类型系统,所以在编译的时候也不会怎么大改你的代码,大多还是直译成字节码。
注:这篇文章不是**软文**,不会用个g(f(x))就当例子给大家说无副作用多么多么好,可缓存结果拉(just a lie)~原生支持并行拉(just another lie),这些都是扯淡而且不实际的。(有机会再写个博客专门谈谈这个)
正文
首先,纯函数式的语言强调没有副作用,它不会改变任何实际的东西,当然也没有(全局的)状态,这样的程序如果不配上代表副作用的输入输出当然是什么都干不了的。那么如何把副作用嵌入到本不该有副作用的语言设计中那?当然不能直接赋值,不然。。不然。。就变成命令式语言了,而且函数式语言编译中引以为豪的各种优化pass几乎都不能用了。那么把有副作用的函数标注出来?当然是一个办法。还有就是把副作用的表达式都包含在context中,随着函数传递,保证顺序而且要保证引用的唯一性。
作为纯函数式语言的代表,Haskell和Clean对于副作用的设计实现上差别很大,下面就简单说一下它们的实现,刨根究底,其实它们做的还是同一件事情。
haskell
Haskell中有一个很重要的概念:Monad,取名自范畴论,可以粗浅的认为它就是定义了一系列的行为准则(>>= , return)。Haskell中大多数语法糖都是为了这个发明来的。Haskell的标准库中有很多关于副作用的类库封装,比如IORef,MVar,IOMonad等等,他们的内部实现都会归结到ST Monad(State Thread Monad)上,正是这个与forall关键字的结合,从而在语法上保证了副作用嵌入在(纯)Haskell中的正确性。
ST Monad里面主要的定义是:
newtype ST s a = ST (STRep s a)
type STRep s a = State# s -> (# State# s, a #)
data STRef s a = STRef (MutVar# s a)
runST :: (forall s. ST s a) -> a
runSTRep :: (forall s. STRep s a) -> a
其中最关键的是ST s a 与 STref s a 这两个数据结构。
先看看这个用法,let a0 = runST $ newSTRef 0
,会引发一个type error。因为runST的类型是(forall s.ST s a) -> a
,参数(newSTRef 0)
的类型是forall s. ST s (STRef s Int)
,最后求值后的结果是a0::STRef s Int
,显然s脱离了原本的定义域(也就是那层forall之外,forall是Haskell中提供**RankNType**的关键字)。从而用户就只能使用下面的方式:
sumST :: Num a => [a] -> a
sumST xs = runST $ do
n <- newSTRef 0
forM_ xs $ \x -> do
modifySTRef n (+x)
readSTRef n
不用标出标出具体实现,大家就能看出他做的事情就是做了一层wrapper,在type checker上保证被box之后不会被用户取出来乱改。至于如何做到destructive in-place update,这就属于编译器的黑魔法了,语言这层只需保证语义就好。(**注:**ghc的实现中,ST Monad标准库用到了ghc的unsafe打头的内置函数)
Clean
Clean语言用的策略是线性类型系统(linear type system),是Substructural type sysytem的一种。在Curry-Howard同构中对应Substructrual logic。这类类型系统中,不但可以决定一个变量是什么类型,还可以约束被使用的次数与顺序。在Mozilla出的Rust语言中,也可以看到线性类型的影子。
先举个栗子~
transform :: (Int -> Int) *{#Int} -> *{#Int}
transform f s
| size s == 0 = s
| otherwise = if (s.[0] == 0)
{f i \\ i <-: s}
{f i \\ _ <-: s & i <- [s.[0]..]}
(不要在意奇怪的语法,{}里面其实就是list comprehension)
其中*就是uniqueness type的标注,这个函数的类型用haskell写出来就是transform :: (Int -> Int) -> *[Int] -> *[Int]
。这个函数虽然没有很好的看出uniqueness type的特性和传播性,但是作为简单的例子,差不多就是这么回事。
对于uniqueness type最直观的理解就是带有这个标识的类型是不能参与到以后Graph Reduction中,而且会检测会不会有多个“变量”指向他。上面这个函数中就不会存在多个[Int]及相关的副本等着被回收,而是会直接在(ReadWorld中的)内存上更新数据。
最后
其实已经看出,在上面Haskell与Clean的做法中,一个是利用forall关键字与ST Monad+编译器黑魔法,另一个是build-in在类型系统中,但是本质都是做了一件事情,就是保证RealWorld中的对象不会存在多个引用,而且在Graph Reduction中不会被编译器搞乱顺序,这样就能融入到整个纯函数式的大体系中了。
posted on 2014-07-10 15:16
右席 阅读(4427)
评论(1) 编辑 收藏 引用 所属分类:
搬砖之路