Haskell: Funktional Programming

安装 Haskell

进入这个网站 然后在终端运行他们的安装脚本

1
curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh

出现提示后就根据提示输入 YES 然后回车就好了

然后退出终端重新进入后，就可以了

在vscode中可以搜索安装 Haskell 插件

安装 stack 的 hlint 即可， 如果 stack 安装不了，可以更新一下系统再安装

1
2
sudo pacman -S stack
stack install hlint

安装package

比如安装 QuickCheck, 因为它是 library 所以加上 --lib

1
cabal install --lib QuickCheck

Haskell 基本语法

Haskell 网上教程

https://www.bookstack.cn/read/learnyouahaskell-zh-tw/README.md

Hello World

新建一个 hello.hs 文件

1
2
main :: IO ()
main = putStrLn "hello, world"

编译命令

1
ghc hello.hs

一键编译运行的时候可以使用

1
runhaskell hello.hs

在终端输入 ghci 可以进入交互界面

基本语句

stack ghci //运行haskell在命令行

1
2
3
4
5
6
7
:type True -- 显示True的类型
"Hello" ++ "World" --连接字符串
123 :: Float --用Float来解释123
['H','e','l','l','o'] --数组list
length "Hello" --求字符串长度
let a = undefined --未定义类型
:t (==) --解释类型

函数

定义函数 \(f:A\times B \rightarrow C\)

1
f :: A -> B -> C

调用函数 \(f(a), f(a,b), f(g(b)), f(a, g(b))\)

1
2
3
4
f a
f a b 
f (g b)
f a (g b)

优先级

1
f a + b   === (f a) + b

布尔运算

这些是定义好的，最后一个是不等于

1
True False not && || == /=

数据类型

  • Bool
  • Integer
  • Char
  • String
  • Tuple

QuickCheck

首先安装好 QuickCheck, 上文有提到， 然后import一下

1
import Test.QuickCheck

我们这里定义2个函数

1
2
xor2 :: Bool -> Bool -> Bool
xor2 x y = (x || y) && not(x && y)

下面这个是用 pattern matching 的方式定义的

1
2
3
4
5
xor :: Bool -> Bool -> Bool
xor True True = False
xor True False = True
xor False True = True
xor False False = False

然后在 main 里面写

1
2
main = do
	quickCheck prop_xor2

就可以测试了

Integer

大整数类型

运算符有

1
+ - * ^ div mod abs == /= < <= > >=

Int

是至少 29bit 的整数类型

输出语句

1
2
print 3
putStrLn "hello"

函数里面的分支

1
2
3
4
max2 :: Integer -> Integer -> Integer
max2 x y
| x >= y = x
| otherwise = y

或者写在行内

1
max2 x y = if x >= y then x else y

List

list 类型是在外面加一个方括号

如 [Int]

1
[1 .. 5] = [1, 2, 3, 4, 5]

列表相加

只能相同类型的

1
[1, 2] ++ [3] = [1, 2, 3]

List Comprehension

Generators

\[ \left\{x^{2} \mid x \in\{1,2,3,4,5\}\right\} \]

1
2
3
[x^2 | x <- [1 .. 5]]
[(x, even x) | x <- [1 .. 3]]
[x+y | (x, y) <- [(1, 2), (3, 4), (5, 6)]]

多重生成器

1
2
3
4
5
6
7
[(i,j) | i <- [1 .. 2], j <- [7 .. 9]]
[(i,j) | i <- [1 .. 3], j <- [i .. 3]]
= [(1,j) | j <- [1..3]] ++
  [(2,j) | j <- [2..3]] ++
  [(3,j) | j <- [3..3]]
= [(1,1), (1,2), (1,3), (2,2), (2,3), (3,3)]

Tests
1
2
[x*x | x <- [1 .. 5], odd x]
= [1, 9, 25]

concat

1
2
3
4
5
concat [[1,2], [4,5,6]]
= [x | xs <- [[1,2], [4,5,6]], x <- xs]
= [x | x <- [1,2]] ++ [x | x <- [4,5,6]]
= [1,2] ++ [4,5,6]
= [1,2,4,5,6]

抽象函数

下面 a 是一个类型变量

1
length :: [a] -> Int

https://blog.csdn.net/zwvista/article/details/61454004

1
2
3
4
5
6
7
8
9
10
id :: a -> a
id x = x
fst :: (a,b) -> a
fst (x,y) = x
swap :: (a,b) -> (b,a)
swap (x,y) = (y,x)
silly :: Bool -> a -> Char
silly x y = if x then ’c’ else ’d’
silly2 :: Bool -> Bool -> Bool
silly2 x y = if x then x else y

Num 是一个数字类型，比如 Int,Integer,Float 也是

证明

cyp

.cprf 证明文件

.cthy 定理文件

运行证明

先进入cyp的根目录，然后运行下面的命令

1
stack run cyp [.cthy] [.cprf]

一般证明

1
2
3
4
5
6
Lemma sndUnspliceNil: snd (unsplice []) .=. []
  Proof
                          snd (unsplice [])
    (by def unsplice) .=. snd (Pair [] [])
    (by def snd)      .=. []
  QED

