note on haskell

Comments

haskell基础语法

基础定义

都是函数的定义，并不复杂。

1
2
add :: a -> b -> c
add x y = x + y

$\lambda$ 表达式

1
2
add :: a -> b -> c
add = \x -> \y -> x + y

type（可以理解成define）

1
type Cont = [Op]

data（使程序更高效运行，但会占内存）

1
data Maybe a = Nothing | Just a

Class

1
2
3
class Eq a where
	(==) :: a -> a -> Bool
	(/=) :: a -> a -> Bool

instance

1
2
3
4
instance Eq Bool where 
	False == False = True
	True == True = True
	_ == _ = False

list comprehension

1
2
3
4
5
6
primes :: Int -> [Int]
primes n = [x | x <- [2..n], prime x]

positions :: Eq a => a -> [a] -> [Int]
positions x xs =
	[i | (x’,i) <- zip xs [0..], x == x’]

简单应用

1
2
3
4
5
6
7
qsort :: Ord a => [a] -> [a]
qsort [] = []
qsort (x:xs) =
	qsort smaller ++ [x] ++ qsort larger
	where
		smaller = [a | a <- xs, a <= x]
		larger = [b | b <- xs, b > x]

Monads and More

首先要知道我们需要解决一个怎么样的问题

前面的函数看起来都很棒，很有趣。

我们可以让只有真正调用函数的时候才会把值传进去算一遍，不然只是单纯地函数的复合。

那么对于一个 $f:A\to B,g:B\to C$，可以简单地进行 $g \circ f$ ，那么在最后调用 $x\in A$ 的时候，我们直接通过复合函数得到 $y\in C$

在某些情况下，我们需要对类型都进行一个 $\rm M$ 的包装，比如 Maybe Int。那么在 $\rm M \ a$ 相关映射里，我们考虑如下几种

上述映射是确实存在的，一个简单的例子就是：

1
2
3
safeDiv :: Int -> Int -> Maybe Int
	safeDiv _ 0 = Nothing
	safeDiv x y = Just (x / y)

考虑上述四种变换，要应用到 $\rm M\ A$ 中，第二种和第四种是能利用函数复合实现的，但我们还需要实现第一种和第三种。

四种操作实际上是不需要的，在实际操作中，一旦加入了 $\rm M$ 后续不会再打开了。

读者可以利用 IO ，Maybe 作一个简单的类比。

一旦成为 Maybe Int ，是可能并不能打开成为 Int 的，因为 Nothing 无法得到打开。

作为 IO () ，我们可以简单地理解成它把副作用通过增加了一个包装给全扔到里面了。

M 一般用来处理副作用，相当于把副作用封住成一个包，也可以是为了增加类型的一些性质，比如 state 。

functor

functor，实现了fmap，既可以把对象映射成对象，又可以把态射映射到态射。

1
fmap :: (a -> b) -> F a -> F b

显然，通过 fmap 我们可以实现调用fmap func 从而将 func 从 $a \to b$ 变成 $F\ a \to F\ b$。

这时候，我们就可以用函数的复合来实现第一种了。

首先我们有一个 x = M A ，有一个函数 f :: A -> B ，有一个函数 g :: B -> C

那么作用上 f 相当于 fmap f x ，也即通过了 fmap f 这样一个函数的作用。再作用上 g 相当于 fmap g fmap f x ，也就是利用了 fmap g fmap f 的作用。

借鉴上面的思路，我们考虑如果实现了下面的函数

1
myfunc :: (a -> M b) -> M a -> M b

再结合函数的复合，我们是不是就实现了第三种操作？非常棒！

Applicative

上面的 fmap g fmap f 看上去很完美，但是却又一个缺陷，如果我们的 g 并不是给定的，而是根据 f 算出来的，那么我们应该如果实现类似 fmap g fmap f 的操作。

也许我们可以定义如下的函数

1
fmap3 :: (a -> (b -> c)) -> (F a -> (F b -> F c))

但其实我们可以实现得更简洁，我们实现如下两个函数

1
2
pure :: a -> F a
<*> :: F (a -> b) -> F a -> F b

很好，我们考虑之前的 fmap3