Proof by Induction

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Lemma appNil: xs ++ [] .=. xs
Proof by induction on List xs
Case []
    To show: [] ++ [] .=. []
    Proof
                                   [] ++ []
            (by def ++)        .=. []
    QED
Case (x:xs)
    To show: (x:xs) ++ [] .=. (x:xs)
    IH: xs ++ [] .=. xs
    Proof
                                   (x:xs) ++ []
            (by def ++)        .=. x : (xs ++ [])
            (by IH)            .=. x : xs
    QED
QED

Proof by Cases

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Lemma fstUnspliceF: fst (unsplice xs') .=. drop2 xs'
Proof by case analysis on List xs'
Case []
  Assumption : xs' .=. []
  Proof 
    fst (unsplice xs')
  (by Assumption) .=. fst (unsplice [])
  (by fstUnspliceNil) .=. []
  (by def drop2) .=. drop2 []
  (by Assumption) .=. drop2 xs'
QED
Case x:xs
  Assumption : xs' .=. x:xs
  Proof 
      fst (unsplice xs')
  (by Assumption) .=. fst (unsplice (x:xs))
  (by fstUnsplice) .=. drop2 (x:xs)
  (by Assumption) .=. drop2 xs'
  QED
QED

Proof by computation induction

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
36
37

Lemma spliceDrop2: splice (drop2 (x : xs)) (drop2 xs) .=. x : xs
Proof by computation induction on xs with drop2
  Case 1
    To show: splice (drop2 [x]) (drop2 []) .=. [x]
    Proof
                                splice (drop2 [x]) (drop2 [])
      (by def drop2)        .=. splice [x] (drop2 [])
      (by def drop2)        .=. splice [x] []
      (by def splice)       .=. x : splice [] []
      (by def splice)       .=. [x]
    QED

  Case 2
    To show: splice (drop2 [x, y]) (drop2 [y]) .=. [x, y]
    Proof
                                splice (drop2 [x, y]) (drop2 [y])   
      (by def drop2)        .=. splice (drop2 [x, y]) [y]
      (by def drop2)        .=. splice (x : drop2 []) [y]
      (by def drop2)        .=. splice [x] [y]
      (by def splice)       .=. x : splice [y] []
      (by def splice)       .=. x : y : splice [] []
      (by def splice)       .=. [x, y]
    QED

  Case 3
    To show: splice (drop2 (x : y : z : xs)) (drop2 (y : z : xs)) .=. x : y : z : xs
    IH: splice (drop2 (x : xs)) (drop2 xs) .=. x : xs
    Proof
                                splice (drop2 (x : y : z : xs)) (drop2 (y : z : xs))
      (by def drop2)        .=. splice (x : drop2 (z : xs)) (drop2 (y : z : xs))
      (by def drop2)        .=. splice (x : drop2 (z : xs)) (y : drop2 xs)
      (by def splice)       .=. x : splice (y : drop2 xs) (drop2 (z : xs))
      (by def splice)       .=. x : y : splice (drop2 (z : xs)) (drop2 xs)
      (by IH)               .=. x : y : z : xs
    QED
QED

map

把一个函数映射到所以元素

1
2
map even [1, 2, 3]
= [False, True, False]

lambda 表达式

Type Classes

定义具体类

1
2
3
4
5
instance Eq a => Eq [a] where
[] == [] = True
(x:xs) == (y:ys) = x == y && xs == ys
_ == _ = False

定义约束条件

1
2
3
4
5
6
7
8
9
10
11
class Size a where 
    size :: a -> Float

data Shape = Square Float | Circle Float

instance Size Shape where
    size (Square a) = a*a
    size (Circle a) = a*a*pi 

instance Size a => Size [a]  where
    size xs = sum (map size xs)

IO

IO Char: 返回一个Char类型的动作

IO (): 没有返回的动作

基础动作

1
2
3
getChar :: IO Char
putChar :: Char -> IO ()
return :: a -> IO a

do 来连接

1
2
3
4
5
get2 :: IO (Char,Char)
get2 = do x <- getChar -- result is named x
		  getChar -- result is ignored
		  y <- getChar
		  return (x,y)

strlen

1
2
3
4
5
6
7
strLen :: IO ()
strLen = do putStr "Enter a string: "
xs <- getLine
putStr "The string has "
putStr (show (length xs))
putStrLn " characters"

读入int

1
2
3
4
5
6
7
8
readNum :: IO Integer 
readNum = do
    x <- readLn
    if 1 <= x && x <= 5 then
        return x
    else do
        putStrLn "Eingabe muss zwischen 1 und 5 liegen ."
        readNum

putStrLn

连接变量

1
2
putStrLn $ " Streichhoelzer : "
           ++ show a ++ ". Spieler " ++ show s ++ "?"

递归例子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17


ioSeq :: [IO a] -> IO [a]
ioSeq [] = return []
ioSeq (x:xs) = do
    y <- x
    ys <- ioSeq xs
    return (y : ys)

getio :: String -> IO String 
getio s = do
    putStrLn $ s ++ "?"
    getLine

fillForm :: [String] -> IO [String]
fillForm xs = ioSeq [getio x | x <- xs]

文件IO

Modules and Abstract Data Types

Lazy evaluation