首先 (a -> b -> c) -> F (a -> b -> c)

然后 F(a -> b -> c) -> F(a) -> F(b -> c)

然后 f(b -> c) -> F b -> F c

如此，我们可以解决之前纯粹 functor 的缺陷。简单来说，它可以将映射的对象 F (a->b) 变成 F a -> F b ，从一个对象转换成一个映射。

Monad

为了解决类似上面的问题，我们需要把 myfunc 修改成复合我们的需求。

方便起见，不妨假设所有的函数都形如 a -> M b 。

一个简单的例子是

a -> M (b -> M c)

这时候用 Applicative 会出现什么问题？

a -> M (b -> M c) -> M (a -> M (b -> M c)) -> (M a -> M(b -> M c)) -> (M a -> M b -> M M c)

唉，有一个M M C 这不行，不符合我们的预期，我们希望它出来的是 M c 而不是 M M c 。如果有一个自然变换把 M M c 映射到 M c 就好了。也就是需要一个单函子上的幺半群满足这个要求。

我们是不是把 myfunc 改一改就行了？大概是的。

我们不妨来看看 Monad 是怎么实现我们的需求的

Monad 实现了 bind >>=

1
2
return :: a -> M a
(>>=) :: M a -> (a -> M b) -> M b

如果f :: a -> M (b -> M c)

注意这里我们是先有了 a 然后才有 b -> M c 所以 a 应该放在前面。

M a -> (a -> M(b -> M c)) -> M(b -> M c)

M b -> M (b -> M c) -> M c

非常完美地解决了这个问题。事实上这就是 myfunc 的一个简单变形。

举个例子，下面的冗余的写法

1
2
3
4
5
6
7
case safeDiv a b of
  Nothing -> Nothing
  Just x  -> case safeDiv c x of
    Nothing -> Nothing
    Just y  -> case safeDiv d y of
      Nothing -> Nothing
      Just z  -> safeDiv e z

就可以方便地写作

1
2
3
4
safeDiv a b >>= (\x ->
safeDiv c x >>= (\y ->
safeDiv d y >>= (\z ->
  safeDiv e z)))

而且类型出来的就是 Maybe Int ！

haskell对此设置了语法糖

1
2
3
4
5
val = do
	x <- safeDiv a b
	y <- safeDiv c x
	z <- safeDiv d y
	safeDiv e z

more

和范畴论有什么关系？因为其实还有一些性质是需要满足的。

haskell 中只存在一个范畴，所有类型的类作为对象，所有函数的类作为态射。

下面有一些很自然的性质 functor 实现了 fmap ，它需要满足

1
2
fmap id = id
fmap (f . g) = fmap f . fmap g

很好理解，和范畴论里面的 functor 的定义是一样的，单元要满足，同时交换性也要满足。

举个例子，对于都作用在 real 上的函子，那么我们的作用不能是 $ f \to F \ f^{-1} $ ，它虽然满足前一条但不满足后一条，也就是映射之后交换图不再直接交换了。显然这不是我们需要的，因为我们之后还要处理后续操作。

applicative functor 满足下面的性质

1
2
3
4
pure id <*> x = x
pure (g x) = pure g <*> pure x
x <*> pure y = pure (\g -> g y) <*> x
x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z

然而我并不知道为什么上面是对的，也许等更多的了解代数才行

来点看起来有趣的应用：

链式法则：$(g(x) -> f(g(x))) -> \frac{d(g(x))}{dx} -> \frac{d(f(g(x)))}{dx}$

构造这样一个函数就行了。

哥德尔不完备定理：强到蕴含皮亚诺算数公理的形式系统存在不能证明也不能证伪的命题。

哥德尔的认识到了命题不可证明和命题的反命题在形式系统中存在是不同的，构造了 $R_q(n)=n\in K,K=\set{n\mid\sim \mathrm{prov(R_n(n))}}$ ，一方面 $R_q(q)$ 和 $q\in K$ 等价，所以如果 $\mathrm{prov}(\ R_q(q)\ )$ 可证明，就有 $q\in n$ ，即 $\sim \mathrm{prov}(\ R_q(q)\ )$ ，所以 $R_q(q)$ 不可证。另一方面，$\sim R_q(q)$ ，等价于 $\sim (q\in K)$，等价于 $\sim (\sim \mathrm{prov}(R_q(q)))$ ， 等价于 $\mathrm{prov}(R_q(q))$ ，也就是 $\mathrm{prov}(\sim R_q(q))=\mathrm{prov\ }\mathrm{prov}(R_q(q))=\mathrm{prov}(R_q(q))$

在构造集合 $K$ 的时候，$q$ 是作为参数传入的，而 $q$ 在更高的层次，即脱离集合 $K$ 作为所有命题的集合的时候，$q$ 是作为标号存在的，也就是作为一个公式存在的。与符号 $\sim \mathrm{prov(S)}$ 相关的符号，一方面表示了 $S$ 的可证明和不可证明，另一方面表示了命题 $R=\mathrm{prov(S)}$ 和它的反命题。哥德尔构造出了一个命题，这个命题可证明 $\mathrm{prov}(R_q(q))$，和这个命题不可证明 $\sim \mathrm{prov}(\ R_q(q)\ )$，和这个命题的反命题 $\sim R_q(q)$ 可证明等价。我认为这个证明另一个巧妙的地方是如果 $\mathrm{prov}(\mathrm{prov}(S))$，则说明 $\mathrm{prov}(S)$ 是可证的，也就是 $S$ 是可证的，这里就消掉了一层 $\mathrm{prov}$。把两个不同层次的命题进行了比较。

某音乐课上推荐的课外读物《哥德尔，艾舍尔，巴赫》对层次自指与人工智能有很厚的探讨。

关于函数式编程我去年当时真不知道，当时以为就是编程的时候多写几个函数，那会儿还把过程和函数混为一谈，以为没什么区别。

后来听说计算概论实验班讲的是这个，就去翻了一翻ppt，当时看到那个 fmap ，太美了，真的太美了。后面不管是高阶函数，递归还是柯里化，真的是带给人美感。

应该说其思想真的很漂亮。

一些大家肯定见过的东西，比如在实际中广泛存在的一个wrap的东西，python的某个wrap装饰器是这么写的。

1
2
3
4
5
6
7
8
9
10
def 装饰器名(func):
     def wrapper(*args,**kwargs):
         #do something
         ret = func(*args,**kwargs)
         return ret
     return wrapper
 
@装饰器名
 def foo():
     pass

gcc在链接的时候也有-Wl,—wrap的选项，也是外面绑一个东西。

再比如后来的一些语言，比如 rust ，某种程度上就很有函数式那种味道。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
use rand::Rng;
use std::cmp::Ordering;
use std::io;

fn main() {
    println!("Guess the number!");

    let secret_number = rand::thread_rng().gen_range(1..=100);

    loop {
        println!("Please input your guess.");

        let mut guess = String::new();

        io::stdin()
            .read_line(&mut guess)
            .expect("Failed to read line");

        let guess: u32 = match guess.trim().parse() {
            Ok(num) => num,
            Err(_) => continue,
        };

        println!("You guessed: {guess}");

        match guess.cmp(&secret_number) {
            Ordering::Less => println!("Too small!"),
            Ordering::Greater => println!("Too big!"),
            Ordering::Equal => {
                println!("You win!");
                break;
            }
        }
    }
}

再比如用一个lambda实现递归，延伸出一种叫做 Y-组合子的。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
(lambda this:(
	lambda n : (
    	1 if n == 1 else(
        	2 if n == 2 else (
            	this(this)(n-1)+this(this)(n-2)
            )
        )
    )
))(
    lambda this:(
        lambda n : (
            1 if n == 1 else(
                2 if n == 2 else (
                    this(this)(n-1)+this(this)(n-2)
                )
            )
        ) 
    )
)(5)

上面是一个能实现递归求斐波那契数列第 n 项的python代码。

lambda演算是一种和图灵机等价的东西。大概和函数很像，也很漂亮。

完整解释 Monad _weixin_34111819的博客-CSDN博客

课程讲义 - 函数式程序设计 / 2021秋 (zhenjiang888.github.io)

emoairxPKU,EECS

春天来了，冬天还会远吗~